:: Continuous Lattices between T$_0$ Spaces :: by Grzegorz Bancerek :: :: Received September 24, 1999 :: Copyright (c) 1999-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies YELLOW_1, PBOOLE, CARD_3, WAYBEL18, WAYBEL_3, XBOOLE_0, PRE_TOPC, STRUCT_0, ORDERS_2, WAYBEL24, WAYBEL25, RELAT_2, MONOID_0, SUBSET_1, ORDINAL2, FUNCT_1, XXREAL_0, CAT_1, YELLOW_0, NEWTON, TARSKI, YELLOW_9, WAYBEL11, ZFMISC_1, CARD_1, RCOMP_1, FUNCT_3, RELAT_1, WELLORD1, VALUED_1, T_0TOPSP, WAYBEL_0, SEQM_3, BINOP_1, FUNCOP_1, BORSUK_1, GROUP_6, YELLOW16, TOPS_2, REWRITE1, LATTICE3, EQREL_1, FUNCTOR0, WAYBEL_1, FUNCT_6, RLVECT_2, FUNCT_2, CANTOR_1, FUNCT_4, WAYBEL_9, MCART_1, FINSET_1, SETFAM_1, WAYBEL26; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1, FINSET_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, TOPS_2, FUNCT_3, FUNCT_4, ORDINAL1, NUMBERS, SETFAM_1, FUNCT_2, FUNCOP_1, STRUCT_0, CARD_3, FUNCT_6, MONOID_0, PRALG_1, FUNCT_7, WELLORD1, ORDERS_2, LATTICE3, PRE_TOPC, CANTOR_1, T_0TOPSP, BORSUK_1, QUANTAL1, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_9, WAYBEL_3, WAYBEL_9, WAYBEL11, WAYBEL18, WAYBEL24, WAYBEL25, YELLOW16; constructors TOLER_1, FUNCT_7, TOPS_2, BORSUK_1, T_0TOPSP, CANTOR_1, MONOID_0, QUANTAL1, ORDERS_3, PRALG_3, WAYBEL_1, WAYBEL11, YELLOW_9, WAYBEL18, WAYBEL24, WAYBEL25, YELLOW16, XTUPLE_0, XFAMILY; registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, STRUCT_0, PRE_TOPC, BORSUK_1, LATTICE3, YELLOW_0, TSP_1, MONOID_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3, YELLOW_6, WAYBEL10, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL24, YELLOW14, WAYBEL25, YELLOW16, FUNCT_1, XTUPLE_0; requirements SUBSET, BOOLE, NUMERALS; begin notation let I be set; let J be RelStr-yielding ManySortedSet of I; synonym I-POS_prod J for product J; end; notation let I be set; let J be TopStruct-yielding non-Empty ManySortedSet of I; synonym I-TOP_prod J for product J; end; :: 4.1. DEFINITION (a) definition let X,Y be non empty TopSpace; func oContMaps(X, Y) -> non empty strict RelStr equals :: WAYBEL26:def 1 ContMaps(X, Omega Y); end; registration let X,Y be non empty TopSpace; cluster oContMaps(X, Y) -> reflexive transitive constituted-Functions; end; registration let X be non empty TopSpace; let Y be non empty T_0 TopSpace; cluster oContMaps(X, Y) -> antisymmetric; end; theorem :: WAYBEL26:1 for X,Y being non empty TopSpace for a being set holds a is Element of oContMaps(X, Y) iff a is continuous Function of X, Omega Y; theorem :: WAYBEL26:2 for X,Y being non empty TopSpace for a being set holds a is Element of oContMaps(X, Y) iff a is continuous Function of X, Y; theorem :: WAYBEL26:3 :: see yellow14:9 for X,Y being non empty TopSpace for a,b being Element of oContMaps(X,Y) for f,g being Function of X, Omega Y st a = f & b = g holds a <= b iff f <= g; definition let X,Y be non empty TopSpace; let x be Point of X; let A be Subset of oContMaps(X,Y); redefine func pi(A,x) -> Subset of Omega Y; end; registration let X,Y be non empty TopSpace; let x be set; let A be non empty Subset of oContMaps(X,Y); cluster pi(A,x) -> non empty; end; theorem :: WAYBEL26:4 Omega Sierpinski_Space is TopAugmentation of BoolePoset{0}; theorem :: WAYBEL26:5 for X being non empty TopSpace ex f being Function of InclPoset the topology of X, oContMaps(X, Sierpinski_Space) st f is isomorphic & for V being open Subset of X holds f.V = chi(V, the carrier of X); theorem :: WAYBEL26:6 for X being non empty TopSpace holds InclPoset the topology of X, oContMaps(X, Sierpinski_Space) are_isomorphic; :: 4.1. DEFINITION (b) definition let X,Y,Z be non empty TopSpace; let f be continuous Function of Y,Z; func oContMaps(X, f) -> Function of oContMaps(X, Y), oContMaps(X, Z) means :: WAYBEL26:def 2 for g being continuous Function of X,Y holds it.g = f*g; func oContMaps(f, X) -> Function of oContMaps(Z, X), oContMaps(Y, X) means :: WAYBEL26:def 3 for g being continuous Function of Z, X holds it.g = g*f; end; theorem :: WAYBEL26:7 for X being non empty TopSpace for Y being monotone-convergence T_0-TopSpace holds oContMaps(X, Y) is up-complete; theorem :: WAYBEL26:8 for X,Y,Z being non empty TopSpace for f being continuous Function of Y,Z holds oContMaps(X, f) is monotone; theorem :: WAYBEL26:9 for X,Y being non empty TopSpace for f being continuous Function of Y, Y st f is idempotent holds oContMaps(X, f) is idempotent; theorem :: WAYBEL26:10 for X,Y,Z being non empty TopSpace for f being continuous Function of Y,Z holds oContMaps(f, X) is monotone; theorem :: WAYBEL26:11 for X,Y being non empty TopSpace for f being continuous Function of Y,Y st f is idempotent holds oContMaps(f, X) is idempotent; theorem :: WAYBEL26:12 for X,Y,Z being non empty TopSpace for f being continuous Function of Y,Z for x being Element of X, A being Subset of oContMaps(X, Y) holds pi(oContMaps(X,f).:A, x) = f.:pi(A, x); :: 4.2. LEMMA (ii) theorem :: WAYBEL26:13 for X being non empty TopSpace for Y,Z being monotone-convergence T_0-TopSpace for f being continuous Function of Y,Z holds oContMaps(X, f) is directed-sups-preserving; theorem :: WAYBEL26:14 for X,Y,Z being non empty TopSpace for f being continuous Function of Y,Z for x being Element of Y, A being Subset of oContMaps(Z, X) holds pi(oContMaps(f, X).:A, x) = pi(A, f.x); theorem :: WAYBEL26:15 for Y,Z being non empty TopSpace for X being monotone-convergence T_0-TopSpace for f being continuous Function of Y,Z holds oContMaps(f, X) is directed-sups-preserving; :: 4.3. LEMMA (i) genralized theorem :: WAYBEL26:16 for X,Z being non empty TopSpace for Y being non empty SubSpace of Z holds oContMaps(X, Y) is full SubRelStr of oContMaps(X, Z); theorem :: WAYBEL26:17 for Z being monotone-convergence T_0-TopSpace for Y being non empty SubSpace of Z for f being continuous Function of Z,Y st f is being_a_retraction holds Omega Y is directed-sups-inheriting SubRelStr of Omega Z; theorem :: WAYBEL26:18 for X being non empty TopSpace for Z being monotone-convergence T_0-TopSpace for Y being non empty SubSpace of Z for f being continuous Function of Z,Y st f is being_a_retraction holds oContMaps(X, f) is_a_retraction_of oContMaps(X, Z), oContMaps(X, Y); theorem :: WAYBEL26:19 for X being non empty TopSpace for Z being monotone-convergence T_0-TopSpace for Y being non empty SubSpace of Z st Y is_a_retract_of Z holds oContMaps(X, Y) is_a_retract_of oContMaps(X, Z); theorem :: WAYBEL26:20 for X,Y,Z being non empty TopSpace for f being continuous Function of Y,Z st f is being_homeomorphism holds oContMaps(X, f) is isomorphic ; theorem :: WAYBEL26:21 for X,Y,Z being non empty TopSpace st Y,Z are_homeomorphic holds oContMaps(X, Y), oContMaps(X, Z) are_isomorphic; :: 4.3. LEMMA (ii) theorem :: WAYBEL26:22 for X being non empty TopSpace for Z being monotone-convergence T_0-TopSpace for Y being non empty SubSpace of Z st Y is_a_retract_of Z & oContMaps(X, Z) is complete continuous holds oContMaps(X, Y) is complete continuous; theorem :: WAYBEL26:23 for X being non empty TopSpace for Y,Z being monotone-convergence T_0-TopSpace st Y is_Retract_of Z & oContMaps(X, Z) is complete continuous holds oContMaps(X, Y) is complete continuous; theorem :: WAYBEL26:24 for Y being non trivial T_0-TopSpace st not Y is T_1 holds Sierpinski_Space is_Retract_of Y; theorem :: WAYBEL26:25 for X being non empty TopSpace for Y being non trivial T_0-TopSpace st oContMaps(X, Y) is with_suprema holds not Y is T_1; registration cluster Sierpinski_Space -> non trivial monotone-convergence; end; registration cluster injective monotone-convergence non trivial for T_0-TopSpace; end; :: 4.4. PROPOSITION theorem :: WAYBEL26:26 for X being non empty TopSpace for Y being monotone-convergence non trivial T_0-TopSpace st oContMaps(X, Y) is complete continuous holds InclPoset the topology of X is continuous; theorem :: WAYBEL26:27 for X being non empty TopSpace, x being Point of X for Y being monotone-convergence T_0-TopSpace ex F being directed-sups-preserving projection Function of oContMaps(X,Y), oContMaps(X,Y) st (for f being continuous Function of X,Y holds F.f = X --> (f.x)) & ex h being continuous Function of X,X st h = X --> x & F = oContMaps(h, Y); :: 4.5. PROPOSITION theorem :: WAYBEL26:28 for X being non empty TopSpace, Y being monotone-convergence T_0-TopSpace st oContMaps(X, Y) is complete continuous holds Omega Y is complete continuous; theorem :: WAYBEL26:29 for X being non empty 1-sorted, I being non empty set for J being TopStruct-yielding non-Empty ManySortedSet of I for f being Function of X, I-TOP_prod J for i being Element of I holds (commute f).i = proj(J,i)*f; theorem :: WAYBEL26:30 for S being 1-sorted, M being set holds Carrier (M --> S) = M --> the carrier of S; theorem :: WAYBEL26:31 for X,Y being non empty TopSpace, M being non empty set for f being continuous Function of X, M-TOP_prod (M --> Y) holds commute f is Function of M, the carrier of oContMaps(X, Y); theorem :: WAYBEL26:32 for X,Y being non empty TopSpace holds the carrier of oContMaps( X, Y) c= Funcs(the carrier of X, the carrier of Y); theorem :: WAYBEL26:33 for X,Y being non empty TopSpace, M being non empty set for f being Function of M, the carrier of oContMaps(X, Y) holds commute f is continuous Function of X, M-TOP_prod (M --> Y); theorem :: WAYBEL26:34 for X being non empty TopSpace, M being non empty set ex F being Function of oContMaps(X, M-TOP_prod (M --> Sierpinski_Space)), M-POS_prod (M --> oContMaps(X, Sierpinski_Space)) st F is isomorphic & for f being continuous Function of X, M-TOP_prod (M --> Sierpinski_Space) holds F.f = commute f; theorem :: WAYBEL26:35 for X being non empty TopSpace, M being non empty set holds oContMaps(X, M-TOP_prod (M --> Sierpinski_Space)), M-POS_prod (M --> oContMaps( X, Sierpinski_Space)) are_isomorphic; :: 4.6. PROPOSITION theorem :: WAYBEL26:36 for X being non empty TopSpace st InclPoset the topology of X is continuous for Y being injective T_0-TopSpace holds oContMaps(X, Y) is complete continuous; registration cluster non trivial complete Scott for TopLattice; end; :: 4.7. THEOREM p.129. theorem :: WAYBEL26:37 for X being non empty TopSpace for L being non trivial complete Scott TopLattice holds oContMaps(X, L) is complete continuous iff InclPoset the topology of X is continuous & L is continuous; registration let f be Function; cluster Union disjoin f -> Relation-like; end; definition let f be Function; func *graph f -> Relation equals :: WAYBEL26:def 4 (Union disjoin f)~; end; reserve x,y for object, f for Function; theorem :: WAYBEL26:38 [x,y] in *graph f iff x in dom f & y in f.x; theorem :: WAYBEL26:39 for X being finite set holds proj1 X is finite & proj2 X is finite; :: 4.8. LEMMA p.130. theorem :: WAYBEL26:40 for X,Y being non empty TopSpace for S being Scott TopAugmentation of InclPoset the topology of Y for f being Function of X, S st *graph f is open Subset of [:X,Y:] holds f is continuous; definition let W be Relation, X be set; func (W,X)*graph -> Function means :: WAYBEL26:def 5 dom it = X & for x being object st x in X holds it.x = Im(W,x); end; theorem :: WAYBEL26:41 for W being Relation, X being set st dom W c= X holds *graph((W, X)*graph) = W; registration let X, Y be TopSpace; cluster -> Relation-like for Subset of [:X,Y:]; cluster -> Relation-like for Element of the topology of [:X,Y:]; end; theorem :: WAYBEL26:42 for X,Y being non empty TopSpace for W being open Subset of [:X, Y:] for x being Point of X holds Im(W,x) is open Subset of Y; :: 4.9. PROPOSITION a) p.130. theorem :: WAYBEL26:43 for X,Y being non empty TopSpace for S being Scott TopAugmentation of InclPoset the topology of Y for W being open Subset of [:X,Y :] holds (W, the carrier of X)*graph is continuous Function of X, S; :: 4.9. PROPOSITION b) p.130. theorem :: WAYBEL26:44 for X,Y being non empty TopSpace for S being Scott TopAugmentation of InclPoset the topology of Y for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 for f1, f2 being Element of oContMaps(X, S) st f1 = (W1, the carrier of X)*graph & f2 = (W2, the carrier of X)*graph holds f1 <= f2; :: 4.9. PROPOSITION p.130. theorem :: WAYBEL26:45 for X,Y being non empty TopSpace for S being Scott TopAugmentation of InclPoset the topology of Y ex F being Function of InclPoset the topology of [: X, Y:], oContMaps(X, S) st F is monotone & for W being open Subset of [:X,Y:] holds F.W = (W, the carrier of X)*graph;