:: WAYBEL25 semantic presentation begin theorem :: WAYBEL25:1 for p being Point of Sierpinski_Space st p = 0 holds {p} is closed proof set S = Sierpinski_Space ; let p be Point of Sierpinski_Space; ::_thesis: ( p = 0 implies {p} is closed ) A1: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9; assume A2: p = 0 ; ::_thesis: {p} is closed A3: ([#] Sierpinski_Space) \ {p} = {1} proof thus ([#] Sierpinski_Space) \ {p} c= {1} :: according to XBOOLE_0:def_10 ::_thesis: {1} c= ([#] Sierpinski_Space) \ {p} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ([#] Sierpinski_Space) \ {p} or a in {1} ) assume A4: a in ([#] Sierpinski_Space) \ {p} ; ::_thesis: a in {1} then not a in {p} by XBOOLE_0:def_5; then a <> 0 by A2, TARSKI:def_1; then a = 1 by A1, A4, TARSKI:def_2; hence a in {1} by TARSKI:def_1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {1} or a in ([#] Sierpinski_Space) \ {p} ) assume a in {1} ; ::_thesis: a in ([#] Sierpinski_Space) \ {p} then A5: a = 1 by TARSKI:def_1; then A6: not a in {p} by A2, TARSKI:def_1; a in [#] Sierpinski_Space by A1, A5, TARSKI:def_2; hence a in ([#] Sierpinski_Space) \ {p} by A6, XBOOLE_0:def_5; ::_thesis: verum end; the topology of Sierpinski_Space = {{},{1},{0,1}} by WAYBEL18:def_9; hence ([#] Sierpinski_Space) \ {p} in the topology of Sierpinski_Space by A3, ENUMSET1:def_1; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: verum end; theorem Th2: :: WAYBEL25:2 for p being Point of Sierpinski_Space st p = 1 holds not {p} is closed proof set S = Sierpinski_Space ; let p be Point of Sierpinski_Space; ::_thesis: ( p = 1 implies not {p} is closed ) A1: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9; assume A2: p = 1 ; ::_thesis: not {p} is closed A3: ([#] Sierpinski_Space) \ {p} = {0} proof thus ([#] Sierpinski_Space) \ {p} c= {0} :: according to XBOOLE_0:def_10 ::_thesis: {0} c= ([#] Sierpinski_Space) \ {p} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ([#] Sierpinski_Space) \ {p} or a in {0} ) assume A4: a in ([#] Sierpinski_Space) \ {p} ; ::_thesis: a in {0} then not a in {p} by XBOOLE_0:def_5; then a <> 1 by A2, TARSKI:def_1; then a = 0 by A1, A4, TARSKI:def_2; hence a in {0} by TARSKI:def_1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {0} or a in ([#] Sierpinski_Space) \ {p} ) assume a in {0} ; ::_thesis: a in ([#] Sierpinski_Space) \ {p} then A5: a = 0 by TARSKI:def_1; then A6: not a in {p} by A2, TARSKI:def_1; a in [#] Sierpinski_Space by A1, A5, TARSKI:def_2; hence a in ([#] Sierpinski_Space) \ {p} by A6, XBOOLE_0:def_5; ::_thesis: verum end; A7: {0} <> {1} by ZFMISC_1:3; A8: {0} <> {0,1} by ZFMISC_1:5; the topology of Sierpinski_Space = {{},{1},{0,1}} by WAYBEL18:def_9; hence not ([#] Sierpinski_Space) \ {p} in the topology of Sierpinski_Space by A7, A8, A3, ENUMSET1:def_1; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: verum end; registration cluster Sierpinski_Space -> non T_1 ; coherence not Sierpinski_Space is T_1 proof set S = Sierpinski_Space ; ex p being Point of Sierpinski_Space st Cl {p} <> {p} proof the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9; then reconsider p = 1 as Point of Sierpinski_Space by TARSKI:def_2; take p ; ::_thesis: Cl {p} <> {p} thus Cl {p} <> {p} by Th2; ::_thesis: verum end; hence not Sierpinski_Space is T_1 by YELLOW_8:26; ::_thesis: verum end; end; registration cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott -> T_0 for TopRelStr ; coherence for b1 being TopLattice st b1 is complete & b1 is Scott holds b1 is T_0 by WAYBEL11:10; end; registration cluster non empty strict TopSpace-like T_0 injective for TopStruct ; existence ex b1 being T_0-TopSpace st ( b1 is injective & b1 is strict ) proof take Sierpinski_Space ; ::_thesis: ( Sierpinski_Space is injective & Sierpinski_Space is strict ) thus ( Sierpinski_Space is injective & Sierpinski_Space is strict ) ; ::_thesis: verum end; end; registration cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott for TopRelStr ; existence ex b1 being TopLattice st ( b1 is complete & b1 is Scott & b1 is strict ) proof set T = the complete strict Scott TopLattice; take the complete strict Scott TopLattice ; ::_thesis: ( the complete strict Scott TopLattice is complete & the complete strict Scott TopLattice is Scott & the complete strict Scott TopLattice is strict ) thus ( the complete strict Scott TopLattice is complete & the complete strict Scott TopLattice is Scott & the complete strict Scott TopLattice is strict ) ; ::_thesis: verum end; end; theorem Th3: :: WAYBEL25:3 for I being non empty set for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds the carrier of T = the carrier of (product (I --> Sierpinski_Space)) proof set S = Sierpinski_Space ; set B = BoolePoset 1; let I be non empty set ; ::_thesis: for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds the carrier of T = the carrier of (product (I --> Sierpinski_Space)) let T be Scott TopAugmentation of product (I --> (BoolePoset 1)); ::_thesis: the carrier of T = the carrier of (product (I --> Sierpinski_Space)) A1: dom (Carrier (I --> (BoolePoset 1))) = I by PARTFUN1:def_2; A2: dom (Carrier (I --> Sierpinski_Space)) = I by PARTFUN1:def_2; A3: for x being set st x in dom (Carrier (I --> Sierpinski_Space)) holds (Carrier (I --> (BoolePoset 1))) . x = (Carrier (I --> Sierpinski_Space)) . x proof let x be set ; ::_thesis: ( x in dom (Carrier (I --> Sierpinski_Space)) implies (Carrier (I --> (BoolePoset 1))) . x = (Carrier (I --> Sierpinski_Space)) . x ) assume A4: x in dom (Carrier (I --> Sierpinski_Space)) ; ::_thesis: (Carrier (I --> (BoolePoset 1))) . x = (Carrier (I --> Sierpinski_Space)) . x then A5: ex T being 1-sorted st ( T = (I --> Sierpinski_Space) . x & (Carrier (I --> Sierpinski_Space)) . x = the carrier of T ) by PRALG_1:def_13; ex R being 1-sorted st ( R = (I --> (BoolePoset 1)) . x & (Carrier (I --> (BoolePoset 1))) . x = the carrier of R ) by A4, PRALG_1:def_13; hence (Carrier (I --> (BoolePoset 1))) . x = the carrier of (BoolePoset 1) by A4, FUNCOP_1:7 .= bool 1 by WAYBEL_7:2 .= the carrier of Sierpinski_Space by WAYBEL18:def_9, YELLOW14:1 .= (Carrier (I --> Sierpinski_Space)) . x by A4, A5, FUNCOP_1:7 ; ::_thesis: verum end; RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of (product (I --> (BoolePoset 1))), the InternalRel of (product (I --> (BoolePoset 1))) #) by YELLOW_9:def_4; hence the carrier of T = product (Carrier (I --> (BoolePoset 1))) by YELLOW_1:def_4 .= product (Carrier (I --> Sierpinski_Space)) by A1, A2, A3, FUNCT_1:2 .= the carrier of (product (I --> Sierpinski_Space)) by WAYBEL18:def_3 ; ::_thesis: verum end; theorem Th4: :: WAYBEL25:4 for L1, L2 being complete LATTICE for T1 being Scott TopAugmentation of L1 for T2 being Scott TopAugmentation of L2 for h being Function of L1,L2 for H being Function of T1,T2 st h = H & h is isomorphic holds H is being_homeomorphism proof let L1, L2 be complete LATTICE; ::_thesis: for T1 being Scott TopAugmentation of L1 for T2 being Scott TopAugmentation of L2 for h being Function of L1,L2 for H being Function of T1,T2 st h = H & h is isomorphic holds H is being_homeomorphism let T1 be Scott TopAugmentation of L1; ::_thesis: for T2 being Scott TopAugmentation of L2 for h being Function of L1,L2 for H being Function of T1,T2 st h = H & h is isomorphic holds H is being_homeomorphism let T2 be Scott TopAugmentation of L2; ::_thesis: for h being Function of L1,L2 for H being Function of T1,T2 st h = H & h is isomorphic holds H is being_homeomorphism let h be Function of L1,L2; ::_thesis: for H being Function of T1,T2 st h = H & h is isomorphic holds H is being_homeomorphism let H be Function of T1,T2; ::_thesis: ( h = H & h is isomorphic implies H is being_homeomorphism ) assume that A1: h = H and A2: h is isomorphic ; ::_thesis: H is being_homeomorphism A3: RelStr(# the carrier of L2, the InternalRel of L2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) by YELLOW_9:def_4; A4: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) by YELLOW_9:def_4; then reconsider H9 = h " as Function of T2,T1 by A3; consider g being Function of L2,L1 such that A5: g = h " ; g = h " by A2, A5, TOPS_2:def_4; then g is isomorphic by A2, WAYBEL_0:68; then reconsider h2 = h " as sups-preserving Function of L2,L1 by A5, WAYBEL13:20; A6: rng H = [#] T2 by A1, A2, A3, WAYBEL_0:66; A7: for x being set st x in dom H9 holds H9 . x = (H ") . x proof let x be set ; ::_thesis: ( x in dom H9 implies H9 . x = (H ") . x ) assume x in dom H9 ; ::_thesis: H9 . x = (H ") . x A8: H is onto by A6, FUNCT_2:def_3; thus H9 . x = (h ") . x by A2, TOPS_2:def_4 .= (H ") . x by A1, A2, A8, TOPS_2:def_4 ; ::_thesis: verum end; h2 is directed-sups-preserving ; then A9: H9 is directed-sups-preserving by A4, A3, WAYBEL21:6; dom (H ") = the carrier of T2 by FUNCT_2:def_1 .= dom H9 by FUNCT_2:def_1 ; then A10: H " = H9 by A7, FUNCT_1:2; reconsider h1 = h as sups-preserving Function of L1,L2 by A2, WAYBEL13:20; h1 is directed-sups-preserving ; then A11: H is directed-sups-preserving by A1, A4, A3, WAYBEL21:6; dom H = [#] T1 by FUNCT_2:def_1; hence H is being_homeomorphism by A1, A2, A11, A9, A6, A10, TOPS_2:def_5; ::_thesis: verum end; theorem Th5: :: WAYBEL25:5 for L1, L2 being complete LATTICE for T1 being Scott TopAugmentation of L1 for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic holds T1,T2 are_homeomorphic proof let L1, L2 be complete LATTICE; ::_thesis: for T1 being Scott TopAugmentation of L1 for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic holds T1,T2 are_homeomorphic let T1 be Scott TopAugmentation of L1; ::_thesis: for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic holds T1,T2 are_homeomorphic let T2 be Scott TopAugmentation of L2; ::_thesis: ( L1,L2 are_isomorphic implies T1,T2 are_homeomorphic ) given h being Function of L1,L2 such that A1: h is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: T1,T2 are_homeomorphic A2: RelStr(# the carrier of L2, the InternalRel of L2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) by YELLOW_9:def_4; RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) by YELLOW_9:def_4; then reconsider H = h as Function of T1,T2 by A2; take H ; :: according to T_0TOPSP:def_1 ::_thesis: H is being_homeomorphism thus H is being_homeomorphism by A1, Th4; ::_thesis: verum end; theorem Th6: :: WAYBEL25:6 for S, T being non empty TopSpace st S is injective & S,T are_homeomorphic holds T is injective proof let S, T be non empty TopSpace; ::_thesis: ( S is injective & S,T are_homeomorphic implies T is injective ) assume that A1: S is injective and A2: S,T are_homeomorphic ; ::_thesis: T is injective consider p being Function of S,T such that A3: p is being_homeomorphism by A2, T_0TOPSP:def_1; let X be non empty TopSpace; :: according to WAYBEL18:def_5 ::_thesis: for b1 being Element of bool [: the carrier of X, the carrier of T:] holds ( not b1 is continuous or for b2 being TopStruct holds ( not X is SubSpace of b2 or ex b3 being Element of bool [: the carrier of b2, the carrier of T:] st ( b3 is continuous & b3 | the carrier of X = b1 ) ) ) let f be Function of X,T; ::_thesis: ( not f is continuous or for b1 being TopStruct holds ( not X is SubSpace of b1 or ex b2 being Element of bool [: the carrier of b1, the carrier of T:] st ( b2 is continuous & b2 | the carrier of X = f ) ) ) assume A4: f is continuous ; ::_thesis: for b1 being TopStruct holds ( not X is SubSpace of b1 or ex b2 being Element of bool [: the carrier of b1, the carrier of T:] st ( b2 is continuous & b2 | the carrier of X = f ) ) let Y be non empty TopSpace; ::_thesis: ( not X is SubSpace of Y or ex b1 being Element of bool [: the carrier of Y, the carrier of T:] st ( b1 is continuous & b1 | the carrier of X = f ) ) assume A5: X is SubSpace of Y ; ::_thesis: ex b1 being Element of bool [: the carrier of Y, the carrier of T:] st ( b1 is continuous & b1 | the carrier of X = f ) then A6: [#] X c= [#] Y by PRE_TOPC:def_4; A7: p is V7() by A3, TOPS_2:58; set F = (p ") * f; p " is continuous by A3, TOPS_2:def_5; then consider G being Function of Y,S such that A8: G is continuous and A9: G | the carrier of X = (p ") * f by A1, A4, A5, WAYBEL18:def_5; take g = p * G; ::_thesis: ( g is continuous & g | the carrier of X = f ) A10: rng p = [#] T by A3, TOPS_2:58; A11: for x being set st x in dom f holds g . x = f . x proof let x be set ; ::_thesis: ( x in dom f implies g . x = f . x ) assume A12: x in dom f ; ::_thesis: g . x = f . x then A13: f . x in rng f by FUNCT_1:def_3; then f . x in the carrier of T ; then A14: f . x in dom (p ") by FUNCT_2:def_1; x in the carrier of X by A12; then x in the carrier of Y by A6; then x in dom G by FUNCT_2:def_1; hence g . x = p . (G . x) by FUNCT_1:13 .= p . (((p ") * f) . x) by A9, A12, FUNCT_1:49 .= p . ((p ") . (f . x)) by A12, FUNCT_1:13 .= (p * (p ")) . (f . x) by A14, FUNCT_1:13 .= (id the carrier of T) . (f . x) by A10, A7, TOPS_2:52 .= f . x by A13, FUNCT_1:17 ; ::_thesis: verum end; p is continuous by A3, TOPS_2:def_5; hence g is continuous by A8; ::_thesis: g | the carrier of X = f dom f = the carrier of X by FUNCT_2:def_1 .= the carrier of Y /\ the carrier of X by A6, XBOOLE_1:28 .= (dom g) /\ the carrier of X by FUNCT_2:def_1 ; hence g | the carrier of X = f by A11, FUNCT_1:46; ::_thesis: verum end; theorem :: WAYBEL25:7 for L1, L2 being complete LATTICE for T1 being Scott TopAugmentation of L1 for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic & T1 is injective holds T2 is injective by Th5, Th6; definition let X, Y be non empty TopSpace; redefine pred X is_Retract_of Y means :Def1: :: WAYBEL25:def 1 ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X; compatibility ( X is_Retract_of Y iff ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X ) proof thus ( X is_Retract_of Y implies ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X ) ::_thesis: ( ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X implies X is_Retract_of Y ) proof given f being Function of Y,Y such that A1: f is continuous and A2: f * f = f and A3: Image f,X are_homeomorphic ; :: according to WAYBEL18:def_8 ::_thesis: ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X consider h being Function of (Image f),X such that A4: h is being_homeomorphism by A3, T_0TOPSP:def_1; A5: corestr f is continuous by A1, WAYBEL18:10; h " is continuous by A4, TOPS_2:def_5; then reconsider c = (incl (Image f)) * (h ") as continuous Function of X,Y ; h is continuous by A4, TOPS_2:def_5; then reconsider r = h * (corestr f) as continuous Function of Y,X by A5; take c ; ::_thesis: ex r being continuous Function of Y,X st r * c = id X take r ; ::_thesis: r * c = id X A6: rng h = [#] X by A4, TOPS_2:def_5; A7: h is V7() by A4, TOPS_2:def_5; thus r * c = h * ((corestr f) * ((incl (Image f)) * (h "))) by RELAT_1:36 .= h * (((corestr f) * (incl (Image f))) * (h ")) by RELAT_1:36 .= h * ((id (Image f)) * (h ")) by A2, YELLOW14:35 .= h * (h ") by FUNCT_2:17 .= id X by A6, A7, TOPS_2:52 ; ::_thesis: verum end; given c being continuous Function of X,Y, r being continuous Function of Y,X such that A8: r * c = id X ; ::_thesis: X is_Retract_of Y take f = c * r; :: according to WAYBEL18:def_8 ::_thesis: ( f is continuous & f * f = f & Image f,X are_homeomorphic ) A9: dom c = the carrier of X by FUNCT_2:def_1 .= rng r by A8, FUNCT_2:18 ; then reconsider cf = corestr c as Function of X,(Image f) by RELAT_1:28; A10: Image f = Image c by A9, RELAT_1:28; the carrier of (Image c) c= the carrier of Y by BORSUK_1:1; then id (Image c) is Function of the carrier of (Image c), the carrier of Y by FUNCT_2:7; then reconsider q = r * (id (Image c)) as Function of (Image f),X by A10; A11: [#] X <> {} ; A12: for P being Subset of X st P is open holds q " P is open proof let P be Subset of X; ::_thesis: ( P is open implies q " P is open ) A13: dom (id (Image c)) = [#] (Image c) by FUNCT_2:def_1; A14: (id (Image c)) " (r " P) = (r " P) /\ ([#] (Image c)) proof thus (id (Image c)) " (r " P) c= (r " P) /\ ([#] (Image c)) :: according to XBOOLE_0:def_10 ::_thesis: (r " P) /\ ([#] (Image c)) c= (id (Image c)) " (r " P) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (id (Image c)) " (r " P) or a in (r " P) /\ ([#] (Image c)) ) assume A15: a in (id (Image c)) " (r " P) ; ::_thesis: a in (r " P) /\ ([#] (Image c)) then (id (Image c)) . a in r " P by FUNCT_1:def_7; then a in r " P by A15, FUNCT_1:18; hence a in (r " P) /\ ([#] (Image c)) by A15, XBOOLE_0:def_4; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (r " P) /\ ([#] (Image c)) or a in (id (Image c)) " (r " P) ) assume A16: a in (r " P) /\ ([#] (Image c)) ; ::_thesis: a in (id (Image c)) " (r " P) then a in r " P by XBOOLE_0:def_4; then (id (Image c)) . a in r " P by A16, FUNCT_1:18; hence a in (id (Image c)) " (r " P) by A13, A16, FUNCT_1:def_7; ::_thesis: verum end; assume P is open ; ::_thesis: q " P is open then r " P is open by A11, TOPS_2:43; then A17: r " P in the topology of Y by PRE_TOPC:def_2; q " P = (id (Image c)) " (r " P) by RELAT_1:146; hence q " P in the topology of (Image f) by A10, A17, A14, PRE_TOPC:def_4; :: according to PRE_TOPC:def_2 ::_thesis: verum end; A18: r * (cf * (cf ")) = (id X) * (cf ") by A8, RELAT_1:36; thus f is continuous ; ::_thesis: ( f * f = f & Image f,X are_homeomorphic ) thus f * f = c * (r * (c * r)) by RELAT_1:36 .= c * ((id X) * r) by A8, RELAT_1:36 .= f by FUNCT_2:17 ; ::_thesis: Image f,X are_homeomorphic take h = cf " ; :: according to T_0TOPSP:def_1 ::_thesis: h is being_homeomorphism thus dom h = [#] (Image f) by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng h = [#] X & h is one-to-one & h is continuous & h " is continuous ) A19: rng (corestr c) = [#] (Image c) by FUNCT_2:def_3; A20: c is V7() by A8, FUNCT_2:23; hence rng h = [#] X by A10, A19, TOPS_2:49; ::_thesis: ( h is one-to-one & h is continuous & h " is continuous ) (corestr c) " is one-to-one by A20; hence h is V7() by A10, A20, TOPS_2:def_4; ::_thesis: ( h is continuous & h " is continuous ) corestr c is V7() by A8, FUNCT_2:23; then r * (id the carrier of (Image c)) = (id X) * (cf ") by A10, A19, A18, TOPS_2:52; then r * (id (Image c)) = cf " by FUNCT_2:17; hence h is continuous by A11, A12, TOPS_2:43; ::_thesis: h " is continuous corestr c is continuous by WAYBEL18:10; hence h " is continuous by A10, A19, A20, TOPS_2:51; ::_thesis: verum end; end; :: deftheorem Def1 defines is_Retract_of WAYBEL25:def_1_:_ for X, Y being non empty TopSpace holds ( X is_Retract_of Y iff ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X ); theorem :: WAYBEL25:8 for S, T, X, Y being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) & S is_Retract_of X holds T is_Retract_of Y proof let S, T, X, Y be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) & S is_Retract_of X implies T is_Retract_of Y ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) ; ::_thesis: ( not S is_Retract_of X or T is_Retract_of Y ) given c being continuous Function of S,X, r being continuous Function of X,S such that A3: r * c = id S ; :: according to WAYBEL25:def_1 ::_thesis: T is_Retract_of Y reconsider rr = r as continuous Function of Y,T by A1, A2, YELLOW12:36; reconsider cc = c as continuous Function of T,Y by A1, A2, YELLOW12:36; take cc ; :: according to WAYBEL25:def_1 ::_thesis: ex r being continuous Function of Y,T st r * cc = id T take rr ; ::_thesis: rr * cc = id T thus rr * cc = id T by A1, A3; ::_thesis: verum end; theorem :: WAYBEL25:9 for T, S1, S2 being non empty TopStruct st S1,S2 are_homeomorphic & S1 is_Retract_of T holds S2 is_Retract_of T proof let T, S1, S2 be non empty TopStruct ; ::_thesis: ( S1,S2 are_homeomorphic & S1 is_Retract_of T implies S2 is_Retract_of T ) assume that A1: S1,S2 are_homeomorphic and A2: S1 is_Retract_of T ; ::_thesis: S2 is_Retract_of T consider G being Function of S1,S2 such that A3: G is being_homeomorphism by A1, T_0TOPSP:def_1; consider H being Function of T,T such that A4: H is continuous and A5: H * H = H and A6: Image H,S1 are_homeomorphic by A2, WAYBEL18:def_8; take H ; :: according to WAYBEL18:def_8 ::_thesis: ( H is continuous & H * H = H & Image H,S2 are_homeomorphic ) consider F being Function of (Image H),S1 such that A7: F is being_homeomorphism by A6, T_0TOPSP:def_1; G * F is being_homeomorphism by A3, A7, TOPS_2:57; hence ( H is continuous & H * H = H & Image H,S2 are_homeomorphic ) by A4, A5, T_0TOPSP:def_1; ::_thesis: verum end; theorem :: WAYBEL25:10 for S, T being non empty TopSpace st T is injective & S is_Retract_of T holds S is injective proof let S, T be non empty TopSpace; ::_thesis: ( T is injective & S is_Retract_of T implies S is injective ) assume that A1: T is injective and A2: S is_Retract_of T ; ::_thesis: S is injective consider h being Function of T,T such that A3: h is continuous and A4: h * h = h and A5: Image h,S are_homeomorphic by A2, WAYBEL18:def_8; set F = corestr h; for W being Point of T st W in the carrier of (Image h) holds (corestr h) . W = W proof let W be Point of T; ::_thesis: ( W in the carrier of (Image h) implies (corestr h) . W = W ) assume W in the carrier of (Image h) ; ::_thesis: (corestr h) . W = W then W in rng h by WAYBEL18:9; then ex x being set st ( x in dom h & W = h . x ) by FUNCT_1:def_3; hence (corestr h) . W = W by A4, FUNCT_1:13; ::_thesis: verum end; then A6: corestr h is being_a_retraction by BORSUK_1:def_16; corestr h is continuous by A3, WAYBEL18:10; then Image h is_a_retract_of T by A6, BORSUK_1:def_17; then Image h is injective by A1, WAYBEL18:8; hence S is injective by A5, Th6; ::_thesis: verum end; theorem :: WAYBEL25:11 for J being non empty injective TopSpace for Y being non empty TopSpace st J is SubSpace of Y holds J is_Retract_of Y proof let J be non empty injective TopSpace; ::_thesis: for Y being non empty TopSpace st J is SubSpace of Y holds J is_Retract_of Y let Y be non empty TopSpace; ::_thesis: ( J is SubSpace of Y implies J is_Retract_of Y ) assume A1: J is SubSpace of Y ; ::_thesis: J is_Retract_of Y then consider f being Function of Y,J such that A2: f is continuous and A3: f | the carrier of J = id J by WAYBEL18:def_5; A4: the carrier of J c= the carrier of Y by A1, BORSUK_1:1; then reconsider ff = f as Function of Y,Y by FUNCT_2:7; ex ff being Function of Y,Y st ( ff is continuous & ff * ff = ff & Image ff,J are_homeomorphic ) proof reconsider M = [#] J as non empty Subset of Y by A1, BORSUK_1:1; take ff ; ::_thesis: ( ff is continuous & ff * ff = ff & Image ff,J are_homeomorphic ) thus ff is continuous by A1, A2, PRE_TOPC:26; ::_thesis: ( ff * ff = ff & Image ff,J are_homeomorphic ) A5: dom f = the carrier of Y by FUNCT_2:def_1; A6: for x being set st x in the carrier of Y holds (f * f) . x = f . x proof let x be set ; ::_thesis: ( x in the carrier of Y implies (f * f) . x = f . x ) assume A7: x in the carrier of Y ; ::_thesis: (f * f) . x = f . x hence (f * f) . x = f . (f . x) by A5, FUNCT_1:13 .= (id J) . (f . x) by A3, A7, FUNCT_1:49, FUNCT_2:5 .= f . x by A7, FUNCT_1:18, FUNCT_2:5 ; ::_thesis: verum end; dom (ff * ff) = the carrier of Y by FUNCT_2:def_1; hence ff * ff = ff by A5, A6, FUNCT_1:2; ::_thesis: Image ff,J are_homeomorphic A8: rng f = the carrier of J proof thus rng f c= the carrier of J ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of J c= rng f let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of J or y in rng f ) assume A9: y in the carrier of J ; ::_thesis: y in rng f then y in the carrier of Y by A4; then A10: y in dom f by FUNCT_2:def_1; f . y = (f | the carrier of J) . y by A9, FUNCT_1:49 .= y by A3, A9, FUNCT_1:18 ; hence y in rng f by A10, FUNCT_1:def_3; ::_thesis: verum end; the carrier of (Y | M) = [#] (Y | M) .= the carrier of J by PRE_TOPC:def_5 ; then Image ff = TopStruct(# the carrier of J, the topology of J #) by A1, A8, TSEP_1:5; hence Image ff,J are_homeomorphic by YELLOW14:19; ::_thesis: verum end; hence J is_Retract_of Y by WAYBEL18:def_8; ::_thesis: verum end; theorem Th12: :: WAYBEL25:12 for L being complete continuous LATTICE for T being Scott TopAugmentation of L holds T is injective proof let L be complete continuous LATTICE; ::_thesis: for T being Scott TopAugmentation of L holds T is injective let T be Scott TopAugmentation of L; ::_thesis: T is injective let X be non empty TopSpace; :: according to WAYBEL18:def_5 ::_thesis: for b1 being Element of bool [: the carrier of X, the carrier of T:] holds ( not b1 is continuous or for b2 being TopStruct holds ( not X is SubSpace of b2 or ex b3 being Element of bool [: the carrier of b2, the carrier of T:] st ( b3 is continuous & b3 | the carrier of X = b1 ) ) ) let f be Function of X,T; ::_thesis: ( not f is continuous or for b1 being TopStruct holds ( not X is SubSpace of b1 or ex b2 being Element of bool [: the carrier of b1, the carrier of T:] st ( b2 is continuous & b2 | the carrier of X = f ) ) ) assume A1: f is continuous ; ::_thesis: for b1 being TopStruct holds ( not X is SubSpace of b1 or ex b2 being Element of bool [: the carrier of b1, the carrier of T:] st ( b2 is continuous & b2 | the carrier of X = f ) ) let Y be non empty TopSpace; ::_thesis: ( not X is SubSpace of Y or ex b1 being Element of bool [: the carrier of Y, the carrier of T:] st ( b1 is continuous & b1 | the carrier of X = f ) ) assume A2: X is SubSpace of Y ; ::_thesis: ex b1 being Element of bool [: the carrier of Y, the carrier of T:] st ( b1 is continuous & b1 | the carrier of X = f ) deffunc H1( set ) -> Element of the carrier of T = "\/" ( { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : \$1 in V } ,T); consider g being Function of the carrier of Y, the carrier of T such that A3: for x being Element of Y holds g . x = H1(x) from FUNCT_2:sch_4(); reconsider g = g as Function of Y,T ; take g ; ::_thesis: ( g is continuous & g | the carrier of X = f ) A4: dom f = the carrier of X by FUNCT_2:def_1; A5: for P being Subset of T st P is open holds g " P is open proof let P be Subset of T; ::_thesis: ( P is open implies g " P is open ) assume P is open ; ::_thesis: g " P is open then reconsider P = P as open Subset of T ; for x being set holds ( x in g " P iff ex Q being Subset of Y st ( Q is open & Q c= g " P & x in Q ) ) proof let x be set ; ::_thesis: ( x in g " P iff ex Q being Subset of Y st ( Q is open & Q c= g " P & x in Q ) ) thus ( x in g " P implies ex Q being Subset of Y st ( Q is open & Q c= g " P & x in Q ) ) ::_thesis: ( ex Q being Subset of Y st ( Q is open & Q c= g " P & x in Q ) implies x in g " P ) proof assume A6: x in g " P ; ::_thesis: ex Q being Subset of Y st ( Q is open & Q c= g " P & x in Q ) then reconsider y = x as Point of Y ; set A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } ; { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } c= the carrier of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } or a in the carrier of T ) assume a in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } ; ::_thesis: a in the carrier of T then ex V being open Subset of Y st ( a = inf (f .: (V /\ the carrier of X)) & y in V ) ; hence a in the carrier of T ; ::_thesis: verum end; then reconsider A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } as Subset of T ; A7: inf (f .: (([#] Y) /\ the carrier of X)) in A ; A8: A is directed proof let a, b be Element of T; :: according to WAYBEL_0:def_1 ::_thesis: ( not a in A or not b in A or ex b1 being Element of the carrier of T st ( b1 in A & a <= b1 & b <= b1 ) ) assume a in A ; ::_thesis: ( not b in A or ex b1 being Element of the carrier of T st ( b1 in A & a <= b1 & b <= b1 ) ) then consider Va being open Subset of Y such that A9: a = inf (f .: (Va /\ the carrier of X)) and A10: y in Va ; assume b in A ; ::_thesis: ex b1 being Element of the carrier of T st ( b1 in A & a <= b1 & b <= b1 ) then consider Vb being open Subset of Y such that A11: b = inf (f .: (Vb /\ the carrier of X)) and A12: y in Vb ; take inf (f .: ((Va /\ Vb) /\ the carrier of X)) ; ::_thesis: ( inf (f .: ((Va /\ Vb) /\ the carrier of X)) in A & a <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) & b <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) ) y in Va /\ Vb by A10, A12, XBOOLE_0:def_4; hence inf (f .: ((Va /\ Vb) /\ the carrier of X)) in A ; ::_thesis: ( a <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) & b <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) ) (Va /\ Vb) /\ the carrier of X c= Vb /\ the carrier of X by XBOOLE_1:17, XBOOLE_1:26; then A13: f .: ((Va /\ Vb) /\ the carrier of X) c= f .: (Vb /\ the carrier of X) by RELAT_1:123; (Va /\ Vb) /\ the carrier of X c= Va /\ the carrier of X by XBOOLE_1:17, XBOOLE_1:26; then f .: ((Va /\ Vb) /\ the carrier of X) c= f .: (Va /\ the carrier of X) by RELAT_1:123; hence ( a <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) & b <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) ) by A9, A11, A13, WAYBEL_7:1; ::_thesis: verum end; A14: g . y = sup A by A3; g . y in P by A6, FUNCT_2:38; then A meets P by A14, A7, A8, WAYBEL11:def_1; then consider b being set such that A15: b in A and A16: b in P by XBOOLE_0:3; consider B being open Subset of Y such that A17: b = inf (f .: (B /\ the carrier of X)) and A18: y in B by A15; reconsider b = b as Element of T by A17; take B ; ::_thesis: ( B is open & B c= g " P & x in B ) thus B is open ; ::_thesis: ( B c= g " P & x in B ) thus B c= g " P ::_thesis: x in B proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in g " P ) assume A19: a in B ; ::_thesis: a in g " P then reconsider a = a as Point of Y ; A20: g . a = H1(a) by A3; b in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : a in V } by A17, A19; then b <= g . a by A20, YELLOW_2:22; then g . a in P by A16, WAYBEL_0:def_20; hence a in g " P by FUNCT_2:38; ::_thesis: verum end; thus x in B by A18; ::_thesis: verum end; thus ( ex Q being Subset of Y st ( Q is open & Q c= g " P & x in Q ) implies x in g " P ) ; ::_thesis: verum end; hence g " P is open by TOPS_1:25; ::_thesis: verum end; set gX = g | the carrier of X; A21: the carrier of X c= the carrier of Y by A2, BORSUK_1:1; A22: for a being set st a in the carrier of X holds (g | the carrier of X) . a = f . a proof let a be set ; ::_thesis: ( a in the carrier of X implies (g | the carrier of X) . a = f . a ) assume A23: a in the carrier of X ; ::_thesis: (g | the carrier of X) . a = f . a then reconsider x = a as Point of X ; reconsider y = x as Point of Y by A21, A23; set A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } ; { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } c= the carrier of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } or a in the carrier of T ) assume a in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } ; ::_thesis: a in the carrier of T then ex V being open Subset of Y st ( a = inf (f .: (V /\ the carrier of X)) & y in V ) ; hence a in the carrier of T ; ::_thesis: verum end; then reconsider A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } as Subset of T ; A24: f . x is_>=_than A proof let z be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not z in A or z <= f . x ) assume z in A ; ::_thesis: z <= f . x then consider V being open Subset of Y such that A25: z = inf (f .: (V /\ the carrier of X)) and A26: y in V ; A27: ex_inf_of f .: (V /\ the carrier of X),T by YELLOW_0:17; y in V /\ the carrier of X by A26, XBOOLE_0:def_4; hence z <= f . x by A25, A27, FUNCT_2:35, YELLOW_4:2; ::_thesis: verum end; A28: for b being Element of T st b is_>=_than A holds f . x <= b proof let b be Element of T; ::_thesis: ( b is_>=_than A implies f . x <= b ) assume A29: for k being Element of T st k in A holds k <= b ; :: according to LATTICE3:def_9 ::_thesis: f . x <= b A30: for V being open Subset of X st x in V holds inf (f .: V) <= b proof let V be open Subset of X; ::_thesis: ( x in V implies inf (f .: V) <= b ) V in the topology of X by PRE_TOPC:def_2; then consider Q being Subset of Y such that A31: Q in the topology of Y and A32: V = Q /\ ([#] X) by A2, PRE_TOPC:def_4; reconsider Q = Q as open Subset of Y by A31, PRE_TOPC:def_2; assume x in V ; ::_thesis: inf (f .: V) <= b then y in Q by A32, XBOOLE_0:def_4; then inf (f .: (Q /\ the carrier of X)) in A ; hence inf (f .: V) <= b by A29, A32; ::_thesis: verum end; A33: b is_>=_than waybelow (f . x) proof let w be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not w in waybelow (f . x) or w <= b ) A34: wayabove w is open by WAYBEL11:36; A35: ex_inf_of f .: (f " (wayabove w)),T by YELLOW_0:17; A36: w <= inf (wayabove w) by WAYBEL14:9; ex_inf_of wayabove w,T by YELLOW_0:17; then inf (wayabove w) <= inf (f .: (f " (wayabove w))) by A35, FUNCT_1:75, YELLOW_0:35; then A37: w <= inf (f .: (f " (wayabove w))) by A36, ORDERS_2:3; assume w in waybelow (f . x) ; ::_thesis: w <= b then w << f . x by WAYBEL_3:7; then f . x in wayabove w by WAYBEL_3:8; then A38: x in f " (wayabove w) by FUNCT_2:38; [#] T <> {} ; then f " (wayabove w) is open by A1, A34, TOPS_2:43; then inf (f .: (f " (wayabove w))) <= b by A30, A38; hence w <= b by A37, ORDERS_2:3; ::_thesis: verum end; f . x = sup (waybelow (f . x)) by WAYBEL_3:def_5; hence f . x <= b by A33, YELLOW_0:32; ::_thesis: verum end; thus (g | the carrier of X) . a = g . y by FUNCT_1:49 .= H1(y) by A3 .= f . a by A24, A28, YELLOW_0:30 ; ::_thesis: verum end; [#] T <> {} ; hence g is continuous by A5, TOPS_2:43; ::_thesis: g | the carrier of X = f dom (g | the carrier of X) = (dom g) /\ the carrier of X by RELAT_1:61 .= the carrier of Y /\ the carrier of X by FUNCT_2:def_1 .= the carrier of X by A2, BORSUK_1:1, XBOOLE_1:28 ; hence g | the carrier of X = f by A4, A22, FUNCT_1:2; ::_thesis: verum end; registration let L be complete continuous LATTICE; cluster Scott -> injective for TopAugmentation of L; coherence for b1 being TopAugmentation of L st b1 is Scott holds b1 is injective by Th12; end; registration let T be non empty injective TopSpace; cluster TopStruct(# the carrier of T, the topology of T #) -> injective ; coherence TopStruct(# the carrier of T, the topology of T #) is injective by WAYBEL18:16; end; begin definition let T be TopStruct ; func Omega T -> strict TopRelStr means :Def2: :: WAYBEL25:def 2 ( TopStruct(# the carrier of it, the topology of it #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of it holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) ) ); existence ex b1 being strict TopRelStr st ( TopStruct(# the carrier of b1, the topology of b1 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b1 holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) ) ) proof defpred S1[ set , set ] means ex Y being Subset of T st ( Y = {\$2} & \$1 in Cl Y ); consider R being Relation of the carrier of T such that A1: for x, y being set holds ( [x,y] in R iff ( x in the carrier of T & y in the carrier of T & S1[x,y] ) ) from RELSET_1:sch_1(); take G = TopRelStr(# the carrier of T,R, the topology of T #); ::_thesis: ( TopStruct(# the carrier of G, the topology of G #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of G holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) ) ) thus TopStruct(# the carrier of G, the topology of G #) = TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: for x, y being Element of G holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) thus for x, y being Element of G holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) ::_thesis: verum proof let x, y be Element of G; ::_thesis: ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) hereby ::_thesis: ( ex Y being Subset of T st ( Y = {y} & x in Cl Y ) implies x <= y ) assume x <= y ; ::_thesis: ex Y being Subset of T st ( Y = {y} & x in Cl Y ) then [x,y] in R by ORDERS_2:def_5; hence ex Y being Subset of T st ( Y = {y} & x in Cl Y ) by A1; ::_thesis: verum end; given Y being Subset of T such that A2: Y = {y} and A3: x in Cl Y ; ::_thesis: x <= y [x,y] in R by A1, A2, A3; hence x <= y by ORDERS_2:def_5; ::_thesis: verum end; end; uniqueness for b1, b2 being strict TopRelStr st TopStruct(# the carrier of b1, the topology of b1 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b1 holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) ) & TopStruct(# the carrier of b2, the topology of b2 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b2 holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) ) holds b1 = b2 proof let R1, R2 be strict TopRelStr ; ::_thesis: ( TopStruct(# the carrier of R1, the topology of R1 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of R1 holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) ) & TopStruct(# the carrier of R2, the topology of R2 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of R2 holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) ) implies R1 = R2 ) assume that A4: TopStruct(# the carrier of R1, the topology of R1 #) = TopStruct(# the carrier of T, the topology of T #) and A5: for x, y being Element of R1 holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) and A6: TopStruct(# the carrier of R2, the topology of R2 #) = TopStruct(# the carrier of T, the topology of T #) and A7: for x, y being Element of R2 holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) ; ::_thesis: R1 = R2 the InternalRel of R1 = the InternalRel of R2 proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of R1 or [x,y] in the InternalRel of R2 ) & ( not [x,y] in the InternalRel of R2 or [x,y] in the InternalRel of R1 ) ) hereby ::_thesis: ( not [x,y] in the InternalRel of R2 or [x,y] in the InternalRel of R1 ) assume A8: [x,y] in the InternalRel of R1 ; ::_thesis: [x,y] in the InternalRel of R2 then reconsider x1 = x, y1 = y as Element of R1 by ZFMISC_1:87; reconsider x2 = x, y2 = y as Element of R2 by A4, A6, A8, ZFMISC_1:87; x1 <= y1 by A8, ORDERS_2:def_5; then ex Y being Subset of T st ( Y = {y1} & x1 in Cl Y ) by A5; then x2 <= y2 by A7; hence [x,y] in the InternalRel of R2 by ORDERS_2:def_5; ::_thesis: verum end; assume A9: [x,y] in the InternalRel of R2 ; ::_thesis: [x,y] in the InternalRel of R1 then reconsider x2 = x, y2 = y as Element of R2 by ZFMISC_1:87; reconsider x1 = x, y1 = y as Element of R1 by A4, A6, A9, ZFMISC_1:87; x2 <= y2 by A9, ORDERS_2:def_5; then ex Y being Subset of T st ( Y = {y2} & x2 in Cl Y ) by A7; then x1 <= y1 by A5; hence [x,y] in the InternalRel of R1 by ORDERS_2:def_5; ::_thesis: verum end; hence R1 = R2 by A4, A6; ::_thesis: verum end; end; :: deftheorem Def2 defines Omega WAYBEL25:def_2_:_ for T being TopStruct for b2 being strict TopRelStr holds ( b2 = Omega T iff ( TopStruct(# the carrier of b2, the topology of b2 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b2 holds ( x <= y iff ex Y being Subset of T st ( Y = {y} & x in Cl Y ) ) ) ) ); Lm1: for T being TopStruct holds the carrier of T = the carrier of (Omega T) proof let T be TopStruct ; ::_thesis: the carrier of T = the carrier of (Omega T) TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2; hence the carrier of T = the carrier of (Omega T) ; ::_thesis: verum end; registration let T be empty TopStruct ; cluster Omega T -> empty strict ; coherence Omega T is empty proof the carrier of (Omega T) = the carrier of T by Lm1; hence the carrier of (Omega T) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; registration let T be non empty TopStruct ; cluster Omega T -> non empty strict ; coherence not Omega T is empty proof the carrier of (Omega T) = the carrier of T by Lm1; hence not the carrier of (Omega T) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; registration let T be TopSpace; cluster Omega T -> TopSpace-like strict ; coherence Omega T is TopSpace-like proof A1: TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) = TopStruct(# the carrier of T, the topology of T #) by Def2; hence the carrier of (Omega T) in the topology of (Omega T) by PRE_TOPC:def_1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of (Omega T)) holds ( not b1 c= the topology of (Omega T) or K252( the carrier of (Omega T),b1) in the topology of (Omega T) ) ) & ( for b1, b2 being Element of bool the carrier of (Omega T) holds ( not b1 in the topology of (Omega T) or not b2 in the topology of (Omega T) or b1 /\ b2 in the topology of (Omega T) ) ) ) thus ( ( for b1 being Element of bool (bool the carrier of (Omega T)) holds ( not b1 c= the topology of (Omega T) or K252( the carrier of (Omega T),b1) in the topology of (Omega T) ) ) & ( for b1, b2 being Element of bool the carrier of (Omega T) holds ( not b1 in the topology of (Omega T) or not b2 in the topology of (Omega T) or b1 /\ b2 in the topology of (Omega T) ) ) ) by A1, PRE_TOPC:def_1; ::_thesis: verum end; end; registration let T be TopStruct ; cluster Omega T -> reflexive strict ; coherence Omega T is reflexive proof let x be set ; :: according to ORDERS_2:def_2,RELAT_2:def_1 ::_thesis: ( not x in the carrier of (Omega T) or [x,x] in the InternalRel of (Omega T) ) assume A1: x in the carrier of (Omega T) ; ::_thesis: [x,x] in the InternalRel of (Omega T) then reconsider T9 = T as non empty TopStruct ; reconsider a = x as Element of (Omega T) by A1; reconsider t9 = x as Element of T9 by A1, Lm1; consider Y being Subset of T such that A2: Y = {t9} ; A3: Y c= Cl Y by PRE_TOPC:18; a in Y by A2, TARSKI:def_1; then a <= a by A2, A3, Def2; hence [x,x] in the InternalRel of (Omega T) by ORDERS_2:def_5; ::_thesis: verum end; end; Lm2: for T being TopStruct for x, y being Element of T for X, Y being Subset of T st X = {x} & Y = {y} holds ( x in Cl Y iff Cl X c= Cl Y ) proof let T be TopStruct ; ::_thesis: for x, y being Element of T for X, Y being Subset of T st X = {x} & Y = {y} holds ( x in Cl Y iff Cl X c= Cl Y ) let x, y be Element of T; ::_thesis: for X, Y being Subset of T st X = {x} & Y = {y} holds ( x in Cl Y iff Cl X c= Cl Y ) let X, Y be Subset of T; ::_thesis: ( X = {x} & Y = {y} implies ( x in Cl Y iff Cl X c= Cl Y ) ) assume that A1: X = {x} and A2: Y = {y} ; ::_thesis: ( x in Cl Y iff Cl X c= Cl Y ) hereby ::_thesis: ( Cl X c= Cl Y implies x in Cl Y ) assume x in Cl Y ; ::_thesis: Cl X c= Cl Y then for V being Subset of T st V is open & x in V holds y in V by A2, YELLOW14:21; hence Cl X c= Cl Y by A1, A2, YELLOW14:22; ::_thesis: verum end; assume Cl X c= Cl Y ; ::_thesis: x in Cl Y hence x in Cl Y by A1, YELLOW14:20; ::_thesis: verum end; registration let T be TopStruct ; cluster Omega T -> transitive strict ; coherence Omega T is transitive proof let x, y, z be set ; :: according to ORDERS_2:def_3,RELAT_2:def_8 ::_thesis: ( not x in the carrier of (Omega T) or not y in the carrier of (Omega T) or not z in the carrier of (Omega T) or not [x,y] in the InternalRel of (Omega T) or not [y,z] in the InternalRel of (Omega T) or [x,z] in the InternalRel of (Omega T) ) assume that A1: x in the carrier of (Omega T) and A2: y in the carrier of (Omega T) and A3: z in the carrier of (Omega T) and A4: [x,y] in the InternalRel of (Omega T) and A5: [y,z] in the InternalRel of (Omega T) ; ::_thesis: [x,z] in the InternalRel of (Omega T) reconsider a = x, b = y, c = z as Element of (Omega T) by A1, A2, A3; a <= b by A4, ORDERS_2:def_5; then consider Y2 being Subset of T such that A6: Y2 = {b} and A7: a in Cl Y2 by Def2; TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) = TopStruct(# the carrier of T, the topology of T #) by Def2; then reconsider t3 = z as Element of T by A3; b <= c by A5, ORDERS_2:def_5; then consider Y3 being Subset of T such that A8: Y3 = {c} and A9: b in Cl Y3 by Def2; Y3 = {t3} by A8; then Cl Y2 c= Cl Y3 by A6, A9, Lm2; then a <= c by A7, A8, Def2; hence [x,z] in the InternalRel of (Omega T) by ORDERS_2:def_5; ::_thesis: verum end; end; registration let T be T_0-TopSpace; cluster Omega T -> antisymmetric strict ; coherence Omega T is antisymmetric proof let x, y be set ; :: according to ORDERS_2:def_4,RELAT_2:def_4 ::_thesis: ( not x in the carrier of (Omega T) or not y in the carrier of (Omega T) or not [x,y] in the InternalRel of (Omega T) or not [y,x] in the InternalRel of (Omega T) or x = y ) assume that A1: x in the carrier of (Omega T) and A2: y in the carrier of (Omega T) and A3: [x,y] in the InternalRel of (Omega T) and A4: [y,x] in the InternalRel of (Omega T) ; ::_thesis: x = y reconsider a = x, b = y as Element of (Omega T) by A1, A2; b <= a by A4, ORDERS_2:def_5; then A5: ex Y1 being Subset of T st ( Y1 = {a} & b in Cl Y1 ) by Def2; TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) = TopStruct(# the carrier of T, the topology of T #) by Def2; then reconsider t1 = x, t2 = y as Element of T by A1, A2; a <= b by A3, ORDERS_2:def_5; then ex Y2 being Subset of T st ( Y2 = {b} & a in Cl Y2 ) by Def2; then for V being Subset of T holds ( not V is open or ( ( t1 in V implies t2 in V ) & ( t2 in V implies t1 in V ) ) ) by A5, YELLOW14:21; hence x = y by T_0TOPSP:def_7; ::_thesis: verum end; end; theorem Th13: :: WAYBEL25:13 for S, T being TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds Omega S = Omega T proof let S, T be TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) implies Omega S = Omega T ) assume A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: Omega S = Omega T A2: TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) = TopStruct(# the carrier of S, the topology of S #) by Def2 .= TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by A1, Def2 ; the InternalRel of (Omega S) = the InternalRel of (Omega T) proof let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in the InternalRel of (Omega S) or [a,b] in the InternalRel of (Omega T) ) & ( not [a,b] in the InternalRel of (Omega T) or [a,b] in the InternalRel of (Omega S) ) ) thus ( [a,b] in the InternalRel of (Omega S) implies [a,b] in the InternalRel of (Omega T) ) ::_thesis: ( not [a,b] in the InternalRel of (Omega T) or [a,b] in the InternalRel of (Omega S) ) proof assume A3: [a,b] in the InternalRel of (Omega S) ; ::_thesis: [a,b] in the InternalRel of (Omega T) then reconsider s1 = a, s2 = b as Element of (Omega S) by ZFMISC_1:87; reconsider t1 = s1, t2 = s2 as Element of (Omega T) by A2; s1 <= s2 by A3, ORDERS_2:def_5; then consider Y being Subset of S such that A4: Y = {s2} and A5: s1 in Cl Y by Def2; reconsider Z = Y as Subset of T by A1; t1 in Cl Z by A1, A5, TOPS_3:80; then t1 <= t2 by A4, Def2; hence [a,b] in the InternalRel of (Omega T) by ORDERS_2:def_5; ::_thesis: verum end; assume A6: [a,b] in the InternalRel of (Omega T) ; ::_thesis: [a,b] in the InternalRel of (Omega S) then reconsider s1 = a, s2 = b as Element of (Omega T) by ZFMISC_1:87; reconsider t1 = s1, t2 = s2 as Element of (Omega S) by A2; s1 <= s2 by A6, ORDERS_2:def_5; then consider Y being Subset of T such that A7: Y = {s2} and A8: s1 in Cl Y by Def2; reconsider Z = Y as Subset of S by A1; t1 in Cl Z by A1, A8, TOPS_3:80; then t1 <= t2 by A7, Def2; hence [a,b] in the InternalRel of (Omega S) by ORDERS_2:def_5; ::_thesis: verum end; hence Omega S = Omega T by A2; ::_thesis: verum end; theorem :: WAYBEL25:14 for M being non empty set for T being non empty TopSpace holds RelStr(# the carrier of (Omega (product (M --> T))), the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))), the InternalRel of (product (M --> (Omega T))) #) proof let M be non empty set ; ::_thesis: for T being non empty TopSpace holds RelStr(# the carrier of (Omega (product (M --> T))), the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))), the InternalRel of (product (M --> (Omega T))) #) let T be non empty TopSpace; ::_thesis: RelStr(# the carrier of (Omega (product (M --> T))), the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))), the InternalRel of (product (M --> (Omega T))) #) A1: dom (Carrier (M --> T)) = M by PARTFUN1:def_2 .= dom (Carrier (M --> (Omega T))) by PARTFUN1:def_2 ; A2: for i being set st i in dom (Carrier (M --> T)) holds (Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i proof let i be set ; ::_thesis: ( i in dom (Carrier (M --> T)) implies (Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i ) assume i in dom (Carrier (M --> T)) ; ::_thesis: (Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i then A3: i in M ; then consider R1 being 1-sorted such that A4: R1 = (M --> T) . i and A5: (Carrier (M --> T)) . i = the carrier of R1 by PRALG_1:def_13; consider R2 being 1-sorted such that A6: R2 = (M --> (Omega T)) . i and A7: (Carrier (M --> (Omega T))) . i = the carrier of R2 by A3, PRALG_1:def_13; the carrier of R1 = the carrier of T by A3, A4, FUNCOP_1:7 .= the carrier of (Omega T) by Lm1 .= the carrier of R2 by A3, A6, FUNCOP_1:7 ; hence (Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i by A5, A7; ::_thesis: verum end; A8: the carrier of (Omega (product (M --> T))) = the carrier of (product (M --> T)) by Lm1 .= product (Carrier (M --> T)) by WAYBEL18:def_3 .= product (Carrier (M --> (Omega T))) by A1, A2, FUNCT_1:2 ; A9: the carrier of (Omega (product (M --> T))) = the carrier of (product (M --> T)) by Lm1; the InternalRel of (Omega (product (M --> T))) = the InternalRel of (product (M --> (Omega T))) proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of (Omega (product (M --> T))) or [x,y] in the InternalRel of (product (M --> (Omega T))) ) & ( not [x,y] in the InternalRel of (product (M --> (Omega T))) or [x,y] in the InternalRel of (Omega (product (M --> T))) ) ) hereby ::_thesis: ( not [x,y] in the InternalRel of (product (M --> (Omega T))) or [x,y] in the InternalRel of (Omega (product (M --> T))) ) assume A10: [x,y] in the InternalRel of (Omega (product (M --> T))) ; ::_thesis: [x,y] in the InternalRel of (product (M --> (Omega T))) then A11: y in the carrier of (Omega (product (M --> T))) by ZFMISC_1:87; A12: x in the carrier of (Omega (product (M --> T))) by A10, ZFMISC_1:87; then reconsider xp = x, yp = y as Element of (product (M --> (Omega T))) by A8, A11, YELLOW_1:def_4; reconsider p1 = x, p2 = y as Element of (product (M --> T)) by A12, A11, Lm1; reconsider xo = x, yo = y as Element of (Omega (product (M --> T))) by A10, ZFMISC_1:87; A13: xp in product (Carrier (M --> (Omega T))) by A8, A10, ZFMISC_1:87; then consider f being Function such that A14: xp = f and dom f = dom (Carrier (M --> (Omega T))) and for i being set st i in dom (Carrier (M --> (Omega T))) holds f . i in (Carrier (M --> (Omega T))) . i by CARD_3:def_5; yp in product (Carrier (M --> (Omega T))) by A8, A10, ZFMISC_1:87; then consider g being Function such that A15: yp = g and dom g = dom (Carrier (M --> (Omega T))) and for i being set st i in dom (Carrier (M --> (Omega T))) holds g . i in (Carrier (M --> (Omega T))) . i by CARD_3:def_5; xo <= yo by A10, ORDERS_2:def_5; then A16: ex Yp being Subset of (product (M --> T)) st ( Yp = {p2} & p1 in Cl Yp ) by Def2; for i being set st i in M holds ex R being RelStr ex xi, yi being Element of R st ( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi ) proof let i be set ; ::_thesis: ( i in M implies ex R being RelStr ex xi, yi being Element of R st ( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi ) ) assume A17: i in M ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st ( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi ) then reconsider j = i as Element of M ; set t1 = p1 . j; set t2 = p2 . j; reconsider xi = p1 . j, yi = p2 . j as Element of (Omega T) by Lm1; take Omega T ; ::_thesis: ex xi, yi being Element of (Omega T) st ( Omega T = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi ) take xi ; ::_thesis: ex yi being Element of (Omega T) st ( Omega T = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi ) take yi ; ::_thesis: ( Omega T = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi ) thus Omega T = (M --> (Omega T)) . i by A17, FUNCOP_1:7; ::_thesis: ( xi = f . i & yi = g . i & xi <= yi ) thus xi = f . i by A14; ::_thesis: ( yi = g . i & xi <= yi ) thus yi = g . i by A15; ::_thesis: xi <= yi p1 . j in Cl {(p2 . j)} by A16, YELLOW14:30; hence xi <= yi by Def2; ::_thesis: verum end; then xp <= yp by A13, A14, A15, YELLOW_1:def_4; hence [x,y] in the InternalRel of (product (M --> (Omega T))) by ORDERS_2:def_5; ::_thesis: verum end; assume A18: [x,y] in the InternalRel of (product (M --> (Omega T))) ; ::_thesis: [x,y] in the InternalRel of (Omega (product (M --> T))) then reconsider xp = x, yp = y as Element of (product (M --> (Omega T))) by ZFMISC_1:87; A19: xp <= yp by A18, ORDERS_2:def_5; A20: x in the carrier of (product (M --> (Omega T))) by A18, ZFMISC_1:87; then xp in product (Carrier (M --> (Omega T))) by YELLOW_1:def_4; then consider f, g being Function such that A21: f = xp and A22: g = yp and A23: for i being set st i in M holds ex R being RelStr ex xi, yi being Element of R st ( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi ) by A19, YELLOW_1:def_4; A24: y in the carrier of (product (M --> (Omega T))) by A18, ZFMISC_1:87; then reconsider xo = x, yo = y as Element of (Omega (product (M --> T))) by A8, A20, YELLOW_1:def_4; reconsider p1 = x, p2 = y as Element of (product (M --> T)) by A8, A9, A20, A24, YELLOW_1:def_4; for i being Element of M holds p1 . i in Cl {(p2 . i)} proof let i be Element of M; ::_thesis: p1 . i in Cl {(p2 . i)} consider R1 being RelStr , xi, yi being Element of R1 such that A25: R1 = (M --> (Omega T)) . i and A26: xi = f . i and A27: yi = g . i and A28: xi <= yi by A23; reconsider xi = xi, yi = yi as Element of (Omega T) by A25, FUNCOP_1:7; xi <= yi by A25, A28, FUNCOP_1:7; then ex Y being Subset of T st ( Y = {yi} & xi in Cl Y ) by Def2; hence p1 . i in Cl {(p2 . i)} by A21, A22, A26, A27; ::_thesis: verum end; then p1 in Cl {p2} by YELLOW14:30; then xo <= yo by Def2; hence [x,y] in the InternalRel of (Omega (product (M --> T))) by ORDERS_2:def_5; ::_thesis: verum end; hence RelStr(# the carrier of (Omega (product (M --> T))), the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))), the InternalRel of (product (M --> (Omega T))) #) by A8, YELLOW_1:def_4; ::_thesis: verum end; theorem Th15: :: WAYBEL25:15 for S being complete Scott TopLattice holds Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) proof let S be complete Scott TopLattice; ::_thesis: Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) A1: TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) = TopStruct(# the carrier of S, the topology of S #) by Def2; the InternalRel of (Omega S) = the InternalRel of S proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of (Omega S) or [x,y] in the InternalRel of S ) & ( not [x,y] in the InternalRel of S or [x,y] in the InternalRel of (Omega S) ) ) hereby ::_thesis: ( not [x,y] in the InternalRel of S or [x,y] in the InternalRel of (Omega S) ) assume A2: [x,y] in the InternalRel of (Omega S) ; ::_thesis: [x,y] in the InternalRel of S then A3: y in the carrier of (Omega S) by ZFMISC_1:87; x in the carrier of (Omega S) by A2, ZFMISC_1:87; then reconsider t1 = x, t2 = y as Element of S by A3, Lm1; reconsider o1 = x, o2 = y as Element of (Omega S) by A2, ZFMISC_1:87; o1 <= o2 by A2, ORDERS_2:def_5; then ex Y2 being Subset of S st ( Y2 = {o2} & o1 in Cl Y2 ) by Def2; then t1 in downarrow t2 by WAYBEL11:9; then ex t3 being Element of S st ( t3 >= t1 & t3 in {t2} ) by WAYBEL_0:def_15; then t1 <= t2 by TARSKI:def_1; hence [x,y] in the InternalRel of S by ORDERS_2:def_5; ::_thesis: verum end; assume A4: [x,y] in the InternalRel of S ; ::_thesis: [x,y] in the InternalRel of (Omega S) then reconsider t1 = x, t2 = y as Element of S by ZFMISC_1:87; reconsider o1 = x, o2 = y as Element of (Omega S) by A1, A4, ZFMISC_1:87; A5: t2 in {t2} by TARSKI:def_1; t1 <= t2 by A4, ORDERS_2:def_5; then t1 in downarrow t2 by A5, WAYBEL_0:def_15; then t1 in Cl {t2} by WAYBEL11:9; then o1 <= o2 by Def2; hence [x,y] in the InternalRel of (Omega S) by ORDERS_2:def_5; ::_thesis: verum end; hence Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) by A1; ::_thesis: verum end; theorem Th16: :: WAYBEL25:16 for L being complete LATTICE for S being Scott TopAugmentation of L holds RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of L, the InternalRel of L #) proof let L be complete LATTICE; ::_thesis: for S being Scott TopAugmentation of L holds RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of L, the InternalRel of L #) let S be Scott TopAugmentation of L; ::_thesis: RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of L, the InternalRel of L #) TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) = Omega S by Th15; hence RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4; ::_thesis: verum end; registration let S be complete Scott TopLattice; cluster Omega S -> complete strict ; coherence Omega S is complete proof set T = the Scott TopAugmentation of S; A1: RelStr(# the carrier of (Omega the Scott TopAugmentation of S), the InternalRel of (Omega the Scott TopAugmentation of S) #) = RelStr(# the carrier of S, the InternalRel of S #) by Th16; the topology of S = sigma S by WAYBEL14:23 .= the topology of the Scott TopAugmentation of S by YELLOW_9:51 ; then TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of the Scott TopAugmentation of S, the topology of the Scott TopAugmentation of S #) by A1, Lm1; then Omega S = Omega the Scott TopAugmentation of S by Th13; hence Omega S is complete by A1, YELLOW_0:3; ::_thesis: verum end; end; theorem Th17: :: WAYBEL25:17 for T being non empty TopSpace for S being non empty SubSpace of T holds Omega S is full SubRelStr of Omega T proof let T be non empty TopSpace; ::_thesis: for S being non empty SubSpace of T holds Omega S is full SubRelStr of Omega T let S be non empty SubSpace of T; ::_thesis: Omega S is full SubRelStr of Omega T A1: the carrier of S c= the carrier of T by BORSUK_1:1; A2: the carrier of (Omega S) = the carrier of S by Lm1; A3: the InternalRel of (Omega S) c= the InternalRel of (Omega T) proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the InternalRel of (Omega S) or [x,y] in the InternalRel of (Omega T) ) assume A4: [x,y] in the InternalRel of (Omega S) ; ::_thesis: [x,y] in the InternalRel of (Omega T) then reconsider o1 = x, o2 = y as Element of (Omega S) by ZFMISC_1:87; A5: y in the carrier of (Omega S) by A4, ZFMISC_1:87; then reconsider s2 = y as Element of S by Lm1; x in the carrier of (Omega S) by A4, ZFMISC_1:87; then reconsider o3 = x, o4 = y as Element of (Omega T) by A1, A2, A5, Lm1; reconsider t2 = y as Element of T by A1, A2, A5; Cl {s2} = (Cl {t2}) /\ ([#] S) by PRE_TOPC:17; then A6: Cl {s2} c= Cl {t2} by XBOOLE_1:17; o1 <= o2 by A4, ORDERS_2:def_5; then ex Y2 being Subset of S st ( Y2 = {o2} & o1 in Cl Y2 ) by Def2; then o3 <= o4 by A6, Def2; hence [x,y] in the InternalRel of (Omega T) by ORDERS_2:def_5; ::_thesis: verum end; A7: the InternalRel of (Omega S) = the InternalRel of (Omega T) |_2 the carrier of (Omega S) proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of (Omega S) or [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) ) & ( not [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) or [x,y] in the InternalRel of (Omega S) ) ) thus ( [x,y] in the InternalRel of (Omega S) implies [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) ) by A3, XBOOLE_0:def_4; ::_thesis: ( not [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) or [x,y] in the InternalRel of (Omega S) ) assume A8: [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) ; ::_thesis: [x,y] in the InternalRel of (Omega S) then A9: y in the carrier of (Omega S) by ZFMISC_1:87; A10: x in the carrier of (Omega S) by A8, ZFMISC_1:87; then reconsider t1 = x, t2 = y as Element of T by A1, A2, A9; reconsider o1 = x, o2 = y as Element of (Omega T) by A1, A2, A10, A9, Lm1; [x,y] in the InternalRel of (Omega T) by A8, XBOOLE_0:def_4; then o1 <= o2 by ORDERS_2:def_5; then A11: ex Y being Subset of T st ( Y = {t2} & t1 in Cl Y ) by Def2; reconsider s1 = x, s2 = y as Element of S by A10, A9, Lm1; reconsider o3 = x, o4 = y as Element of (Omega S) by A8, ZFMISC_1:87; Cl {s2} = (Cl {t2}) /\ ([#] S) by PRE_TOPC:17; then s1 in Cl {s2} by A11, XBOOLE_0:def_4; then o3 <= o4 by Def2; hence [x,y] in the InternalRel of (Omega S) by ORDERS_2:def_5; ::_thesis: verum end; the carrier of (Omega S) c= the carrier of (Omega T) by A1, A2, Lm1; hence Omega S is full SubRelStr of Omega T by A3, A7, YELLOW_0:def_13, YELLOW_0:def_14; ::_thesis: verum end; theorem Th18: :: WAYBEL25:18 for S, T being TopSpace for h being Function of S,T for g being Function of (Omega S),(Omega T) st h = g & h is being_homeomorphism holds g is isomorphic proof let S, T be TopSpace; ::_thesis: for h being Function of S,T for g being Function of (Omega S),(Omega T) st h = g & h is being_homeomorphism holds g is isomorphic let h be Function of S,T; ::_thesis: for g being Function of (Omega S),(Omega T) st h = g & h is being_homeomorphism holds g is isomorphic let g be Function of (Omega S),(Omega T); ::_thesis: ( h = g & h is being_homeomorphism implies g is isomorphic ) assume that A1: h = g and A2: h is being_homeomorphism ; ::_thesis: g is isomorphic A3: dom h = [#] S by A2, TOPS_2:def_5; A4: rng h = [#] T by A2, TOPS_2:def_5; A5: the carrier of T = the carrier of (Omega T) by Lm1; A6: the carrier of S = the carrier of (Omega S) by Lm1; A7: h is one-to-one by A2, TOPS_2:def_5; percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ; supposeA8: ( not S is empty & not T is empty ) ; ::_thesis: g is isomorphic then reconsider s = S, t = T as non empty TopSpace ; reconsider f = g as Function of (Omega s),(Omega t) ; for x, y being Element of (Omega s) holds ( x <= y iff f . x <= f . y ) proof let x, y be Element of (Omega s); ::_thesis: ( x <= y iff f . x <= f . y ) A9: dom f = [#] S by A1, A2, TOPS_2:def_5 .= the carrier of S ; reconsider Z = {((f ") . (f . y))} as Subset of s by Lm1; A10: h " is being_homeomorphism by A2, A8, TOPS_2:56; A11: f is onto by A1, A4, A5, FUNCT_2:def_3; then A12: f " = f " by A1, A7, TOPS_2:def_4; A13: dom h = the carrier of (Omega s) by A3, Lm1; then A14: y = (h ") . (h . y) by A7, FUNCT_1:34 .= (f ") . (f . y) by A11, A1, A7, TOPS_2:def_4 ; hereby ::_thesis: ( f . x <= f . y implies x <= y ) reconsider Z = {(f . y)} as Subset of t by Lm1; assume x <= y ; ::_thesis: f . x <= f . y then consider Y being Subset of s such that A15: Y = {y} and A16: x in Cl Y by Def2; A17: Im (h,y) = Z by A1, A13, FUNCT_1:59; f . x in f .: (Cl Y) by A16, FUNCT_2:35; then h . x in Cl (h .: Y) by A1, A2, TOPS_2:60; hence f . x <= f . y by A1, A15, A17, Def2; ::_thesis: verum end; assume f . x <= f . y ; ::_thesis: x <= y then consider Y being Subset of t such that A18: Y = {(f . y)} and A19: f . x in Cl Y by Def2; A20: f " = h " by A1, A5, A6; A21: x = (f ") . (f . x) by A1, A7, A12, A13, FUNCT_1:34; (f ") . (f . x) in (f ") .: (Cl Y) by A19, FUNCT_2:35; then A22: (h ") . (h . x) in Cl ((h ") .: Y) by A1, A10, A20, TOPS_2:60; (f ") .: Y = f " Y by A1, A7, A12, FUNCT_1:85 .= Z by A1, A6, A7, A18, A14, A9, FINSEQ_5:4 ; hence x <= y by A1, A20, A22, A21, A14, Def2; ::_thesis: verum end; hence g is isomorphic by A1, A5, A7, A4, WAYBEL_0:66; ::_thesis: verum end; suppose ( S is empty or T is empty ) ; ::_thesis: g is isomorphic then reconsider s = S, t = T as empty TopSpace by A3, A4; A23: Omega t is empty ; Omega s is empty ; hence g is isomorphic by A23, WAYBEL_0:def_38; ::_thesis: verum end; end; end; theorem Th19: :: WAYBEL25:19 for S, T being TopSpace st S,T are_homeomorphic holds Omega S, Omega T are_isomorphic proof let S, T be TopSpace; ::_thesis: ( S,T are_homeomorphic implies Omega S, Omega T are_isomorphic ) assume S,T are_homeomorphic ; ::_thesis: Omega S, Omega T are_isomorphic then consider h being Function of S,T such that A1: h is being_homeomorphism by T_0TOPSP:def_1; A2: the carrier of T = the carrier of (Omega T) by Lm1; the carrier of S = the carrier of (Omega S) by Lm1; then reconsider f = h as Function of (Omega S),(Omega T) by A2; take f ; :: according to WAYBEL_1:def_8 ::_thesis: f is isomorphic thus f is isomorphic by A1, Th18; ::_thesis: verum end; Lm3: for S, T being non empty RelStr for f being Function of S,S for g being Function of T,T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & f = g & f is projection holds g is projection proof let S, T be non empty RelStr ; ::_thesis: for f being Function of S,S for g being Function of T,T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & f = g & f is projection holds g is projection let f be Function of S,S; ::_thesis: for g being Function of T,T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & f = g & f is projection holds g is projection let g be Function of T,T; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & f = g & f is projection implies g is projection ) assume that A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) and A2: f = g and A3: ( f is idempotent & f is monotone ) ; :: according to WAYBEL_1:def_13 ::_thesis: g is projection thus ( g is idempotent & g is monotone ) by A1, A2, A3, WAYBEL_9:1; :: according to WAYBEL_1:def_13 ::_thesis: verum end; theorem Th20: :: WAYBEL25:20 for T being injective T_0-TopSpace holds Omega T is complete continuous LATTICE proof let T be injective T_0-TopSpace; ::_thesis: Omega T is complete continuous LATTICE set S = Sierpinski_Space ; set B = BoolePoset 1; consider M being non empty set such that A1: T is_Retract_of product (M --> Sierpinski_Space) by WAYBEL18:19; consider f being Function of (product (M --> Sierpinski_Space)),(product (M --> Sierpinski_Space)) such that A2: f is continuous and A3: f * f = f and A4: Image f,T are_homeomorphic by A1, WAYBEL18:def_8; A5: RelStr(# the carrier of (Omega (Image f)), the InternalRel of (Omega (Image f)) #), Omega (Image f) are_isomorphic by WAYBEL13:26; Omega (Image f), Omega T are_isomorphic by A4, Th19; then A6: RelStr(# the carrier of (Omega (Image f)), the InternalRel of (Omega (Image f)) #), Omega T are_isomorphic by A5, WAYBEL_1:7; Omega (Image f) is full SubRelStr of Omega (product (M --> Sierpinski_Space)) by Th17; then A7: the InternalRel of (Omega (Image f)) = the InternalRel of (Omega (product (M --> Sierpinski_Space))) |_2 the carrier of (Omega (Image f)) by YELLOW_0:def_14; set TL = the Scott TopAugmentation of product (M --> (BoolePoset 1)); A8: RelStr(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the InternalRel of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by YELLOW_9:def_4; A9: the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)) = the carrier of (product (M --> Sierpinski_Space)) by Th3; then reconsider ff = f as Function of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the Scott TopAugmentation of product (M --> (BoolePoset 1)) ; A10: the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) = the topology of (product (M --> Sierpinski_Space)) by WAYBEL18:15; then A11: ff is continuous by A2, A9, YELLOW12:36; then ( ff is idempotent & ff is monotone ) by A3, QUANTAL1:def_9; then ff is projection by WAYBEL_1:def_13; then reconsider g = ff as projection Function of (product (M --> (BoolePoset 1))),(product (M --> (BoolePoset 1))) by A8, Lm3; A12: the InternalRel of (Image g) = the InternalRel of (product (M --> (BoolePoset 1))) |_2 the carrier of (Image g) by YELLOW_0:def_14; ( TopStruct(# the carrier of TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #), the topology of TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) #) = TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) implies Omega TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) = Omega the Scott TopAugmentation of product (M --> (BoolePoset 1)) ) by Th13; then A13: RelStr(# the carrier of (Omega TopStruct(# the carrier of (product (M --> Sierpinski_Space)), the topology of (product (M --> Sierpinski_Space)) #)), the InternalRel of (Omega TopStruct(# the carrier of (product (M --> Sierpinski_Space)), the topology of (product (M --> Sierpinski_Space)) #)) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by A10, A9, Th16; g is directed-sups-preserving by A8, A11, WAYBEL21:6; then A14: Image g is complete continuous LATTICE by WAYBEL15:15, YELLOW_2:35; the carrier of (Image g) = rng g by YELLOW_0:def_15 .= the carrier of (Image f) by WAYBEL18:9 .= the carrier of (Omega (Image f)) by Lm1 ; hence Omega T is complete continuous LATTICE by A13, A14, A6, A12, A7, WAYBEL15:9, WAYBEL20:18, YELLOW14:11, YELLOW14:12; ::_thesis: verum end; registration let T be injective T_0-TopSpace; cluster Omega T -> complete strict continuous ; coherence ( Omega T is complete & Omega T is continuous ) by Th20; end; theorem Th21: :: WAYBEL25:21 for X, Y being non empty TopSpace for f being continuous Function of (Omega X),(Omega Y) holds f is monotone proof let X, Y be non empty TopSpace; ::_thesis: for f being continuous Function of (Omega X),(Omega Y) holds f is monotone let f be continuous Function of (Omega X),(Omega Y); ::_thesis: f is monotone let x, y be Element of (Omega X); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y ) reconsider Z = {(f . y)} as Subset of Y by Lm1; assume x <= y ; ::_thesis: f . x <= f . y then consider A being Subset of X such that A1: A = {y} and A2: x in Cl A by Def2; A3: for G being Subset of Y st G is open & f . x in G holds Z meets G proof the carrier of X = the carrier of (Omega X) by Lm1; then reconsider g = f as Function of X,Y by Lm1; let G be Subset of Y; ::_thesis: ( G is open & f . x in G implies Z meets G ) assume that A4: G is open and A5: f . x in G ; ::_thesis: Z meets G A6: x in g " G by A5, FUNCT_2:38; A7: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) by Def2; A8: f . y in Z by TARSKI:def_1; TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2; then A9: g is continuous by A7, YELLOW12:36; [#] Y <> {} ; then g " G is open by A4, A9, TOPS_2:43; then A meets g " G by A2, A6, PRE_TOPC:def_7; then consider m being set such that A10: m in A /\ (g " G) by XBOOLE_0:4; m in A by A10, XBOOLE_0:def_4; then A11: m = y by A1, TARSKI:def_1; m in g " G by A10, XBOOLE_0:def_4; then f . y in G by A11, FUNCT_2:38; then Z /\ G <> {} Y by A8, XBOOLE_0:def_4; hence Z meets G by XBOOLE_0:def_7; ::_thesis: verum end; the carrier of Y = the carrier of (Omega Y) by Lm1; then f . x in Cl Z by A3, PRE_TOPC:def_7; hence f . x <= f . y by Def2; ::_thesis: verum end; registration let X, Y be non empty TopSpace; cluster Function-like quasi_total continuous -> monotone for Element of bool [: the carrier of (Omega X), the carrier of (Omega Y):]; coherence for b1 being Function of (Omega X),(Omega Y) st b1 is continuous holds b1 is monotone by Th21; end; theorem Th22: :: WAYBEL25:22 for T being non empty TopSpace for x being Element of (Omega T) holds Cl {x} = downarrow x proof let T be non empty TopSpace; ::_thesis: for x being Element of (Omega T) holds Cl {x} = downarrow x let x be Element of (Omega T); ::_thesis: Cl {x} = downarrow x A1: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: downarrow x c= Cl {x} reconsider Z = {x} as Subset of T by A1; let a be set ; ::_thesis: ( a in Cl {x} implies a in downarrow x ) assume A2: a in Cl {x} ; ::_thesis: a in downarrow x then reconsider b = a as Element of (Omega T) ; a in Cl Z by A1, A2, TOPS_3:80; then b <= x by Def2; hence a in downarrow x by WAYBEL_0:17; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow x or a in Cl {x} ) assume A3: a in downarrow x ; ::_thesis: a in Cl {x} then reconsider b = a as Element of (Omega T) ; b <= x by A3, WAYBEL_0:17; then ex Z being Subset of T st ( Z = {x} & b in Cl Z ) by Def2; hence a in Cl {x} by A1, TOPS_3:80; ::_thesis: verum end; registration let T be non empty TopSpace; let x be Element of (Omega T); cluster Cl {x} -> non empty directed lower ; coherence ( not Cl {x} is empty & Cl {x} is lower & Cl {x} is directed ) proof reconsider y = x as Element of (Omega T) ; Cl {y} = downarrow y by Th22; hence ( not Cl {x} is empty & Cl {x} is lower & Cl {x} is directed ) ; ::_thesis: verum end; cluster downarrow x -> closed ; coherence downarrow x is closed proof Cl {x} = downarrow x by Th22; hence downarrow x is closed ; ::_thesis: verum end; end; theorem Th23: :: WAYBEL25:23 for X being TopSpace for A being open Subset of (Omega X) holds A is upper proof let X be TopSpace; ::_thesis: for A being open Subset of (Omega X) holds A is upper let A be open Subset of (Omega X); ::_thesis: A is upper let x, y be Element of (Omega X); :: according to WAYBEL_0:def_20 ::_thesis: ( not x in A or not x <= y or y in A ) assume A1: x in A ; ::_thesis: ( not x <= y or y in A ) assume x <= y ; ::_thesis: y in A then A2: ex Z being Subset of X st ( Z = {y} & x in Cl Z ) by Def2; then reconsider X = X as non empty TopSpace ; reconsider y = y as Element of (Omega X) ; TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2; then x in Cl {y} by A2, TOPS_3:80; then A meets {y} by A1, PRE_TOPC:def_7; hence y in A by ZFMISC_1:50; ::_thesis: verum end; registration let T be TopSpace; cluster open -> upper for Element of bool the carrier of (Omega T); coherence for b1 being Subset of (Omega T) st b1 is open holds b1 is upper by Th23; end; Lm4: now__::_thesis:_for_X,_Y_being_non_empty_TopSpace for_N_being_net_of_ContMaps_(X,(Omega_Y))_holds_the_mapping_of_N_in_Funcs_(_the_carrier_of_N,(Funcs_(_the_carrier_of_X,_the_carrier_of_Y))) let X, Y be non empty TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y)) holds the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) let N be net of ContMaps (X,(Omega Y)); ::_thesis: the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) A1: the carrier of Y = the carrier of (Omega Y) by Lm1; the carrier of (ContMaps (X,(Omega Y))) c= Funcs ( the carrier of X, the carrier of Y) proof let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in the carrier of (ContMaps (X,(Omega Y))) or f in Funcs ( the carrier of X, the carrier of Y) ) assume f in the carrier of (ContMaps (X,(Omega Y))) ; ::_thesis: f in Funcs ( the carrier of X, the carrier of Y) then ex x being Function of X,(Omega Y) st ( x = f & x is continuous ) by WAYBEL24:def_3; hence f in Funcs ( the carrier of X, the carrier of Y) by A1, FUNCT_2:8; ::_thesis: verum end; then A2: Funcs ( the carrier of N, the carrier of (ContMaps (X,(Omega Y)))) c= Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) by FUNCT_5:56; the mapping of N in Funcs ( the carrier of N, the carrier of (ContMaps (X,(Omega Y)))) by FUNCT_2:8; hence the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) by A2; ::_thesis: verum end; definition let I be non empty set ; let S, T be non empty RelStr ; let N be net of T; let i be Element of I; assume A1: the carrier of T c= the carrier of (S |^ I) ; func commute (N,i,S) -> strict net of S means :Def3: :: WAYBEL25:def 3 ( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = (commute the mapping of N) . i ); existence ex b1 being strict net of S st ( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = (commute the mapping of N) . i ) proof the carrier of T c= Funcs (I, the carrier of S) by A1, YELLOW_1:28; then A1: Funcs ( the carrier of N, the carrier of T) c= Funcs ( the carrier of N,(Funcs (I, the carrier of S))) by FUNCT_5:56; A2: the mapping of N in Funcs ( the carrier of N, the carrier of T) by FUNCT_2:8; then A3: rng ((commute the mapping of N) . i) c= the carrier of S by A1, EQUATION:3; dom ((commute the mapping of N) . i) = the carrier of N by A2, A1, EQUATION:3; then reconsider f = (commute the mapping of N) . i as Function of the carrier of N, the carrier of S by A3, FUNCT_2:def_1, RELSET_1:4; set A = NetStr(# the carrier of N, the InternalRel of N,f #); A4: RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,f #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,f #) #) = RelStr(# the carrier of N, the InternalRel of N #) ; [#] N is directed by WAYBEL_0:def_6; then [#] NetStr(# the carrier of N, the InternalRel of N,f #) is directed by A4, WAYBEL_0:3; then reconsider A = NetStr(# the carrier of N, the InternalRel of N,f #) as strict net of S by A4, WAYBEL_0:def_6, WAYBEL_8:13; take A ; ::_thesis: ( RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of A = (commute the mapping of N) . i ) thus ( RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of A = (commute the mapping of N) . i ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict net of S st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = (commute the mapping of N) . i & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b2 = (commute the mapping of N) . i holds b1 = b2 ; end; :: deftheorem Def3 defines commute WAYBEL25:def_3_:_ for I being non empty set for S, T being non empty RelStr for N being net of T for i being Element of I st the carrier of T c= the carrier of (S |^ I) holds for b6 being strict net of S holds ( b6 = commute (N,i,S) iff ( RelStr(# the carrier of b6, the InternalRel of b6 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b6 = (commute the mapping of N) . i ) ); theorem Th24: :: WAYBEL25:24 for X, Y being non empty TopSpace for N being net of ContMaps (X,(Omega Y)) for i being Element of N for x being Point of X holds the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x proof let X, Y be non empty TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y)) for i being Element of N for x being Point of X holds the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x let N be net of ContMaps (X,(Omega Y)); ::_thesis: for i being Element of N for x being Point of X holds the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x let i be Element of N; ::_thesis: for x being Point of X holds the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x let x be Point of X; ::_thesis: the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x A1: the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) by Lm4; ContMaps (X,(Omega Y)) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3; then the carrier of (ContMaps (X,(Omega Y))) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def_13; hence the mapping of (commute (N,x,(Omega Y))) . i = ((commute the mapping of N) . x) . i by Def3 .= ( the mapping of N . i) . x by A1, FUNCT_6:56 ; ::_thesis: verum end; theorem Th25: :: WAYBEL25:25 for X, Y being non empty TopSpace for N being eventually-directed net of ContMaps (X,(Omega Y)) for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed proof let X, Y be non empty TopSpace; ::_thesis: for N being eventually-directed net of ContMaps (X,(Omega Y)) for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed let N be eventually-directed net of ContMaps (X,(Omega Y)); ::_thesis: for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed let x be Point of X; ::_thesis: commute (N,x,(Omega Y)) is eventually-directed set M = commute (N,x,(Omega Y)); set L = (Omega Y) |^ the carrier of X; for i being Element of (commute (N,x,(Omega Y))) ex j being Element of (commute (N,x,(Omega Y))) st for k being Element of (commute (N,x,(Omega Y))) st j <= k holds (commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k proof let i be Element of (commute (N,x,(Omega Y))); ::_thesis: ex j being Element of (commute (N,x,(Omega Y))) st for k being Element of (commute (N,x,(Omega Y))) st j <= k holds (commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k A1: ContMaps (X,(Omega Y)) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3; then the carrier of (ContMaps (X,(Omega Y))) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def_13; then A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (commute (N,x,(Omega Y))), the InternalRel of (commute (N,x,(Omega Y))) #) by Def3; then reconsider a = i as Element of N ; consider b being Element of N such that A3: for c being Element of N st b <= c holds N . a <= N . c by WAYBEL_0:11; reconsider j = b as Element of (commute (N,x,(Omega Y))) by A2; take j ; ::_thesis: for k being Element of (commute (N,x,(Omega Y))) st j <= k holds (commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k let k be Element of (commute (N,x,(Omega Y))); ::_thesis: ( j <= k implies (commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k ) reconsider c = k as Element of N by A2; reconsider Na = N . a, Nc = N . c as Element of ((Omega Y) |^ the carrier of X) by A1, YELLOW_0:58; reconsider A = Na, C = Nc as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5; assume j <= k ; ::_thesis: (commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k then b <= c by A2, YELLOW_0:1; then N . a <= N . c by A3; then Na <= Nc by A1, YELLOW_0:59; then A <= C by YELLOW_1:def_5; then A4: A . x <= C . x by WAYBEL_3:28; A5: the mapping of (commute (N,x,(Omega Y))) . c = ( the mapping of N . k) . x by Th24; the mapping of (commute (N,x,(Omega Y))) . a = ( the mapping of N . i) . x by Th24; hence (commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k by A4, A5, FUNCOP_1:7; ::_thesis: verum end; hence commute (N,x,(Omega Y)) is eventually-directed by WAYBEL_0:11; ::_thesis: verum end; registration let X, Y be non empty TopSpace; let N be eventually-directed net of ContMaps (X,(Omega Y)); let x be Point of X; cluster commute (N,x,(Omega Y)) -> strict eventually-directed ; coherence commute (N,x,(Omega Y)) is eventually-directed by Th25; end; registration let X, Y be non empty TopSpace; cluster non empty transitive directed -> Function-yielding for NetStr over ContMaps (X,(Omega Y)); coherence for b1 being net of ContMaps (X,(Omega Y)) holds b1 is Function-yielding ; end; Lm5: now__::_thesis:_for_X,_Y_being_non_empty_TopSpace for_N_being_net_of_ContMaps_(X,(Omega_Y)) for_i_being_Element_of_N_holds_ (_the_mapping_of_N_._i_is_Function_of_X,(Omega_Y)_&_the_mapping_of_N_._i_is_Function_of_X,Y_) let X, Y be non empty TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y)) for i being Element of N holds ( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y ) let N be net of ContMaps (X,(Omega Y)); ::_thesis: for i being Element of N holds ( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y ) let i be Element of N; ::_thesis: ( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y ) thus the mapping of N . i is Function of X,(Omega Y) by WAYBEL24:21; ::_thesis: the mapping of N . i is Function of X,Y the carrier of Y = the carrier of (Omega Y) by Lm1; hence the mapping of N . i is Function of X,Y by WAYBEL24:21; ::_thesis: verum end; Lm6: now__::_thesis:_for_X,_Y_being_non_empty_TopSpace for_N_being_net_of_ContMaps_(X,(Omega_Y)) for_x_being_Point_of_X_holds_dom_the_mapping_of_N_=_dom_the_mapping_of_(commute_(N,x,(Omega_Y))) let X, Y be non empty TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y)) for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y))) let N be net of ContMaps (X,(Omega Y)); ::_thesis: for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y))) let x be Point of X; ::_thesis: dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y))) ContMaps (X,(Omega Y)) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3; then the carrier of (ContMaps (X,(Omega Y))) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def_13; then A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (commute (N,x,(Omega Y))), the InternalRel of (commute (N,x,(Omega Y))) #) by Def3; thus dom the mapping of N = the carrier of N by FUNCT_2:def_1 .= dom the mapping of (commute (N,x,(Omega Y))) by A1, FUNCT_2:def_1 ; ::_thesis: verum end; theorem Th26: :: WAYBEL25:26 for X being non empty TopSpace for Y being T_0-TopSpace for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) holds ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X proof let X be non empty TopSpace; ::_thesis: for Y being T_0-TopSpace for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) holds ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X let Y be T_0-TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) holds ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X let N be net of ContMaps (X,(Omega Y)); ::_thesis: ( ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) implies ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X ) assume A1: for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ; ::_thesis: ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X deffunc H1( Element of X) -> Element of the carrier of (Omega Y) = sup (commute (N,\$1,(Omega Y))); set n = the mapping of N; set L = (Omega Y) |^ the carrier of X; consider f being Function of the carrier of X, the carrier of (Omega Y) such that A2: for u being Element of X holds f . u = H1(u) from FUNCT_2:sch_4(); reconsider a = f as Element of ((Omega Y) |^ the carrier of X) by WAYBEL24:19; ex a being Element of ((Omega Y) |^ the carrier of X) st ( rng the mapping of N is_<=_than a & ( for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds a <= b ) ) proof take a ; ::_thesis: ( rng the mapping of N is_<=_than a & ( for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds a <= b ) ) A3: dom the mapping of N = the carrier of N by FUNCT_2:def_1; A4: (Omega Y) |^ the carrier of X = product ( the carrier of X --> (Omega Y)) by YELLOW_1:def_5; thus rng the mapping of N is_<=_than a ::_thesis: for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds a <= b proof let k be Element of ((Omega Y) |^ the carrier of X); :: according to LATTICE3:def_9 ::_thesis: ( not k in rng the mapping of N or k <= a ) reconsider k9 = k, a9 = a as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5; assume k in rng the mapping of N ; ::_thesis: k <= a then consider i being set such that A5: i in dom the mapping of N and A6: k = the mapping of N . i by FUNCT_1:def_3; reconsider i = i as Point of N by A5; for u being Element of X holds k9 . u <= a9 . u proof let u be Element of X; ::_thesis: k9 . u <= a9 . u A7: Omega Y = ( the carrier of X --> (Omega Y)) . u by FUNCOP_1:7; ex_sup_of commute (N,u,(Omega Y)) by A1; then A8: ex_sup_of rng the mapping of (commute (N,u,(Omega Y))), Omega Y by WAYBEL_9:def_3; A9: k9 . u = the mapping of (commute (N,u,(Omega Y))) . i by A6, Th24; dom the mapping of (commute (N,u,(Omega Y))) = the carrier of N by A3, Lm6; then A10: k9 . u in rng the mapping of (commute (N,u,(Omega Y))) by A9, FUNCT_1:def_3; a9 . u = sup (commute (N,u,(Omega Y))) by A2 .= Sup by WAYBEL_2:def_1 .= sup (rng the mapping of (commute (N,u,(Omega Y)))) ; hence k9 . u <= a9 . u by A7, A8, A10, YELLOW_4:1; ::_thesis: verum end; hence k <= a by A4, WAYBEL_3:28; ::_thesis: verum end; let b be Element of ((Omega Y) |^ the carrier of X); ::_thesis: ( rng the mapping of N is_<=_than b implies a <= b ) assume A11: for k being Element of ((Omega Y) |^ the carrier of X) st k in rng the mapping of N holds k <= b ; :: according to LATTICE3:def_9 ::_thesis: a <= b reconsider a9 = a, b9 = b as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5; for u being Element of X holds a9 . u <= b9 . u proof let u be Element of X; ::_thesis: a9 . u <= b9 . u ex_sup_of commute (N,u,(Omega Y)) by A1; then A12: ex_sup_of rng the mapping of (commute (N,u,(Omega Y))), Omega Y by WAYBEL_9:def_3; A13: Omega Y = ( the carrier of X --> (Omega Y)) . u by FUNCOP_1:7; A14: rng the mapping of (commute (N,u,(Omega Y))) is_<=_than b . u proof let s be Element of (Omega Y); :: according to LATTICE3:def_9 ::_thesis: ( not s in rng the mapping of (commute (N,u,(Omega Y))) or s <= b . u ) assume s in rng the mapping of (commute (N,u,(Omega Y))) ; ::_thesis: s <= b . u then consider i being set such that A15: i in dom the mapping of (commute (N,u,(Omega Y))) and A16: the mapping of (commute (N,u,(Omega Y))) . i = s by FUNCT_1:def_3; reconsider i = i as Point of N by A3, A15, Lm6; the mapping of N . i is Function of X,(Omega Y) by WAYBEL24:21; then reconsider k = the mapping of N . i as Element of ((Omega Y) |^ the carrier of X) by WAYBEL24:19; reconsider k9 = k as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5; the mapping of N . i in rng the mapping of N by A3, FUNCT_1:def_3; then k <= b by A11; then A17: k9 <= b9 by YELLOW_1:def_5; s = ( the mapping of N . i) . u by A16, Th24; hence s <= b . u by A13, A17, WAYBEL_3:28; ::_thesis: verum end; a9 . u = sup (commute (N,u,(Omega Y))) by A2 .= Sup by WAYBEL_2:def_1 .= sup (rng the mapping of (commute (N,u,(Omega Y)))) ; hence a9 . u <= b9 . u by A13, A12, A14, YELLOW_0:30; ::_thesis: verum end; hence a <= b by A4, WAYBEL_3:28; ::_thesis: verum end; hence ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X by YELLOW_0:15; ::_thesis: verum end; begin definition let T be non empty TopSpace; attrT is monotone-convergence means :Def4: :: WAYBEL25:def 4 for D being non empty directed Subset of (Omega T) holds ( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds D meets V ) ); end; :: deftheorem Def4 defines monotone-convergence WAYBEL25:def_4_:_ for T being non empty TopSpace holds ( T is monotone-convergence iff for D being non empty directed Subset of (Omega T) holds ( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds D meets V ) ) ); theorem Th27: :: WAYBEL25:27 for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is monotone-convergence holds T is monotone-convergence proof let S, T be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is monotone-convergence implies T is monotone-convergence ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: for D being non empty directed Subset of (Omega S) holds ( ex_sup_of D, Omega S & ( for V being open Subset of S st sup D in V holds D meets V ) ) ; :: according to WAYBEL25:def_4 ::_thesis: T is monotone-convergence let E be non empty directed Subset of (Omega T); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of E, Omega T & ( for V being open Subset of T st sup E in V holds E meets V ) ) A3: Omega S = Omega T by A1, Th13; hence ex_sup_of E, Omega T by A2; ::_thesis: for V being open Subset of T st sup E in V holds E meets V let V be open Subset of T; ::_thesis: ( sup E in V implies E meets V ) assume A4: sup E in V ; ::_thesis: E meets V reconsider W = V as Subset of S by A1; W is open by A1, TOPS_3:76; hence E meets V by A2, A3, A4; ::_thesis: verum end; Lm7: now__::_thesis:_for_T_being_non_empty_1-sorted_ for_D_being_non_empty_Subset_of_T for_d_being_Element_of_T_st_the_carrier_of_T_=_{d}_holds_ D_=_{d} let T be non empty 1-sorted ; ::_thesis: for D being non empty Subset of T for d being Element of T st the carrier of T = {d} holds D = {d} let D be non empty Subset of T; ::_thesis: for d being Element of T st the carrier of T = {d} holds D = {d} let d be Element of T; ::_thesis: ( the carrier of T = {d} implies D = {d} ) assume A1: the carrier of T = {d} ; ::_thesis: D = {d} thus D = {d} ::_thesis: verum proof thus D c= {d} by A1; :: according to XBOOLE_0:def_10 ::_thesis: {d} c= D set x = the Element of D; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {d} or a in D ) assume a in {d} ; ::_thesis: a in D then A2: a = d by TARSKI:def_1; the Element of D in D ; hence a in D by A1, A2, TARSKI:def_1; ::_thesis: verum end; end; registration cluster non empty trivial TopSpace-like T_0 -> monotone-convergence for TopStruct ; coherence for b1 being T_0-TopSpace st b1 is trivial holds b1 is monotone-convergence proof let T be T_0-TopSpace; ::_thesis: ( T is trivial implies T is monotone-convergence ) assume T is trivial ; ::_thesis: T is monotone-convergence then consider d being Element of T such that A1: the carrier of T = {d} by TEX_1:def_1; reconsider d = d as Element of (Omega T) by Lm1; let D be non empty directed Subset of (Omega T); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds D meets V ) ) A2: the carrier of T = the carrier of (Omega T) by Lm1; then D = {d} by A1, Lm7; hence ex_sup_of D, Omega T by YELLOW_0:38; ::_thesis: for V being open Subset of T st sup D in V holds D meets V let V be open Subset of T; ::_thesis: ( sup D in V implies D meets V ) A3: {d} meets {d} ; assume sup D in V ; ::_thesis: D meets V then V = {d} by A1, Lm7; hence D meets V by A1, A2, A3, Lm7; ::_thesis: verum end; end; theorem :: WAYBEL25:28 for S being monotone-convergence T_0-TopSpace for T being T_0-TopSpace st S,T are_homeomorphic holds T is monotone-convergence proof let S be monotone-convergence T_0-TopSpace; ::_thesis: for T being T_0-TopSpace st S,T are_homeomorphic holds T is monotone-convergence let T be T_0-TopSpace; ::_thesis: ( S,T are_homeomorphic implies T is monotone-convergence ) given h being Function of S,T such that A1: h is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: T is monotone-convergence the carrier of S = the carrier of (Omega S) by Lm1; then reconsider f = h as Function of (Omega S),(Omega T) by Lm1; f is isomorphic by A1, Th18; then A2: rng f = the carrier of (Omega T) by WAYBEL_0:66; let D be non empty directed Subset of (Omega T); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds D meets V ) ) A3: f " is isomorphic by A1, Th18, YELLOW14:10; then f " is sups-preserving by WAYBEL13:20; then A4: f " preserves_sup_of D by WAYBEL_0:def_33; A5: rng h = [#] T by A1, TOPS_2:def_5; A6: h is V7() by A1, TOPS_2:def_5; A7: h is onto by A5, FUNCT_2:def_3; (f ") .: D is directed by A3, YELLOW_2:15; then A8: f " D is non empty directed Subset of (Omega S) by A2, A5, A6, TOPS_2:55; then ex_sup_of f " D, Omega S by Def4; then ex_sup_of f .: (f " D), Omega T by A1, Th18, YELLOW14:16; hence A9: ex_sup_of D, Omega T by A2, FUNCT_1:77; ::_thesis: for V being open Subset of T st sup D in V holds D meets V let V be open Subset of T; ::_thesis: ( sup D in V implies D meets V ) assume sup D in V ; ::_thesis: D meets V then (h ") . (sup D) in (h ") .: V by FUNCT_2:35; then (h ") . (sup D) in h " V by A5, A6, TOPS_2:55; then (h ") . (sup D) in h " V by A7, A6, TOPS_2:def_4; then (f ") . (sup D) in h " V by A2, A6, A7, A5, TOPS_2:def_4; then sup ((f ") .: D) in h " V by A9, A4, WAYBEL_0:def_31; then A10: sup (f " D) in h " V by A2, A5, A6, TOPS_2:55; h " V is open by A1, TOPGRP_1:26; then f " D meets h " V by A8, A10, Def4; then consider a being set such that A11: a in f " D and A12: a in h " V by XBOOLE_0:3; reconsider a = a as Element of S by A12; now__::_thesis:_ex_b_being_Element_of_the_carrier_of_T_st_ (_b_in_D_&_b_in_V_) take b = h . a; ::_thesis: ( b in D & b in V ) thus ( b in D & b in V ) by A11, A12, FUNCT_2:38; ::_thesis: verum end; hence D meets V by XBOOLE_0:3; ::_thesis: verum end; theorem Th29: :: WAYBEL25:29 for S being complete Scott TopLattice holds S is monotone-convergence proof let S be complete Scott TopLattice; ::_thesis: S is monotone-convergence let D be non empty directed Subset of (Omega S); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of D, Omega S & ( for V being open Subset of S st sup D in V holds D meets V ) ) thus ex_sup_of D, Omega S by YELLOW_0:17; ::_thesis: for V being open Subset of S st sup D in V holds D meets V A1: Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) by Th15; then A2: RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of S, the InternalRel of S #) ; reconsider E = D as Subset of S by A1; let V be open Subset of S; ::_thesis: ( sup D in V implies D meets V ) assume sup D in V ; ::_thesis: D meets V then A3: sup E in V by A2, YELLOW_0:17, YELLOW_0:26; E is non empty directed Subset of S by A2, WAYBEL_0:3; hence D meets V by A3, WAYBEL11:def_1; ::_thesis: verum end; registration let L be complete LATTICE; cluster Scott -> Scott monotone-convergence for TopAugmentation of L; coherence for b1 being Scott TopAugmentation of L holds b1 is monotone-convergence by Th29; end; registration let L be complete LATTICE; let S be Scott TopAugmentation of L; cluster TopStruct(# the carrier of S, the topology of S #) -> monotone-convergence ; coherence TopStruct(# the carrier of S, the topology of S #) is monotone-convergence by Th27; end; theorem Th30: :: WAYBEL25:30 for X being monotone-convergence T_0-TopSpace holds Omega X is up-complete proof let X be monotone-convergence T_0-TopSpace; ::_thesis: Omega X is up-complete for A being non empty directed Subset of (Omega X) holds ex_sup_of A, Omega X by Def4; hence Omega X is up-complete by WAYBEL_0:75; ::_thesis: verum end; registration let X be monotone-convergence T_0-TopSpace; cluster Omega X -> up-complete strict ; coherence Omega X is up-complete by Th30; end; theorem Th31: :: WAYBEL25:31 for X being non empty monotone-convergence TopSpace for N being eventually-directed prenet of Omega X holds ex_sup_of N proof let X be non empty monotone-convergence TopSpace; ::_thesis: for N being eventually-directed prenet of Omega X holds ex_sup_of N let N be eventually-directed prenet of Omega X; ::_thesis: ex_sup_of N rng (netmap (N,(Omega X))) is directed by WAYBEL_2:18; hence ex_sup_of rng the mapping of N, Omega X by Def4; :: according to WAYBEL_9:def_3 ::_thesis: verum end; theorem Th32: :: WAYBEL25:32 for X being non empty monotone-convergence TopSpace for N being eventually-directed net of Omega X holds sup N in Lim N proof let X be non empty monotone-convergence TopSpace; ::_thesis: for N being eventually-directed net of Omega X holds sup N in Lim N let N be eventually-directed net of Omega X; ::_thesis: sup N in Lim N rng (netmap (N,(Omega X))) is directed by WAYBEL_2:18; then reconsider D = rng the mapping of N as non empty directed Subset of (Omega X) ; for V being a_neighborhood of sup N holds N is_eventually_in V proof let V be a_neighborhood of sup N; ::_thesis: N is_eventually_in V A1: Int V c= V by TOPS_1:16; A2: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2; then reconsider I = Int V as Subset of X ; A3: I is open by A2, TOPS_3:76; sup N in I by CONNSP_2:def_1; then Sup in I by WAYBEL_2:def_1; then D meets I by A3, Def4; then consider y being set such that A4: y in D and A5: y in I by XBOOLE_0:3; reconsider y = y as Point of X by A5; consider x being set such that A6: x in dom the mapping of N and A7: the mapping of N . x = y by A4, FUNCT_1:def_3; reconsider x = x as Element of N by A6; consider j being Element of N such that A8: for k being Element of N st j <= k holds N . x <= N . k by WAYBEL_0:11; take j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not j <= b1 or N . b1 in V ) let k be Element of N; ::_thesis: ( not j <= k or N . k in V ) assume j <= k ; ::_thesis: N . k in V then N . x <= N . k by A8; then consider Y being Subset of X such that A9: Y = {(N . k)} and A10: N . x in Cl Y by Def2; Y meets I by A3, A5, A7, A10, PRE_TOPC:def_7; then consider m being set such that A11: m in Y /\ I by XBOOLE_0:4; m in Y by A11, XBOOLE_0:def_4; then A12: m = N . k by A9, TARSKI:def_1; m in I by A11, XBOOLE_0:def_4; hence N . k in V by A12, A1; ::_thesis: verum end; hence sup N in Lim N by YELLOW_6:def_15; ::_thesis: verum end; theorem Th33: :: WAYBEL25:33 for X being non empty monotone-convergence TopSpace for N being eventually-directed net of Omega X holds N is convergent proof let X be non empty monotone-convergence TopSpace; ::_thesis: for N being eventually-directed net of Omega X holds N is convergent let N be eventually-directed net of Omega X; ::_thesis: N is convergent thus Lim N <> {} by Th32; :: according to YELLOW_6:def_16 ::_thesis: verum end; registration let X be non empty monotone-convergence TopSpace; cluster non empty transitive directed eventually-directed -> eventually-directed convergent for NetStr over Omega X; coherence for b1 being eventually-directed net of Omega X holds b1 is convergent by Th33; end; theorem :: WAYBEL25:34 for X being non empty TopSpace st ( for N being eventually-directed net of Omega X holds ( ex_sup_of N & sup N in Lim N ) ) holds X is monotone-convergence proof let X be non empty TopSpace; ::_thesis: ( ( for N being eventually-directed net of Omega X holds ( ex_sup_of N & sup N in Lim N ) ) implies X is monotone-convergence ) assume A1: for N being eventually-directed net of Omega X holds ( ex_sup_of N & sup N in Lim N ) ; ::_thesis: X is monotone-convergence let D be non empty directed Subset of (Omega X); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of D, Omega X & ( for V being open Subset of X st sup D in V holds D meets V ) ) Net-Str D = NetStr(# D,( the InternalRel of (Omega X) |_2 D),((id the carrier of (Omega X)) | D) #) by WAYBEL17:def_4; then A2: rng the mapping of (Net-Str D) = D by YELLOW14:2; ex_sup_of Net-Str D by A1; hence ex_sup_of D, Omega X by A2, WAYBEL_9:def_3; ::_thesis: for V being open Subset of X st sup D in V holds D meets V let V be open Subset of X; ::_thesis: ( sup D in V implies D meets V ) assume A3: sup D in V ; ::_thesis: D meets V reconsider Z = V as Subset of (Omega X) by Lm1; A4: sup (Net-Str D) = Sup by WAYBEL_2:def_1 .= sup (rng the mapping of (Net-Str D)) ; TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2; then Int Z = Int V by TOPS_3:77; then sup (Net-Str D) in Int Z by A2, A3, A4, TOPS_1:23; then A5: Z is a_neighborhood of sup (Net-Str D) by CONNSP_2:def_1; sup (Net-Str D) in Lim (Net-Str D) by A1; then Net-Str D is_eventually_in V by A5, YELLOW_6:def_15; then consider i being Element of (Net-Str D) such that A6: for j being Element of (Net-Str D) st i <= j holds (Net-Str D) . j in V by WAYBEL_0:def_11; now__::_thesis:_ex_a_being_Element_of_the_carrier_of_(Omega_X)_st_ (_a_in_D_&_a_in_V_) take a = (Net-Str D) . i; ::_thesis: ( a in D & a in V ) dom the mapping of (Net-Str D) = the carrier of (Net-Str D) by FUNCT_2:def_1; hence a in D by A2, FUNCT_1:def_3; ::_thesis: a in V thus a in V by A6; ::_thesis: verum end; hence D meets V by XBOOLE_0:3; ::_thesis: verum end; theorem Th35: :: WAYBEL25:35 for X being non empty monotone-convergence TopSpace for Y being T_0-TopSpace for f being continuous Function of (Omega X),(Omega Y) holds f is directed-sups-preserving proof let X be non empty monotone-convergence TopSpace; ::_thesis: for Y being T_0-TopSpace for f being continuous Function of (Omega X),(Omega Y) holds f is directed-sups-preserving let Y be T_0-TopSpace; ::_thesis: for f being continuous Function of (Omega X),(Omega Y) holds f is directed-sups-preserving let f be continuous Function of (Omega X),(Omega Y); ::_thesis: f is directed-sups-preserving let D be non empty directed Subset of (Omega X); :: according to YELLOW14:def_1 ::_thesis: f preserves_sup_of D assume A1: ex_sup_of D, Omega X ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: D, Omega Y & "\/" ((f .: D),(Omega Y)) = f . ("\/" (D,(Omega X))) ) set V = (downarrow (sup (f .: D))) ` ; A2: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2; then reconsider fV = f " ((downarrow (sup (f .: D))) `) as Subset of X ; [#] (Omega Y) <> {} ; then f " ((downarrow (sup (f .: D))) `) is open by TOPS_2:43; then reconsider fV = fV as open Subset of X by A2, TOPS_3:76; sup (f .: D) <= sup (f .: D) ; then A3: sup (f .: D) in downarrow (sup (f .: D)) by WAYBEL_0:17; A4: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) by Def2; ex a being Element of (Omega Y) st ( f .: D is_<=_than a & ( for b being Element of (Omega Y) st f .: D is_<=_than b holds a <= b ) ) proof take a = f . (sup D); ::_thesis: ( f .: D is_<=_than a & ( for b being Element of (Omega Y) st f .: D is_<=_than b holds a <= b ) ) D is_<=_than sup D by A1, YELLOW_0:def_9; hence f .: D is_<=_than a by YELLOW_2:14; ::_thesis: for b being Element of (Omega Y) st f .: D is_<=_than b holds a <= b let b be Element of (Omega Y); ::_thesis: ( f .: D is_<=_than b implies a <= b ) assume A5: for c being Element of (Omega Y) st c in f .: D holds c <= b ; :: according to LATTICE3:def_9 ::_thesis: a <= b reconsider Z = {b} as Subset of Y by Lm1; for G being Subset of Y st G is open & a in G holds Z meets G proof let G be Subset of Y; ::_thesis: ( G is open & a in G implies Z meets G ) assume that A6: G is open and A7: a in G ; ::_thesis: Z meets G reconsider H = G as open Subset of (Omega Y) by A4, A6, TOPS_3:76; [#] (Omega Y) <> {} ; then f " H is open by TOPS_2:43; then A8: f " H is open Subset of X by A2, TOPS_3:76; sup D in f " H by A7, FUNCT_2:38; then D meets f " H by A8, Def4; then consider c being set such that A9: c in D and A10: c in f " H by XBOOLE_0:3; reconsider c = c as Point of (Omega X) by A9; A11: f . c in H by A10, FUNCT_2:38; f . c <= b by A5, A9, FUNCT_2:35; then A12: b in G by A11, WAYBEL_0:def_20; b in {b} by TARSKI:def_1; hence Z meets G by A12, XBOOLE_0:3; ::_thesis: verum end; then a in Cl Z by A4, PRE_TOPC:def_7; hence a <= b by Def2; ::_thesis: verum end; hence A13: ex_sup_of f .: D, Omega Y by YELLOW_0:15; ::_thesis: "\/" ((f .: D),(Omega Y)) = f . ("\/" (D,(Omega X))) assume A14: sup (f .: D) <> f . (sup D) ; ::_thesis: contradiction sup (f .: D) <= f . (sup D) by A1, A13, WAYBEL17:15; then not f . (sup D) <= sup (f .: D) by A14, ORDERS_2:2; then not f . (sup D) in downarrow (sup (f .: D)) by WAYBEL_0:17; then f . (sup D) in (downarrow (sup (f .: D))) ` by XBOOLE_0:def_5; then sup D in fV by FUNCT_2:38; then D meets fV by Def4; then consider d being set such that A15: d in D and A16: d in fV by XBOOLE_0:3; reconsider d = d as Element of (Omega X) by A15; A17: f . d in (downarrow (sup (f .: D))) ` by A16, FUNCT_2:38; f . d <= sup (f .: D) by A13, A15, FUNCT_2:35, YELLOW_4:1; then sup (f .: D) in (downarrow (sup (f .: D))) ` by A17, WAYBEL_0:def_20; hence contradiction by A3, XBOOLE_0:def_5; ::_thesis: verum end; registration let X be non empty monotone-convergence TopSpace; let Y be T_0-TopSpace; cluster Function-like quasi_total continuous -> directed-sups-preserving for Element of bool [: the carrier of (Omega X), the carrier of (Omega Y):]; coherence for b1 being Function of (Omega X),(Omega Y) st b1 is continuous holds b1 is directed-sups-preserving by Th35; end; theorem Th36: :: WAYBEL25:36 for T being monotone-convergence T_0-TopSpace for R being T_0-TopSpace st R is_Retract_of T holds R is monotone-convergence proof let T be monotone-convergence T_0-TopSpace; ::_thesis: for R being T_0-TopSpace st R is_Retract_of T holds R is monotone-convergence let R be T_0-TopSpace; ::_thesis: ( R is_Retract_of T implies R is monotone-convergence ) given c being continuous Function of R,T, r being continuous Function of T,R such that A1: r * c = id R ; :: according to WAYBEL25:def_1 ::_thesis: R is monotone-convergence let D be non empty directed Subset of (Omega R); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of D, Omega R & ( for V being open Subset of R st sup D in V holds D meets V ) ) A2: TopStruct(# the carrier of R, the topology of R #) = TopStruct(# the carrier of (Omega R), the topology of (Omega R) #) by Def2; then reconsider DR = D as non empty Subset of R ; A3: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2; then reconsider f = c * r as Function of (Omega T),(Omega T) ; reconsider rr = r as Function of (Omega T),(Omega R) by A3, A2; A4: r .: (c .: D) = (r * c) .: DR by RELAT_1:126 .= D by A1, FUNCT_1:92 ; reconsider cc = c as Function of (Omega R),(Omega T) by A3, A2; cc is continuous by A3, A2, YELLOW12:36; then A5: cc .: D is directed by YELLOW_2:15; then A6: ex_sup_of cc .: D, Omega T by Def4; f is continuous by A3, YELLOW12:36; then A7: f preserves_sup_of cc .: D by A5, WAYBEL_0:def_37; rr is continuous by A3, A2, YELLOW12:36; then A8: rr preserves_sup_of cc .: D by A5, WAYBEL_0:def_37; hence ex_sup_of D, Omega R by A6, A4, WAYBEL_0:def_31; ::_thesis: for V being open Subset of R st sup D in V holds D meets V A9: c . (sup D) = c . (r . (sup (cc .: D))) by A6, A4, A8, WAYBEL_0:def_31 .= f . (sup (cc .: D)) by A3, FUNCT_2:15 .= sup (f .: (cc .: D)) by A6, A7, WAYBEL_0:def_31 .= sup (cc .: D) by A4, RELAT_1:126 ; let V be open Subset of R; ::_thesis: ( sup D in V implies D meets V ) assume sup D in V ; ::_thesis: D meets V then A10: c . (sup D) in c .: V by FUNCT_2:35; A11: c .: V c= r " V proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in c .: V or a in r " V ) assume a in c .: V ; ::_thesis: a in r " V then consider x being set such that A12: x in the carrier of R and A13: x in V and A14: a = c . x by FUNCT_2:64; reconsider x = x as Point of R by A12; A15: a = c . x by A14; r . a = (r * c) . x by A14, FUNCT_2:15 .= x by A1, FUNCT_1:18 ; hence a in r " V by A13, A15, FUNCT_2:38; ::_thesis: verum end; [#] R <> {} ; then r " V is open by TOPS_2:43; then c .: D meets r " V by A5, A11, A9, A10, Def4; then consider d being set such that A16: d in cc .: D and A17: d in r " V by XBOOLE_0:3; now__::_thesis:_ex_a_being_set_st_ (_a_in_D_&_a_in_V_) take a = r . d; ::_thesis: ( a in D & a in V ) thus a in D by A4, A16, FUNCT_2:35; ::_thesis: a in V thus a in V by A17, FUNCT_2:38; ::_thesis: verum end; hence D meets V by XBOOLE_0:3; ::_thesis: verum end; theorem Th37: :: WAYBEL25:37 for T being injective T_0-TopSpace for S being Scott TopAugmentation of Omega T holds TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) proof set SS = Sierpinski_Space ; set B = BoolePoset 1; let T be injective T_0-TopSpace; ::_thesis: for S being Scott TopAugmentation of Omega T holds TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) let S be Scott TopAugmentation of Omega T; ::_thesis: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) consider M being non empty set such that A1: T is_Retract_of product (M --> Sierpinski_Space) by WAYBEL18:19; consider c being continuous Function of T,(product (M --> Sierpinski_Space)), r being continuous Function of (product (M --> Sierpinski_Space)),T such that A2: r * c = id T by A1, Def1; A3: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2; A4: TopStruct(# the carrier of (product (M --> Sierpinski_Space)), the topology of (product (M --> Sierpinski_Space)) #) = TopStruct(# the carrier of (Omega (product (M --> Sierpinski_Space))), the topology of (Omega (product (M --> Sierpinski_Space))) #) by Def2; then reconsider c1a = c as Function of (Omega T),(Omega (product (M --> Sierpinski_Space))) by A3; set S2M = the Scott TopAugmentation of product (M --> (BoolePoset 1)); A5: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of S, the topology of S #) ; A6: RelStr(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the InternalRel of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by YELLOW_9:def_4; then reconsider c1 = c as Function of (Omega T),(product (M --> (BoolePoset 1))) by A3, Th3; A7: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (Omega T), the InternalRel of (Omega T) #) by YELLOW_9:def_4; then reconsider c2 = c1 as Function of S, the Scott TopAugmentation of product (M --> (BoolePoset 1)) by A6; A8: the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)) = the carrier of (product (M --> Sierpinski_Space)) by Th3; then reconsider rr = r as Function of the Scott TopAugmentation of product (M --> (BoolePoset 1)),T ; A9: the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) = the topology of (product (M --> Sierpinski_Space)) by WAYBEL18:15; then reconsider W = T as non empty monotone-convergence TopSpace by A1, A8, Th36; Omega (product (M --> Sierpinski_Space)) = Omega the Scott TopAugmentation of product (M --> (BoolePoset 1)) by A9, A8, Th13; then A10: RelStr(# the carrier of (Omega (product (M --> Sierpinski_Space))), the InternalRel of (Omega (product (M --> Sierpinski_Space))) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by Th16 .= RelStr(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the InternalRel of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) by YELLOW_9:def_4 ; reconsider r1 = r as Function of (product (M --> (BoolePoset 1))),(Omega T) by A8, A6, A3; A11: RelStr(# the carrier of (Omega the Scott TopAugmentation of product (M --> (BoolePoset 1))), the InternalRel of (Omega the Scott TopAugmentation of product (M --> (BoolePoset 1))) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by Th16; then reconsider rr1 = r1 as Function of (Omega the Scott TopAugmentation of product (M --> (BoolePoset 1))),(Omega T) ; reconsider r2 = r1 as Function of the Scott TopAugmentation of product (M --> (BoolePoset 1)),S by A6, A7; reconsider r3 = r2 as Function of (product (M --> Sierpinski_Space)),S by Th3; TopStruct(# the carrier of (Omega the Scott TopAugmentation of product (M --> (BoolePoset 1))), the topology of (Omega the Scott TopAugmentation of product (M --> (BoolePoset 1))) #) = TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) by Def2; then rr1 is continuous by A9, A8, A3, YELLOW12:36; then r2 is directed-sups-preserving by A6, A7, A11, WAYBEL21:6; then r3 is continuous by A9, A8, A5, YELLOW12:36; then A12: r3 * c is continuous ; reconsider c1a = c1a as continuous Function of (Omega W),(Omega (product (M --> Sierpinski_Space))) by A3, A4, YELLOW12:36; c2 = c1a ; then A13: c2 is directed-sups-preserving by A7, A10, WAYBEL21:6; TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T, the topology of T #) ; then rr is continuous by A9, A8, YELLOW12:36; then rr * c2 is continuous by A13; hence TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) by A2, A12, YELLOW14:33; ::_thesis: verum end; theorem :: WAYBEL25:38 for T being injective T_0-TopSpace holds ( T is compact & T is locally-compact & T is sober ) proof let T be injective T_0-TopSpace; ::_thesis: ( T is compact & T is locally-compact & T is sober ) set S = the Scott TopAugmentation of Omega T; A1: ( the Scott TopAugmentation of Omega T is compact & the Scott TopAugmentation of Omega T is locally-compact & the Scott TopAugmentation of Omega T is sober ) by WAYBEL14:32; TopStruct(# the carrier of the Scott TopAugmentation of Omega T, the topology of the Scott TopAugmentation of Omega T #) = TopStruct(# the carrier of T, the topology of T #) by Th37; hence ( T is compact & T is locally-compact & T is sober ) by A1, YELLOW14:26, YELLOW14:27, YELLOW14:28; ::_thesis: verum end; theorem Th39: :: WAYBEL25:39 for T being injective T_0-TopSpace holds T is monotone-convergence proof let T be injective T_0-TopSpace; ::_thesis: T is monotone-convergence set S = the Scott TopAugmentation of Omega T; TopStruct(# the carrier of the Scott TopAugmentation of Omega T, the topology of the Scott TopAugmentation of Omega T #) = TopStruct(# the carrier of T, the topology of T #) by Th37; hence T is monotone-convergence by Th27; ::_thesis: verum end; registration cluster non empty TopSpace-like T_0 injective -> monotone-convergence for TopStruct ; coherence for b1 being T_0-TopSpace st b1 is injective holds b1 is monotone-convergence by Th39; end; theorem Th40: :: WAYBEL25:40 for X being non empty TopSpace for Y being monotone-convergence T_0-TopSpace for N being net of ContMaps (X,(Omega Y)) for f, g being Function of X,(Omega Y) st f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds g <= f proof let X be non empty TopSpace; ::_thesis: for Y being monotone-convergence T_0-TopSpace for N being net of ContMaps (X,(Omega Y)) for f, g being Function of X,(Omega Y) st f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds g <= f let Y be monotone-convergence T_0-TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y)) for f, g being Function of X,(Omega Y) st f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds g <= f let N be net of ContMaps (X,(Omega Y)); ::_thesis: for f, g being Function of X,(Omega Y) st f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds g <= f let f, g be Function of X,(Omega Y); ::_thesis: ( f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N implies g <= f ) set m = the mapping of N; set L = (Omega Y) |^ the carrier of X; set s = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)); assume that A1: f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) and A2: ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X and A3: g in rng the mapping of N ; ::_thesis: g <= f reconsider g1 = g as Element of ((Omega Y) |^ the carrier of X) by WAYBEL24:19; rng the mapping of N is_<=_than "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) by A2, YELLOW_0:def_9; then g1 <= "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) by A3, LATTICE3:def_9; hence g <= f by A1, WAYBEL10:11; ::_thesis: verum end; theorem Th41: :: WAYBEL25:41 for X being non empty TopSpace for Y being monotone-convergence T_0-TopSpace for N being net of ContMaps (X,(Omega Y)) for x being Point of X for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds f . x = sup (commute (N,x,(Omega Y))) proof let X be non empty TopSpace; ::_thesis: for Y being monotone-convergence T_0-TopSpace for N being net of ContMaps (X,(Omega Y)) for x being Point of X for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds f . x = sup (commute (N,x,(Omega Y))) let Y be monotone-convergence T_0-TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y)) for x being Point of X for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds f . x = sup (commute (N,x,(Omega Y))) let N be net of ContMaps (X,(Omega Y)); ::_thesis: for x being Point of X for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds f . x = sup (commute (N,x,(Omega Y))) let x be Point of X; ::_thesis: for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds f . x = sup (commute (N,x,(Omega Y))) let f be Function of X,(Omega Y); ::_thesis: ( ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) implies f . x = sup (commute (N,x,(Omega Y))) ) assume that A1: for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed and A2: f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) ; ::_thesis: f . x = sup (commute (N,x,(Omega Y))) set n = the mapping of N; set m = the mapping of (commute (N,x,(Omega Y))); set L = (Omega Y) |^ the carrier of X; A3: for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) proof let x be Point of X; ::_thesis: ex_sup_of commute (N,x,(Omega Y)) commute (N,x,(Omega Y)) is eventually-directed by A1; hence ex_sup_of commute (N,x,(Omega Y)) by Th31; ::_thesis: verum end; then A4: ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X by Th26; A5: dom the mapping of N = the carrier of N by FUNCT_2:def_1; then A6: dom the mapping of (commute (N,x,(Omega Y))) = the carrier of N by Lm6; A7: for a being Element of (Omega Y) st rng the mapping of (commute (N,x,(Omega Y))) is_<=_than a holds f . x <= a proof let a be Element of (Omega Y); ::_thesis: ( rng the mapping of (commute (N,x,(Omega Y))) is_<=_than a implies f . x <= a ) defpred S1[ set , set ] means ( ( \$1 = x implies \$2 = a ) & ( \$1 <> x implies ex u being Element of X st ( \$1 = u & \$2 = sup (commute (N,u,(Omega Y))) ) ) ); A8: Omega Y = ( the carrier of X --> (Omega Y)) . x by FUNCOP_1:7; A9: for e being Element of X ex u being Element of (Omega Y) st S1[e,u] proof let e be Element of X; ::_thesis: ex u being Element of (Omega Y) st S1[e,u] percases ( e = x or e <> x ) ; suppose e = x ; ::_thesis: ex u being Element of (Omega Y) st S1[e,u] hence ex u being Element of (Omega Y) st S1[e,u] ; ::_thesis: verum end; supposeA10: e <> x ; ::_thesis: ex u being Element of (Omega Y) st S1[e,u] reconsider e = e as Element of X ; take sup (commute (N,e,(Omega Y))) ; ::_thesis: S1[e, sup (commute (N,e,(Omega Y)))] thus S1[e, sup (commute (N,e,(Omega Y)))] by A10; ::_thesis: verum end; end; end; consider t being Function of the carrier of X, the carrier of (Omega Y) such that A11: for u being Element of X holds S1[u,t . u] from FUNCT_2:sch_3(A9); reconsider t = t as Function of X,(Omega Y) ; reconsider tt = t as Element of ((Omega Y) |^ the carrier of X) by WAYBEL24:19; reconsider p = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)), q = tt as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5; assume A12: for e being Element of (Omega Y) st e in rng the mapping of (commute (N,x,(Omega Y))) holds e <= a ; :: according to LATTICE3:def_9 ::_thesis: f . x <= a tt is_>=_than rng the mapping of N proof let s be Element of ((Omega Y) |^ the carrier of X); :: according to LATTICE3:def_9 ::_thesis: ( not s in rng the mapping of N or s <= tt ) reconsider ss = s as Function of X,(Omega Y) by WAYBEL24:19; reconsider s9 = s, t9 = tt as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5; assume s in rng the mapping of N ; ::_thesis: s <= tt then consider i being set such that A13: i in dom the mapping of N and A14: s = the mapping of N . i by FUNCT_1:def_3; reconsider i = i as Point of N by A13; A15: for j being Element of X holds s9 . j <= t9 . j proof let j be Element of X; ::_thesis: s9 . j <= t9 . j A16: Omega Y = ( the carrier of X --> (Omega Y)) . j by FUNCOP_1:7; A17: ss . j = the mapping of (commute (N,j,(Omega Y))) . i by A14, Th24; percases ( j <> x or j = x ) ; suppose j <> x ; ::_thesis: s9 . j <= t9 . j then ex u being Element of X st ( j = u & t . j = sup (commute (N,u,(Omega Y))) ) by A11; then A18: t9 . j = Sup by WAYBEL_2:def_1 .= sup (rng the mapping of (commute (N,j,(Omega Y)))) ; commute (N,j,(Omega Y)) is eventually-directed by A1; then ex_sup_of commute (N,j,(Omega Y)) by Th31; then A19: ex_sup_of rng the mapping of (commute (N,j,(Omega Y))), Omega Y by WAYBEL_9:def_3; i in dom the mapping of (commute (N,j,(Omega Y))) by A13, Lm6; then ss . j in rng the mapping of (commute (N,j,(Omega Y))) by A17, FUNCT_1:def_3; hence s9 . j <= t9 . j by A16, A18, A19, YELLOW_4:1; ::_thesis: verum end; supposeA20: j = x ; ::_thesis: s9 . j <= t9 . j A21: the mapping of (commute (N,x,(Omega Y))) . i in rng the mapping of (commute (N,x,(Omega Y))) by A6, FUNCT_1:def_3; ss . x = the mapping of (commute (N,x,(Omega Y))) . i by A14, Th24; then ss . x <= a by A12, A21; hence s9 . j <= t9 . j by A11, A16, A20; ::_thesis: verum end; end; end; (Omega Y) |^ the carrier of X = product ( the carrier of X --> (Omega Y)) by YELLOW_1:def_5; hence s <= tt by A15, WAYBEL_3:28; ::_thesis: verum end; then "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) <= tt by A4, YELLOW_0:30; then A22: p <= q by YELLOW_1:def_5; tt . x = a by A11; hence f . x <= a by A2, A8, A22, WAYBEL_3:28; ::_thesis: verum end; rng the mapping of (commute (N,x,(Omega Y))) is_<=_than f . x proof let w be Element of (Omega Y); :: according to LATTICE3:def_9 ::_thesis: ( not w in rng the mapping of (commute (N,x,(Omega Y))) or w <= f . x ) assume w in rng the mapping of (commute (N,x,(Omega Y))) ; ::_thesis: w <= f . x then consider i being set such that A23: i in dom the mapping of (commute (N,x,(Omega Y))) and A24: the mapping of (commute (N,x,(Omega Y))) . i = w by FUNCT_1:def_3; reconsider i = i as Point of N by A5, A23, Lm6; reconsider g = the mapping of N . i as Function of X,(Omega Y) by Lm5; g in rng the mapping of N by A5, FUNCT_1:def_3; then g <= f by A2, A3, Th26, Th40; then ex a, b being Element of (Omega Y) st ( a = g . x & b = f . x & a <= b ) by YELLOW_2:def_1; hence w <= f . x by A24, Th24; ::_thesis: verum end; hence f . x = Sup by A7, YELLOW_0:30 .= sup (commute (N,x,(Omega Y))) by WAYBEL_2:def_1 ; ::_thesis: verum end; theorem Th42: :: WAYBEL25:42 for X being non empty TopSpace for Y being monotone-convergence T_0-TopSpace for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed ) holds "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y proof let X be non empty TopSpace; ::_thesis: for Y being monotone-convergence T_0-TopSpace for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed ) holds "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y let Y be monotone-convergence T_0-TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed ) holds "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y let N be net of ContMaps (X,(Omega Y)); ::_thesis: ( ( for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed ) implies "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y ) assume A1: for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed ; ::_thesis: "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y set m = the mapping of N; set L = (Omega Y) |^ the carrier of X; reconsider fo = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) as Function of X,(Omega Y) by WAYBEL24:19; A2: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) by Def2; then reconsider f = fo as Function of X,Y ; A3: dom the mapping of N = the carrier of N by FUNCT_2:def_1; A4: for V being Subset of Y st V is open holds f " V is open proof let V be Subset of Y; ::_thesis: ( V is open implies f " V is open ) assume A5: V is open ; ::_thesis: f " V is open set M = { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } ; for x being set holds ( x in f " V iff x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } ) proof let x be set ; ::_thesis: ( x in f " V iff x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } ) A6: dom f = the carrier of X by FUNCT_2:def_1; thus ( x in f " V implies x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } ) ::_thesis: ( x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } implies x in f " V ) proof A7: the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) by Lm4; assume A8: x in f " V ; ::_thesis: x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } then A9: f . x in V by FUNCT_2:38; reconsider x = x as Point of X by A8; set NET = commute (N,x,(Omega Y)); commute (N,x,(Omega Y)) is eventually-directed by A1; then reconsider W = rng (netmap ((commute (N,x,(Omega Y))),(Omega Y))) as non empty directed Subset of (Omega Y) by WAYBEL_2:18; f . x = sup (commute (N,x,(Omega Y))) by A1, Th41 .= Sup by WAYBEL_2:def_1 .= sup W ; then W meets V by A5, A9, Def4; then consider k being set such that A10: k in W and A11: k in V by XBOOLE_0:3; consider i being set such that A12: i in dom (netmap ((commute (N,x,(Omega Y))),(Omega Y))) and A13: k = (netmap ((commute (N,x,(Omega Y))),(Omega Y))) . i by A10, FUNCT_1:def_3; ContMaps (X,(Omega Y)) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3; then A14: the carrier of (ContMaps (X,(Omega Y))) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def_13; then RelStr(# the carrier of (commute (N,x,(Omega Y))), the InternalRel of (commute (N,x,(Omega Y))) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3; then reconsider i = i as Element of N by A12; reconsider g = N . i as Function of X,(Omega Y) by WAYBEL24:21; A15: dom g = the carrier of X by FUNCT_2:def_1; A16: g " V in { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } ; (netmap ((commute (N,x,(Omega Y))),(Omega Y))) . i = ((commute the mapping of N) . x) . i by A14, Def3 .= ( the mapping of N . i) . x by A7, FUNCT_6:56 ; then x in g " V by A11, A13, A15, FUNCT_1:def_7; hence x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } by A16, TARSKI:def_4; ::_thesis: verum end; assume x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } ; ::_thesis: x in f " V then consider Z being set such that A17: x in Z and A18: Z in { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } by TARSKI:def_4; consider A being Subset of X such that A19: Z = A and A20: ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) by A18; consider i being Element of N, g being Function of X,(Omega Y) such that A21: g = N . i and A22: A = g " V by A20; A23: g . x in V by A17, A19, A22, FUNCT_1:def_7; A24: for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) proof let x be Point of X; ::_thesis: ex_sup_of commute (N,x,(Omega Y)) commute (N,x,(Omega Y)) is eventually-directed by A1; hence ex_sup_of commute (N,x,(Omega Y)) by Th31; ::_thesis: verum end; reconsider x = x as Element of X by A17, A19; the mapping of N . i in rng the mapping of N by A3, FUNCT_1:def_3; then g <= fo by A21, A24, Th26, Th40; then ex a, b being Element of (Omega Y) st ( a = g . x & b = fo . x & a <= b ) by YELLOW_2:def_1; then consider O being Subset of Y such that A25: O = {(f . x)} and A26: g . x in Cl O by Def2; V meets O by A5, A23, A26, PRE_TOPC:def_7; then consider w being set such that A27: w in V /\ O by XBOOLE_0:4; w in O by A27, XBOOLE_0:def_4; then A28: w = f . x by A25, TARSKI:def_1; w in V by A27, XBOOLE_0:def_4; hence x in f " V by A6, A28, FUNCT_1:def_7; ::_thesis: verum end; then A29: f " V = union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } by TARSKI:1; { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } c= bool the carrier of X proof let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } or m in bool the carrier of X ) assume m in { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } ; ::_thesis: m in bool the carrier of X then ex A being Subset of X st ( m = A & ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) ) ; hence m in bool the carrier of X ; ::_thesis: verum end; then reconsider M = { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) } as Subset-Family of X ; reconsider M = M as Subset-Family of X ; M is open proof let P be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not P in M or P is open ) assume P in M ; ::_thesis: P is open then consider A being Subset of X such that A30: P = A and A31: ex i being Element of N ex g being Function of X,(Omega Y) st ( g = N . i & A = g " V ) ; consider i being Element of N, g being Function of X,(Omega Y) such that A32: g = N . i and A33: A = g " V by A31; consider g9 being Function of X,(Omega Y) such that A34: g = g9 and A35: g9 is continuous by A32, WAYBEL24:def_3; TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) ; then reconsider g99 = g9 as continuous Function of X,Y by A2, A35, YELLOW12:36; [#] Y <> {} ; then g99 " V is open by A5, TOPS_2:43; hence P is open by A30, A33, A34; ::_thesis: verum end; hence f " V is open by A29, TOPS_2:19; ::_thesis: verum end; [#] Y <> {} ; hence "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y by A4, TOPS_2:43; ::_thesis: verum end; theorem :: WAYBEL25:43 for X being non empty TopSpace for Y being monotone-convergence T_0-TopSpace holds ContMaps (X,(Omega Y)) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X proof let X be non empty TopSpace; ::_thesis: for Y being monotone-convergence T_0-TopSpace holds ContMaps (X,(Omega Y)) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X let Y be monotone-convergence T_0-TopSpace; ::_thesis: ContMaps (X,(Omega Y)) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X set L = (Omega Y) |^ the carrier of X; reconsider C = ContMaps (X,(Omega Y)) as non empty full SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3; C is directed-sups-inheriting proof let D be directed Subset of C; :: according to WAYBEL_0:def_4 ::_thesis: ( D = {} or not ex_sup_of D,(Omega Y) |^ the carrier of X or "\/" (D,((Omega Y) |^ the carrier of X)) in the carrier of C ) assume that A1: D <> {} and ex_sup_of D,(Omega Y) |^ the carrier of X ; ::_thesis: "\/" (D,((Omega Y) |^ the carrier of X)) in the carrier of C reconsider D = D as non empty directed Subset of C by A1; set N = Net-Str D; A2: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) ; for x being Point of X holds commute ((Net-Str D),x,(Omega Y)) is eventually-directed ; then A3: "\/" ((rng the mapping of (Net-Str D)),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y by Th42; TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) by Def2; then "\/" ((rng the mapping of (Net-Str D)),((Omega Y) |^ the carrier of X)) is continuous Function of X,(Omega Y) by A2, A3, YELLOW12:36; then A4: "\/" ((rng the mapping of (Net-Str D)),((Omega Y) |^ the carrier of X)) in the carrier of C by WAYBEL24:def_3; Net-Str D = NetStr(# D,( the InternalRel of C |_2 D),((id the carrier of C) | D) #) by WAYBEL17:def_4; hence "\/" (D,((Omega Y) |^ the carrier of X)) in the carrier of C by A4, YELLOW14:2; ::_thesis: verum end; hence ContMaps (X,(Omega Y)) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X ; ::_thesis: verum end;