### The Mizar article:

### Injective Spaces. Part II

**by****Artur Kornilowicz, and****Jaroslaw Gryko**

- Received July 3, 1999
Copyright (c) 1999 Association of Mizar Users

- MML identifier: WAYBEL25
- [ MML identifier index ]

environ vocabulary PRE_TOPC, WAYBEL18, BOOLE, SUBSET_1, URYSOHN1, BHSP_3, WAYBEL11, METRIC_1, WAYBEL_9, FUNCTOR0, T_0TOPSP, YELLOW_9, CARD_3, FUNCOP_1, YELLOW_1, RELAT_1, RLVECT_2, FUNCT_1, ORDERS_1, WAYBEL_0, CAT_1, TOPS_2, ORDINAL2, WELLORD1, GROUP_6, FUNCT_3, WAYBEL_1, BORSUK_1, LATTICES, QUANTAL1, LATTICE3, YELLOW_0, WAYBEL_3, RELAT_2, PROB_1, BINOP_1, SEQM_3, WAYBEL24, FUNCT_2, GROUP_1, PRALG_2, PRALG_1, YELLOW_2, REALSET1, CONNSP_2, TOPS_1, SEQ_2, COMPTS_1, YELLOW_8, TARSKI, SETFAM_1, WAYBEL25; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, REALSET1, NATTRA_1, TOLER_1, QUANTAL1, CARD_3, PRALG_1, PRALG_2, PRE_CIRC, WAYBEL18, STRUCT_0, PRE_TOPC, GRCAT_1, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, TMAP_1, T_0TOPSP, URYSOHN1, BORSUK_3, ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_2, YELLOW_6, WAYBEL_3, YELLOW_8, WAYBEL_9, WAYBEL11, YELLOW_9, WAYBEL17, YELLOW_1, WAYBEL24, YELLOW14; constructors BORSUK_3, CANTOR_1, ENUMSET1, GRCAT_1, NATTRA_1, ORDERS_3, PRALG_2, QUANTAL1, RELAT_2, TMAP_1, TOLER_1, TOPS_1, TOPS_2, URYSOHN1, WAYBEL_1, WAYBEL_8, WAYBEL17, WAYBEL24, YELLOW_8, YELLOW_9, YELLOW14, MONOID_0, MEMBERED; clusters BORSUK_3, FUNCT_1, LATTICE3, PRALG_1, PRE_TOPC, RELSET_1, STRUCT_0, TEX_1, TSP_1, TOPS_1, YELLOW_0, YELLOW_1, YELLOW_9, YELLOW12, WAYBEL_0, WAYBEL_2, WAYBEL_8, WAYBEL10, WAYBEL12, WAYBEL17, WAYBEL18, WAYBEL19, WAYBEL21, WAYBEL24, YELLOW14, SUBSET_1, BORSUK_1, MEMBERED, ZFMISC_1, FUNCT_2; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_2, ORDERS_1, RELAT_1, RELAT_2, STRUCT_0, WAYBEL_1, T_0TOPSP, WAYBEL18, LATTICE3, YELLOW_6, WAYBEL_0, WAYBEL_9, CONNSP_2, YELLOW14; theorems TARSKI, PRE_TOPC, ZFMISC_1, STRUCT_0, ORDERS_1, T_0TOPSP, FUNCT_1, FUNCT_2, QUANTAL1, RELAT_1, FINSEQ_5, TEX_1, PBOOLE, PRALG_1, FUNCOP_1, CARD_3, BORSUK_1, WELLORD1, WAYBEL14, TOPS_1, TOPS_2, TOPS_3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_4, YELLOW_6, YELLOW_9, YELLOW12, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_7, WAYBEL_9, WAYBEL11, LATTICE3, WAYBEL10, WAYBEL13, WAYBEL15, WAYBEL17, WAYBEL18, WAYBEL20, WAYBEL24, CONNSP_2, WAYBEL_3, PRALG_2, FUNCT_5, WAYBEL_8, TOPMETR, GRCAT_1, TSEP_1, EQUATION, TOPGRP_1, WAYBEL21, FRECHET2, ENUMSET1, YELLOW14, RELSET_1, SETFAM_1, XBOOLE_0, XBOOLE_1; schemes FUNCT_2, RELSET_1; begin :: Injective spaces theorem for p being Point of Sierpinski_Space st p = 0 holds {p} is closed proof set S = Sierpinski_Space; let p be Point of S; assume A1: p = 0; A2: the carrier of S = {0,1} by WAYBEL18:def 9; A3: the topology of S = {{}, {1}, {0,1}} by WAYBEL18:def 9; [#]S \ {p} = {1} proof thus [#]S \ {p} c= {1} proof let a be set; assume a in [#]S \ {p}; then a in [#]S & not a in {p} by XBOOLE_0:def 4; then a in the carrier of S & a <> 0 by A1,TARSKI:def 1; then a = 1 by A2,TARSKI:def 2; hence a in {1} by TARSKI:def 1; end; let a be set; assume a in {1}; then a = 1 by TARSKI:def 1; then a in the carrier of S & a <> 0 by A2,TARSKI:def 2; then a in [#]S & not a in {p} by A1,PRE_TOPC:12,TARSKI:def 1; hence thesis by XBOOLE_0:def 4; end; hence [#]S \ {p} in the topology of S by A3,ENUMSET1:14; end; theorem Th2: for p being Point of Sierpinski_Space st p = 1 holds {p} is non closed proof set S = Sierpinski_Space; let p be Point of S; assume A1: p = 1; A2: the carrier of S = {0,1} by WAYBEL18:def 9; A3: the topology of S = {{}, {1}, {0,1}} by WAYBEL18:def 9; A4: {0} <> {1} & {0} <> {0,1} by ZFMISC_1:6,9; [#]S \ {p} = {0} proof thus [#]S \ {p} c= {0} proof let a be set; assume a in [#]S \ {p}; then a in [#]S & not a in {p} by XBOOLE_0:def 4; then a in the carrier of S & a <> 1 by A1,TARSKI:def 1; then a = 0 by A2,TARSKI:def 2; hence a in {0} by TARSKI:def 1; end; let a be set; assume a in {0}; then a = 0 by TARSKI:def 1; then a in the carrier of S & a <> 1 by A2,TARSKI:def 2; then a in [#]S & not a in {p} by A1,PRE_TOPC:12,TARSKI:def 1; hence thesis by XBOOLE_0:def 4; end; hence not [#]S \ {p} in the topology of S by A3,A4,ENUMSET1:13; end; definition cluster Sierpinski_Space -> non being_T1; coherence proof set S = Sierpinski_Space; ex p being Point of S st Cl {p} <> {p} proof the carrier of S = {0,1} by WAYBEL18:def 9; then reconsider p = 1 as Point of S by TARSKI:def 2; take p; thus thesis by Th2; end; hence thesis by FRECHET2:47; end; end; definition cluster complete Scott -> discerning TopLattice; coherence by WAYBEL11:10; end; definition cluster injective strict T_0-TopSpace; existence proof take Sierpinski_Space; thus thesis; end; end; definition cluster complete Scott strict TopLattice; existence proof consider T being complete Scott strict TopLattice; take T; thus thesis; end; end; theorem Th3: :: see WAYBEL18:16 for I being non empty set, T being Scott TopAugmentation of product(I --> BoolePoset 1) holds the carrier of T = the carrier of product(I --> Sierpinski_Space) proof let I be non empty set, T be Scott TopAugmentation of product(I --> BoolePoset 1); set S = Sierpinski_Space, B = BoolePoset 1; A1: dom Carrier (I --> B) = I by PBOOLE:def 3; A2: dom Carrier (I --> S) = I by PBOOLE:def 3; A3: for x being set st x in dom Carrier (I --> S) holds (Carrier (I --> B)).x = (Carrier (I --> S)).x proof let x be set; assume A4: x in dom Carrier (I --> S); then consider R being 1-sorted such that A5: R = (I --> B).x & (Carrier (I --> B)).x = the carrier of R by A2,PRALG_1:def 13; consider T being 1-sorted such that A6: T = (I --> S).x & (Carrier (I --> S)).x = the carrier of T by A2,A4,PRALG_1:def 13; thus (Carrier (I --> B)).x = the carrier of B by A2,A4,A5,FUNCOP_1:13 .= bool 1 by WAYBEL_7:4 .= the carrier of S by WAYBEL18:def 9,YELLOW14:1 .= (Carrier (I --> S)).x by A2,A4,A6,FUNCOP_1:13; end; the RelStr of T = the RelStr of product(I --> B) by YELLOW_9:def 4; hence the carrier of T = product Carrier (I --> B) by YELLOW_1:def 4 .= product Carrier (I --> S) by A1,A2,A3,FUNCT_1:9 .= the carrier of product(I --> S) by WAYBEL18:def 3; end; theorem Th4: for L1, L2 being complete LATTICE, T1 being Scott TopAugmentation of L1, T2 being Scott TopAugmentation of L2, h being map of L1, L2, H being map of T1, T2 st h = H & h is isomorphic holds H is_homeomorphism proof let L1, L2 be complete LATTICE, T1 be Scott TopAugmentation of L1, T2 be Scott TopAugmentation of L2, h be map of L1, L2, H be map of T1, T2 such that A1: h = H and A2: h is isomorphic; A3: the RelStr of L1 = the RelStr of T1 by YELLOW_9:def 4; A4: the RelStr of L2 = the RelStr of T2 by YELLOW_9:def 4; A5: h is one-to-one by A2,WAYBEL_0:66; A6: rng h = the carrier of L2 by A2,WAYBEL_0:66 .= [#]L2 by PRE_TOPC:12; consider g being map of L2,L1 such that A7: g = h"; g = (h qua Function)" by A5,A6,A7,TOPS_2:def 4; then A8: g is isomorphic by A2,WAYBEL_0:68; reconsider h1 = h as sups-preserving map of L1,L2 by A2,WAYBEL13:20; reconsider h2 = h" as sups-preserving map of L2,L1 by A7,A8,WAYBEL13:20; A9: h1 is directed-sups-preserving; A10: h2 is directed-sups-preserving; reconsider H' = h" as map of T2, T1 by A3,A4; H is directed-sups-preserving by A1,A3,A4,A9,WAYBEL21:6; then A11: H is continuous by WAYBEL17:22; H' is directed-sups-preserving by A3,A4,A10,WAYBEL21:6; then A12: H' is continuous by WAYBEL17:22; A13: dom H = the carrier of T1 by FUNCT_2:def 1 .= [#]T1 by PRE_TOPC:12; A14: rng H = the carrier of T2 by A1,A2,A4,WAYBEL_0:66 .= [#]T2 by PRE_TOPC:12; A15: H is one-to-one by A1,A2,WAYBEL_0:66; A16: dom (H") = the carrier of T2 by FUNCT_2:def 1 .= dom H' by FUNCT_2:def 1; for x being set st x in dom H' holds H'.x = H".x proof let x be set; assume x in dom H'; thus H'.x = (h qua Function)".x by A5,A6,TOPS_2:def 4 .= H".x by A1,A5,A14,TOPS_2:def 4; end; then H" = H' by A16,FUNCT_1:9; hence H is_homeomorphism by A11,A12,A13,A14,A15,TOPS_2:def 5; end; theorem Th5: for L1, L2 being complete LATTICE, T1 being Scott TopAugmentation of L1, T2 being Scott TopAugmentation of L2 st L1, L2 are_isomorphic holds T1, T2 are_homeomorphic proof let L1, L2 be complete LATTICE, T1 be Scott TopAugmentation of L1, T2 be Scott TopAugmentation of L2; given h being map of L1, L2 such that A1: h is isomorphic; the RelStr of L1 = the RelStr of T1 & the RelStr of L2 = the RelStr of T2 by YELLOW_9:def 4; then reconsider H = h as map of T1, T2 ; take H; thus thesis by A1,Th4; end; theorem Th6: 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 such that A1: S is injective and A2: S, T are_homeomorphic; consider p being map of S,T such that A3: p is_homeomorphism by A2,T_0TOPSP:def 1; A4: p is continuous by A3,TOPS_2:def 5; let X be non empty TopSpace, f be map of X, T; assume A5: f is continuous; let Y be non empty TopSpace; assume A6: X is SubSpace of Y; set F = p"*f; p" is continuous by A3,TOPS_2:def 5; then F is continuous by A5,TOPS_2:58; then consider G being map of Y,S such that A7: G is continuous and A8: G|(the carrier of X) = F by A1,A6,WAYBEL18:def 5; take g = p*G; thus g is continuous by A4,A7,TOPS_2:58; [#]X c= [#]Y by A6,PRE_TOPC:def 9; then the carrier of X c= [#]Y by PRE_TOPC:12; then A9: the carrier of X c= the carrier of Y by PRE_TOPC:12; A10: rng p = [#]T & p is one-to-one by A3,TOPS_2:72; A11: dom f = the carrier of X by FUNCT_2:def 1 .= (the carrier of Y) /\ (the carrier of X) by A9,XBOOLE_1:28 .= dom g /\ (the carrier of X) by FUNCT_2:def 1; for x being set st x in dom f holds g.x = f.x proof let x be set; assume A12: x in dom f; then x in the carrier of X; then x in the carrier of Y by A9; then A13: x in dom G by FUNCT_2:def 1; A14: f.x in rng f by A12,FUNCT_1:def 5; then f.x in the carrier of T; then A15: f.x in dom (p") by FUNCT_2:def 1; thus g.x = p.(G.x) by A13,FUNCT_1:23 .= p.((p"*f).x) by A8,A12,FUNCT_1:72 .= p.(p".(f.x)) by A12,FUNCT_1:23 .= (p*p").(f.x) by A15,FUNCT_1:23 .= (id [#]T).(f.x) by A10,TOPS_2:65 .= (id the carrier of T).(f.x) by PRE_TOPC:12 .= f.x by A14,FUNCT_1:34; end; hence g|(the carrier of X) = f by A11,FUNCT_1:68; end; theorem for L1, L2 being complete LATTICE, T1 being Scott TopAugmentation of L1, T2 being Scott TopAugmentation of L2 st L1, L2 are_isomorphic & T1 is injective holds T2 is injective proof let L1, L2 be complete LATTICE, T1 be Scott TopAugmentation of L1, T2 be Scott TopAugmentation of L2 such that A1: L1, L2 are_isomorphic and A2: T1 is injective; T1, T2 are_homeomorphic by A1,Th5; hence thesis by A2,Th6; end; definition let X, Y be non empty TopSpace; redefine pred X is_Retract_of Y means :Def1: ex c being continuous map of X, Y, r being continuous map of Y, X st r * c = id X; compatibility proof thus X is_Retract_of Y implies ex c being continuous map of X, Y, r being continuous map of Y, X st r * c = id X proof given f being map of Y, Y such that A1: f is continuous and A2: f*f = f and A3: Image f, X are_homeomorphic; consider h being map of Image f, X such that A4: h is_homeomorphism by A3,T_0TOPSP:def 1; h" is continuous by A4,TOPS_2:def 5; then reconsider c = incl Image f * h" as continuous map of X, Y by TOPS_2 :58; h is continuous & corestr f is continuous by A1,A4,TOPS_2:def 5,WAYBEL18:11; then reconsider r = h * corestr f as continuous map of Y, X by TOPS_2:58; take c, r; A5: rng h = [#]X & h is one-to-one by A4,TOPS_2:def 5; thus r * c = h * (corestr f * (incl Image f * h")) by RELAT_1:55 .= h * (corestr f * incl Image f * h") by RELAT_1:55 .= h * (id Image f * h") by A2,YELLOW14:36 .= h * h" by GRCAT_1:12 .= id rng h by A5,TOPS_2:65 .= id the carrier of X by A5,PRE_TOPC:12 .= id X by GRCAT_1:def 11; end; given c being continuous map of X, Y, r being continuous map of Y, X such that A6: r * c = id X; take f = c * r; thus f is continuous; thus f * f = c * (r * (c * r)) by RELAT_1:55 .= c * (id X * r) by A6,RELAT_1:55 .= f by GRCAT_1:12; A7: r * c = id the carrier of X by A6,GRCAT_1:def 11; A8: dom c = the carrier of X by FUNCT_2:def 1 .= rng r by A7,FUNCT_2:24; A9: Image f = Y|rng f by WAYBEL18:def 6 .= Y|rng c by A8,RELAT_1:47 .= Image c by WAYBEL18:def 6; then reconsider cf = corestr c as map of X, Image f; take h = cf"; thus dom h = the carrier of Image f by FUNCT_2:def 1 .= [#]Image f by PRE_TOPC:12; A10: rng corestr c = the carrier of Image c by FUNCT_2:def 3 .= [#]Image c by PRE_TOPC:12; c is one-to-one by A7,FUNCT_2:29; then A11: corestr c is one-to-one by WAYBEL18:def 7; hence rng h = [#]X by A9,A10,TOPS_2:62; (corestr c) qua Function" is one-to-one by A11,FUNCT_1:62; hence h is one-to-one by A9,A10,A11,TOPS_2:def 4; A12: corestr c is continuous by WAYBEL18:11; r * cf * cf" = id X * cf" by A6,WAYBEL18:def 7; then r * (cf * cf") = id X * cf" by RELAT_1:55; then r * id rng cf = id X * cf" by A9,A10,A11,TOPS_2:65; then r * id the carrier of Image c = id X * cf" by A10,PRE_TOPC:12; then r * id Image c = id X * cf" by GRCAT_1:def 11; then A13: r * id Image c = cf" by GRCAT_1:12; the carrier of Image c c= the carrier of Y by BORSUK_1:35; then id Image c is Function of the carrier of Image c, the carrier of Y by FUNCT_2:9; then r * id Image c is Function of the carrier of Image c, the carrier of X by FUNCT_2:19; then reconsider q = r * id Image c as map of Image f, X by A9; for P being Subset of X st P is open holds q"P is open proof let P be Subset of X; assume A14: P is open; A15: q"P = (id Image c)"(r"P) by RELAT_1:181; r"P is open by A14,TOPS_2:55; then A16: r"P in the topology of Y by PRE_TOPC:def 5; A17: dom id Image c = the carrier of Image c by FUNCT_2:def 1 .= [#]Image c by PRE_TOPC:12; (id Image c)"(r"P) = (r"P) /\ [#]Image c proof thus (id Image c)"(r"P) c= (r"P) /\ [#]Image c proof let a be set; assume A18: a in (id Image c)"(r"P); then A19: a in dom id Image c by FUNCT_1:def 13; (id Image c).a in r"P by A18,FUNCT_1:def 13; then a in r"P by A18,GRCAT_1:11; hence a in (r"P) /\ [#]Image c by A17,A19,XBOOLE_0:def 3; end; let a be set; assume a in (r"P) /\ [#]Image c; then A20: a in r"P & a in [#]Image c by XBOOLE_0:def 3; then (id Image c).a in r"P by GRCAT_1:11; hence thesis by A17,A20,FUNCT_1:def 13; end; hence q"P in the topology of Image f by A9,A15,A16,PRE_TOPC:def 9; end; hence h is continuous by A13,TOPS_2:55; thus h" is continuous by A9,A10,A11,A12,TOPS_2:64; end; end; theorem Th8: for S, T, X, Y being non empty TopSpace st the TopStruct of S = the TopStruct of T & the TopStruct of X = the TopStruct of Y & S is_Retract_of X holds T is_Retract_of Y proof let S, T, X, Y be non empty TopSpace such that A1: the TopStruct of S = the TopStruct of T and A2: the TopStruct of X = the TopStruct of Y; given c being continuous map of S, X, r being continuous map of X, S such that A3: r * c = id S; reconsider cc = c as continuous map of T, Y by A1,A2,YELLOW12:36; reconsider rr = r as continuous map of Y, T by A1,A2,YELLOW12:36; take cc, rr; id S = id the carrier of S & id T = id the carrier of T by GRCAT_1:def 11 ; hence thesis by A1,A3; end; theorem 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 such that A1: S1, S2 are_homeomorphic and A2: S1 is_Retract_of T; consider G being map of S1,S2 such that A3: G is_homeomorphism by A1,T_0TOPSP:def 1; consider H being map 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; consider F being map of Image H,S1 such that A7: F is_homeomorphism by A6,T_0TOPSP:def 1; G*F is_homeomorphism by A3,A7,TOPS_2:71; hence thesis by A4,A5,T_0TOPSP:def 1; end; theorem 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 such that A1: T is injective and A2: S is_Retract_of T; consider h being map 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; A6: corestr h is continuous by A3,WAYBEL18:11; set F = corestr h; for W being Point of T st W in the carrier of Image h holds F.W = W proof let W be Point of T; assume W in the carrier of Image h; then W in rng h by WAYBEL18:10; then consider x being set such that A7: x in dom h and A8: W = h.x by FUNCT_1:def 5; thus F.W = h.(h.x) by A8,WAYBEL18:def 7 .= W by A4,A7,A8,FUNCT_1:23; end; then F is_a_retraction by BORSUK_1:def 19; then Image h is_a_retract_of T by A6,BORSUK_1:def 20; then Image h is injective by A1,WAYBEL18:9; hence S is injective by A5,Th6; end; ::p.126 exercise 3.13, 1 => 2 theorem for J being injective non empty TopSpace, Y being non empty TopSpace st J is SubSpace of Y holds J is_Retract_of Y proof let J be injective non empty TopSpace, Y be non empty TopSpace; assume A1: J is SubSpace of Y; then consider f being map 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:35; then f is Function of the carrier of Y, the carrier of Y by FUNCT_2:9; then reconsider ff = f as map of Y, Y ; ex ff being map of Y, Y st ff is continuous & ff*ff = ff & Image ff, J are_homeomorphic proof take ff; thus ff is continuous by A1,A2,TOPMETR:7; A5: dom (ff*ff) = the carrier of Y by FUNCT_2:def 1; A6: dom f = the carrier of Y by FUNCT_2:def 1; for x being set st x in the carrier of Y holds (f*f).x = f.x proof let x be set; assume A7: x in the carrier of Y; then A8: f.x in the carrier of J by FUNCT_2:7; thus (f*f).x = f.(f.x) by A6,A7,FUNCT_1:23 .= (id J).(f.x) by A3,A8,FUNCT_1:72 .= f.x by A8,GRCAT_1:11; end; hence ff*ff = ff by A5,A6,FUNCT_1:9; A9: rng f = the carrier of J proof thus rng f c= the carrier of J; let y be set; assume A10: y in the carrier of J; then y in the carrier of Y by A4; then A11: y in dom f by FUNCT_2:def 1; f.y = (f|(the carrier of J)).y by A10,FUNCT_1:72 .= y by A3,A10,GRCAT_1:11; hence y in rng f by A11,FUNCT_1:def 5; end; reconsider M = [#]J as non empty Subset of Y by A4,PRE_TOPC:12; A12: the carrier of Y|M = [#](Y|M) by PRE_TOPC:12 .= M by PRE_TOPC:def 10 .= the carrier of J by PRE_TOPC:12; Image ff = Y|rng ff by WAYBEL18:def 6 .= Y|M by A9,PRE_TOPC:12 .= the TopStruct of J by A1,A12,TSEP_1:5; hence Image ff, J are_homeomorphic by YELLOW14:20; end; hence thesis by WAYBEL18:def 8; end; :: p.123 proposition 3.5 :: p.124 theorem 3.8 (i, part a) :: p.126 exercise 3.14 theorem Th12: for L being complete continuous LATTICE, T being Scott TopAugmentation of L holds T is injective proof let L be complete continuous LATTICE, T be Scott TopAugmentation of L; let X be non empty TopSpace, f be map of X, T such that A1: f is continuous; let Y be non empty TopSpace such that A2: X is SubSpace of Y; deffunc F(set) = "\/" ({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 = F(x) from LambdaD; reconsider g as map of Y, T ; take g; for P being Subset of T st P is open holds g"P is open proof let P be Subset of T; assume P is open; then reconsider 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; thus x in g"P implies ex Q being Subset of Y st Q is open & Q c= g"P & x in Q proof assume A4: x in g"P; then reconsider y = x as Point of Y; A5: g.y in P by A4,FUNCT_2:46; set A = {inf (f.: (V /\ the carrier of X)) where V is open Subset of Y: y in V}; A c= the carrier of T proof let a be set; assume a in A; then ex V being open Subset of Y st a = inf (f.:(V /\ the carrier of X)) & y in V; hence thesis; end; then reconsider A as Subset of T; A6: g.y = sup A by A3; the carrier of Y = [#]Y by PRE_TOPC:12; then A7: inf (f.:([#]Y /\ the carrier of X)) in A; A is directed proof let a, b be Element of T; assume a in A; then consider Va being open Subset of Y such that A8: a = inf (f.:(Va /\ the carrier of X)) and A9: y in Va; assume b in A; then consider Vb being open Subset of Y such that A10: b = inf (f.:(Vb /\ the carrier of X)) and A11: y in Vb; take inf (f.:(Va /\ Vb /\ the carrier of X)); A12: Va /\ Vb is open by TOPS_1:38; y in Va /\ Vb by A9,A11,XBOOLE_0:def 3; hence inf (f.:(Va /\ Vb /\ the carrier of X)) in A by A12; Va /\ Vb c= Va & Va /\ Vb c= Vb by XBOOLE_1:17; then Va /\ Vb /\ the carrier of X c= Va /\ the carrier of X & Va /\ Vb /\ the carrier of X c= Vb /\ the carrier of X by XBOOLE_1:26; then f.:(Va /\ Vb /\ the carrier of X) c= f.:(Va /\ the carrier of X) & f.:(Va /\ Vb /\ the carrier of X) c= f.:(Vb /\ the carrier of X) by RELAT_1:156; hence thesis by A8,A10,WAYBEL_7:3; end; then A meets P by A5,A6,A7,WAYBEL11:def 1; then consider b being set such that A13: b in A and A14: b in P by XBOOLE_0:3; consider B being open Subset of Y such that A15: b = inf (f.:(B /\ the carrier of X)) and A16: y in B by A13; reconsider b as Element of T by A15; take B; thus B is open; thus B c= g"P proof let a be set; assume A17: a in B; then reconsider a as Point of Y; A18: g.a = F(a) by A3; b in {inf (f.:(V /\ the carrier of X)) where V is open Subset of Y : a in V} by A15,A17; then b <= g.a by A18,YELLOW_2:24; then g.a in P by A14,WAYBEL_0:def 20; hence thesis by FUNCT_2:46; end; thus x in B by A16; end; thus thesis; end; hence thesis by TOPS_1:57; end; hence g is continuous by TOPS_2:55; set gX = g|(the carrier of X); A19: the carrier of X c= the carrier of Y by A2,BORSUK_1:35; A20: dom gX = dom g /\ the carrier of X by RELAT_1:90 .= (the carrier of Y) /\ the carrier of X by FUNCT_2:def 1 .= the carrier of X by A19,XBOOLE_1:28; A21: dom f = the carrier of X by FUNCT_2:def 1; for a being set st a in the carrier of X holds gX.a = f.a proof let a be set; assume A22: a in the carrier of X; then reconsider x = a as Point of X; reconsider y = x as Point of Y by A19,A22; set A = {inf (f.:(V /\ the carrier of X)) where V is open Subset of Y: y in V}; A c= the carrier of T proof let a be set; assume a in A; then ex V being open Subset of Y st a = inf (f.:(V /\ the carrier of X )) & y in V; hence thesis; end; then reconsider A as Subset of T; A23: f.x is_>=_than A proof let z be Element of T; assume z in A; then consider V being open Subset of Y such that A24: z = inf (f.:(V /\ the carrier of X)) and A25: y in V; A26: ex_inf_of f.:(V /\ the carrier of X),T by YELLOW_0:17; y in V /\ the carrier of X by A25,XBOOLE_0:def 3; then f.x in f.:(V /\ the carrier of X) by FUNCT_2:43; hence z <= f.x by A24,A26,YELLOW_4:2; end; A27: for b being Element of T st b is_>=_than A holds f.x <= b proof let b be Element of T such that A28: for k being Element of T st k in A holds k <= b; A29: for V being open Subset of X st x in V holds inf (f.:V) <= b proof let V be open Subset of X; assume A30: x in V; V in the topology of X by PRE_TOPC:def 5; 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 9; reconsider Q as open Subset of Y by A31,PRE_TOPC:def 5 ; A33: y in Q by A30,A32,XBOOLE_0:def 3; A34: V = Q /\ the carrier of X by A32,PRE_TOPC:12; inf (f.:(Q /\ the carrier of X)) in A by A33; hence thesis by A28,A34; end; A35: b is_>=_than waybelow f.x proof let w be Element of T; assume w in waybelow f.x; then w << f.x by WAYBEL_3:7; then f.x in wayabove w by WAYBEL_3:8; then A36: x in f"wayabove w by FUNCT_2:46; wayabove w is open by WAYBEL11:36; then f"wayabove w is open by A1,TOPS_2:55; then A37: inf (f.:f"wayabove w) <= b by A29,A36; A38: ex_inf_of wayabove w,T & ex_inf_of f.:f"wayabove w,T by YELLOW_0:17; f.:f"wayabove w c= wayabove w by FUNCT_1:145; then A39: inf wayabove w <= inf (f.:f"wayabove w) by A38,YELLOW_0:35; w <= inf wayabove w by WAYBEL14:9; then w <= inf (f.:f"wayabove w) by A39,ORDERS_1:26; hence w <= b by A37,ORDERS_1:26; end; f.x = sup waybelow f.x by WAYBEL_3:def 5; hence f.x <= b by A35,YELLOW_0:32; end; thus gX.a = g.y by FUNCT_1:72 .= F(y) by A3 .= f.a by A23,A27,YELLOW_0:30; end; hence g|(the carrier of X) = f by A20,A21,FUNCT_1:9; end; definition let L be complete continuous LATTICE; cluster Scott -> injective TopAugmentation of L; coherence by Th12; end; definition let T be injective non empty TopSpace; cluster the TopStruct of T -> injective; coherence by WAYBEL18:17; end; begin :: Specialization order ::p.124 definition 3.6 definition let T be TopStruct; func Omega T -> strict TopRelStr means :Def2: the TopStruct of it = the TopStruct 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 proof defpred P[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 & P[x,y] from Rel_On_Set_Ex; take G = TopRelStr (# the carrier of T, R, the topology of T #); thus the TopStruct of G = the TopStruct of T; 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 proof let x, y be Element of G; hereby assume x <= y; then [x,y] in R by ORDERS_1:def 9; hence ex Y being Subset of T st Y = {y} & x in Cl Y by A1; end; given Y being Subset of T such that A2: Y = {y} & x in Cl Y; [x,y] in R by A1,A2; hence x <= y by ORDERS_1:def 9; end; end; uniqueness proof let R1,R2 be strict TopRelStr such that A3: the TopStruct of R1 = the TopStruct of T and A4: 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 A5: the TopStruct of R2 = the TopStruct of T and A6: for x,y being Element of R2 holds x <= y iff ex Y being Subset of T st Y = {y} & x in Cl Y; the InternalRel of R1 = the InternalRel of R2 proof let x,y be set; hereby assume A7: [x,y] in the InternalRel of R1; then A8: x in the carrier of R1 & y in the carrier of R1 by ZFMISC_1:106; then reconsider x1 = x, y1 = y as Element of R1; reconsider x2 = x, y2 = y as Element of R2 by A3,A5,A8; x1 <= y1 by A7,ORDERS_1:def 9; then consider Y being Subset of T such that A9: Y = {y1} & x1 in Cl Y by A4; x2 <= y2 by A6,A9; hence [x,y] in the InternalRel of R2 by ORDERS_1:def 9; end; assume A10: [x,y] in the InternalRel of R2; then A11: x in the carrier of R2 & y in the carrier of R2 by ZFMISC_1:106; then reconsider x2 = x, y2 = y as Element of R2; reconsider x1 = x, y1 = y as Element of R1 by A3,A5,A11; x2 <= y2 by A10,ORDERS_1:def 9; then consider Y being Subset of T such that A12: Y = {y2} & x2 in Cl Y by A6; x1 <= y1 by A4,A12; hence [x,y] in the InternalRel of R1 by ORDERS_1:def 9; end; hence thesis by A3,A5; end; end; Lm1: for T being TopStruct holds the carrier of T = the carrier of Omega T proof let T be TopStruct; the TopStruct of T = the TopStruct of Omega T by Def2; hence the carrier of T = the carrier of Omega T; end; Lm2: for T be TopStruct, a be set holds a is Subset of T iff a is Subset of Omega T by Lm1; definition let T be empty TopStruct; cluster Omega T -> empty; coherence proof the carrier of Omega T = the carrier of T by Lm1; hence the carrier of Omega T is empty; end; end; definition let T be non empty TopStruct; cluster Omega T -> non empty; coherence proof the carrier of Omega T = the carrier of T by Lm1; hence the carrier of Omega T is non empty; end; end; definition let T be TopSpace; cluster Omega T -> TopSpace-like; coherence proof A1: the TopStruct of Omega T = the TopStruct of T by Def2; hence the carrier of Omega T in the topology of Omega T by PRE_TOPC:def 1; thus thesis by A1,PRE_TOPC:def 1; end; end; definition let T be TopStruct; cluster Omega T -> reflexive; coherence proof let x be set; assume A1: x in the carrier of Omega T; the carrier of Omega T = the carrier of T by Lm1; then reconsider T' = T as non empty TopStruct by A1,STRUCT_0:def 1; reconsider t' = x as Element of T' by A1,Lm1; reconsider a = x as Element of Omega T by A1; consider Y being Subset of T such that A2: Y = {t'}; A3: Y c= Cl Y by PRE_TOPC:48; 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_1:def 9; end; end; Lm3: for T being TopStruct, x, y being Element of T, 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, x, y be Element of T, X, Y be Subset of T; assume A1: X = {x} & Y = {y}; hereby assume x in Cl Y; then for V being Subset of T st V is open holds (x in V implies y in V) by A1,YELLOW14:22; hence Cl X c= Cl Y by A1,YELLOW14:23; end; assume Cl X c= Cl Y; hence x in Cl Y by A1,YELLOW14:21; end; definition let T be TopStruct; cluster Omega T -> transitive; coherence proof let x, y, z be set; assume that A1: x in the carrier of Omega T & y in the carrier of Omega T & z in the carrier of Omega T and A2: [x,y] in the InternalRel of Omega T and A3: [y,z] in the InternalRel of Omega T; A4: the TopStruct of Omega T = the TopStruct of T by Def2; reconsider a = x, b = y, c = z as Element of Omega T by A1; reconsider t2=y, t3=z as Element of T by A1,A4; a <= b by A2,ORDERS_1:def 9; then consider Y2 being Subset of T such that A5: Y2 = {b} and A6: a in Cl Y2 by Def2; b <= c by A3,ORDERS_1:def 9; then consider Y3 being Subset of T such that A7: Y3 = {c} and A8: b in Cl Y3 by Def2; Y2 = {t2} & Y3 = {t3} by A5,A7; then Cl Y2 c= Cl Y3 by A8,Lm3; then a <= c by A6,A7,Def2; hence [x,z] in the InternalRel of Omega T by ORDERS_1:def 9; end; end; definition let T be T_0-TopSpace; cluster Omega T -> antisymmetric; coherence proof let x, y be set; assume that A1: x in the carrier of Omega T & y in the carrier of Omega T and A2: [x,y] in the InternalRel of Omega T and A3: [y,x] in the InternalRel of Omega T; reconsider a = x, b = y as Element of Omega T by A1; the TopStruct of Omega T = the TopStruct of T by Def2; then reconsider t1 = x, t2 = y as Element of T by A1; a <= b by A2,ORDERS_1:def 9; then consider Y2 being Subset of T such that A4: Y2 = {b} and A5: a in Cl Y2 by Def2; b <= a by A3,ORDERS_1:def 9; then consider Y1 being Subset of T such that A6: Y1 = {a} and A7: b in Cl Y1 by Def2; 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 A4,A5,A6,A7,YELLOW14:22; hence x = y by T_0TOPSP:def 7; end; end; theorem Th13: for S, T being TopSpace st the TopStruct of S = the TopStruct of T holds Omega S = Omega T proof let S, T be TopSpace such that A1: the TopStruct of S = the TopStruct of T; A2: the TopStruct of Omega S = the TopStruct of S by Def2 .= the TopStruct of Omega T by A1,Def2; the InternalRel of Omega S = the InternalRel of Omega T proof let a,b be set; thus [a,b] in the InternalRel of Omega S implies [a,b] in the InternalRel of Omega T proof assume A3: [a,b] in the InternalRel of Omega S; then a in the carrier of Omega S & b in the carrier of Omega S by ZFMISC_1:106; then reconsider s1 = a, s2 = b as Element of Omega S; reconsider t1 = s1, t2 = s2 as Element of Omega T by A2; s1 <= s2 by A3,ORDERS_1:def 9; then consider Y being Subset of S such that A4: Y = {s2} & s1 in Cl Y by Def2; reconsider Z = Y as Subset of T by A1; Z = {t2} & t1 in Cl Z by A1,A4,TOPS_3:80; then t1 <= t2 by Def2; hence thesis by ORDERS_1:def 9; end; assume A5: [a,b] in the InternalRel of Omega T; then a in the carrier of Omega T & b in the carrier of Omega T by ZFMISC_1:106; then reconsider s1 = a, s2 = b as Element of Omega T; reconsider t1 = s1, t2 = s2 as Element of Omega S by A2; s1 <= s2 by A5,ORDERS_1:def 9; then consider Y being Subset of T such that A6: Y = {s2} & s1 in Cl Y by Def2; reconsider Z = Y as Subset of S by A1; Z = {t2} & t1 in Cl Z by A1,A6,TOPS_3:80; then t1 <= t2 by Def2; hence thesis by ORDERS_1:def 9; end; hence Omega S = Omega T by A2; end; theorem for M being non empty set, T being non empty TopSpace holds the RelStr of Omega product(M --> T) = the RelStr of product(M --> Omega T) proof let M be non empty set, T be non empty TopSpace; A1: dom Carrier (M --> T) = M by PBOOLE:def 3 .= dom Carrier (M --> Omega T) by PBOOLE:def 3; 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; assume i in dom Carrier (M --> T); then A3: i in M by PBOOLE:def 3; 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:13 .= the carrier of Omega T by Lm1 .= the carrier of R2 by A3,A6,FUNCOP_1:13; hence (Carrier (M --> T)).i = (Carrier (M --> Omega T)).i by A5,A7; 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:9; then A9: the carrier of Omega product (M --> T) = the carrier of product (M --> Omega T) by YELLOW_1:def 4; A10: 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; hereby assume A11: [x,y] in the InternalRel of Omega product(M --> T); then A12: x in the carrier of Omega product(M --> T) & y in the carrier of Omega product(M --> T) by ZFMISC_1:106; then reconsider xo = x, yo = y as Element of Omega product(M --> T) ; reconsider p1 = x, p2 = y as Element of product(M --> T) by A10,A12; reconsider xp = x, yp = y as Element of product(M --> Omega T) by A9,A12; xo <= yo by A11,ORDERS_1:def 9; then consider Yp being Subset of product(M --> T) such that A13: Yp = {p2} and A14: p1 in Cl Yp by Def2; A15: xp in product Carrier (M --> Omega T) by A8,A11,ZFMISC_1:106; then consider f being Function such that A16: 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,A11,ZFMISC_1:106; then consider g being Function such that A17: 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; for i being set st i in M ex R being RelStr, 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; assume A18: i in M; then reconsider j = i as Element of M; A19: p1.j in Cl {p2.j} by A13,A14,YELLOW14:31; set t1 = p1.j, t2 = p2.j; t1 in the carrier of T & t2 in the carrier of T; then t1 in the carrier of Omega T & t2 in the carrier of Omega T by Lm1; then reconsider xi = t1, yi = t2 as Element of Omega T; take Omega T, xi, yi; thus Omega T = (M --> Omega T).i by A18,FUNCOP_1:13; thus xi = f.i by A16; thus yi = g.i by A17; thus xi <= yi by A19,Def2; end; then xp <= yp by A15,A16,A17,YELLOW_1:def 4; hence [x,y] in the InternalRel of product (M --> Omega T) by ORDERS_1:def 9; end; assume A20: [x,y] in the InternalRel of product (M --> Omega T); then A21: x in the carrier of product (M --> Omega T) & y in the carrier of product (M --> Omega T) by ZFMISC_1:106; then reconsider xp = x, yp = y as Element of product(M --> Omega T) ; reconsider xo = x, yo = y as Element of Omega product(M --> T) by A9,A21; reconsider p1 = x, p2 = y as Element of product(M --> T) by A9,A10,A21; A22: xp in product Carrier (M --> Omega T) by A21,YELLOW_1:def 4; xp <= yp by A20,ORDERS_1:def 9; then consider f, g being Function such that A23: f = xp and A24: g = yp and A25: for i being set st i in M ex R being RelStr, xi, yi being Element of R st R = (M --> Omega T).i & xi = f.i & yi = g.i & xi <= yi by A22,YELLOW_1:def 4; for i being Element of M holds p1.i in Cl {p2.i} proof let i be Element of M; consider R1 being RelStr, xi, yi being Element of R1 such that A26: R1 = (M --> Omega T).i and A27: xi = f.i & yi = g.i and A28: xi <= yi by A25; reconsider xi, yi as Element of Omega T by A26,FUNCOP_1:13; xi <= yi by A26,A28,FUNCOP_1:13; then ex Y being Subset of T st Y = {yi} & xi in Cl Y by Def2; hence p1.i in Cl {p2.i} by A23,A24,A27; end; then p1 in Cl {p2} by YELLOW14:31; then xo <= yo by Def2; hence [x,y] in the InternalRel of Omega product(M --> T) by ORDERS_1:def 9; end; hence thesis by A8,YELLOW_1:def 4; end; ::p.124 theorem 3.8 (i, part b) theorem Th15: for S being Scott complete TopLattice holds Omega S = the TopRelStr of S proof let S be Scott complete TopLattice; consider L being Scott TopAugmentation of S; A1: the RelStr of S = the RelStr of L by YELLOW_9:def 4; A2: the TopStruct of Omega S = the TopStruct of S by Def2; the InternalRel of Omega S = the InternalRel of S proof let x, y be set; hereby assume A3: [x,y] in the InternalRel of Omega S; then A4: x in the carrier of Omega S & y in the carrier of Omega S by ZFMISC_1:106; then reconsider o1 = x, o2 = y as Element of Omega S; o1 <= o2 by A3,ORDERS_1:def 9; then consider Y2 being Subset of S such that A5: Y2 = {o2} & o1 in Cl Y2 by Def2; x in the carrier of S & y in the carrier of S by A4,Lm1; then reconsider t1 = x, t2 = y as Element of S; t1 in downarrow t2 by A5,WAYBEL11:9; then t1 in downarrow {t2} by WAYBEL_0:def 17; then consider t3 being Element of S such that A6: t3 >= t1 & t3 in {t2} by WAYBEL_0:def 15; t1 <= t2 by A6,TARSKI:def 1; hence [x,y] in the InternalRel of S by ORDERS_1:def 9; end; assume A7: [x,y] in the InternalRel of S; then A8: x in the carrier of S & y in the carrier of S by ZFMISC_1:106; A9: x in the carrier of L & y in the carrier of L by A1,A7,ZFMISC_1:106; reconsider t1 = x, t2 = y as Element of S by A8; A10: t1 <= t2 by A7,ORDERS_1:def 9; t2 in {t2} by TARSKI:def 1; then t1 in downarrow {t2} by A10,WAYBEL_0:def 15; then t1 in downarrow t2 by WAYBEL_0:def 17; then A11: t1 in Cl {t2} by WAYBEL11:9; reconsider o1 = x, o2 = y as Element of Omega S by A1,A2,A9; o1 <= o2 by A11,Def2; hence [x,y] in the InternalRel of Omega S by ORDERS_1:def 9; end; hence thesis by A2; end; ::p.124 theorem 3.8 (i, part b) theorem Th16: for L being complete LATTICE, S being Scott TopAugmentation of L holds the RelStr of Omega S = the RelStr of L proof let L be complete LATTICE, S be Scott TopAugmentation of L; the TopRelStr of S = Omega S by Th15; hence thesis by YELLOW_9:def 4; end; definition let S be Scott complete TopLattice; cluster Omega S -> complete; coherence proof consider T being Scott TopAugmentation of S; A1: the RelStr of Omega T = the RelStr of S by Th16; the topology of S = sigma S by WAYBEL14:23 .= the topology of T by YELLOW_9:51; then the TopStruct of S = the TopStruct of T by A1,Lm1; then Omega S = Omega T by Th13; hence thesis by A1,YELLOW_0:3; end; end; theorem Th17: for T being non empty TopSpace, S being non empty SubSpace of T holds Omega S is full SubRelStr of Omega T proof let T be non empty TopSpace, S be non empty SubSpace of T; A1: the carrier of S c= the carrier of T by BORSUK_1:35; A2: the carrier of Omega S = the carrier of S by Lm1; A3: the carrier of Omega T = the carrier of T by Lm1; A4: the carrier of Omega S c= the carrier of Omega T by A1,A2,Lm1; A5: the InternalRel of Omega S c= the InternalRel of Omega T proof let x, y be set; assume A6: [x,y] in the InternalRel of Omega S; then A7: x in the carrier of Omega S & y in the carrier of Omega S by ZFMISC_1:106; then reconsider o1 = x, o2 = y as Element of Omega S; o1 <= o2 by A6,ORDERS_1:def 9; then consider Y2 being Subset of S such that A8: Y2 = {o2} and A9: o1 in Cl Y2 by Def2; reconsider s2 = y as Element of S by A2,A7; reconsider t2 = y as Element of T by A1,A2,A7; Cl {s2} = (Cl {t2}) /\ ([#]S) by PRE_TOPC:47; then A10: Cl {s2} c= Cl {t2} by XBOOLE_1:17; reconsider o3 = x, o4 = y as Element of Omega T by A1,A2,A3,A7; o3 <= o4 by A8,A9,A10,Def2; hence [x,y] in the InternalRel of Omega T by ORDERS_1:def 9; end; the InternalRel of Omega S = (the InternalRel of Omega T)|_2 the carrier of Omega S proof let x, y be set; 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 A5,WELLORD1:16; assume A11: [x,y] in (the InternalRel of Omega T)|_2 the carrier of Omega S; then A12: [x,y] in the InternalRel of Omega T by WELLORD1:16; A13: x in the carrier of Omega S & y in the carrier of Omega S by A11,ZFMISC_1:106; then reconsider o3 = x, o4 = y as Element of Omega S; reconsider s1 = x, s2 = y as Element of S by A2,A13; reconsider t1 = x, t2 = y as Element of T by A1,A2,A13; reconsider o1 = x, o2 = y as Element of Omega T by A1,A2,A3,A13; o1 <= o2 by A12,ORDERS_1:def 9; then consider Y being Subset of T such that A14: Y = {t2} and A15: t1 in Cl Y by Def2; A16: Cl {s2} = (Cl {t2}) /\ [#]S by PRE_TOPC:47; t1 in [#]S by A2,A13,PRE_TOPC:12; then s1 in Cl {s2} by A14,A15,A16,XBOOLE_0:def 3; then o3 <= o4 by Def2; hence [x,y] in the InternalRel of Omega S by ORDERS_1:def 9; end; hence Omega S is full SubRelStr of Omega T by A4,A5,YELLOW_0:def 13,def 14 ; end; theorem Th18: for S, T being TopSpace, h being map of S, T, g being map of Omega S, Omega T st h = g & h is_homeomorphism holds g is isomorphic proof let S, T be TopSpace, h be map of S, T, g be map of Omega S, Omega T; assume that A1: h = g and A2: h is_homeomorphism; A3: the carrier of S = the carrier of Omega S & the carrier of T = the carrier of Omega T by Lm1; A4: dom h = [#]S by A2,TOPS_2:def 5; A5: h is one-to-one & rng h = [#]T by A2,TOPS_2:def 5; per cases; suppose A6: S is non empty & T is non empty; then reconsider s = S, t = T as non empty TopSpace; reconsider f = g as map of Omega s, Omega t; A7: rng f = the carrier of Omega t by A1,A3,A5,PRE_TOPC:12; 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; dom h = the carrier of S by A4,PRE_TOPC:12; then A8: dom h = the carrier of Omega s by Lm1; hereby assume x <= y; then consider Y being Subset of s such that A9: Y = {y} and A10: x in Cl Y by Def2; reconsider Z = {f.y} as Subset of t by A3; f.x in f.:Cl Y by A10,FUNCT_2:43; then A11: h.x in Cl (h.:Y) by A1,A2,TOPS_2:74; h.:Y = Z by A1,A8,A9,FUNCT_1:117; hence f.x <= f.y by A1,A11,Def2; end; assume f.x <= f.y; then consider Y being Subset of t such that A12: Y = {f.y} and A13: f.x in Cl Y by Def2; reconsider Z = {f".(f.y)} as Subset of s by A3; A14: h" is_homeomorphism by A2,A6,TOPS_2:70; A15: rng f = [#]Omega t by A7,PRE_TOPC:12; then A16: f" = f qua Function" by A1,A5,TOPS_2:def 4 .= h" by A1,A5,TOPS_2:def 4; f".(f.x) in f".:Cl Y by A13,FUNCT_2:43; then A17: h".(h.x) in Cl (h".:Y) by A1,A14,A16,TOPS_2:74; A18: x = (f qua Function)".(f.x) by A1,A5,A8,FUNCT_1:56 .= f".(f.x) by A1,A5,A15,TOPS_2:def 4; A19: y = (h qua Function)".(h.y) by A5,A8,FUNCT_1:56 .= f".(f.y) by A1,A5,A15,TOPS_2:def 4; A20: dom f = [#]S by A1,A2,TOPS_2:def 5 .= the carrier of S by PRE_TOPC:12; f".:Y = f qua Function".:Y by A1,A5,A15,TOPS_2:def 4 .= f"Y by A1,A5,FUNCT_1:155 .= Z by A1,A3,A5,A12,A19,A20,FINSEQ_5:4; hence x <= y by A1,A16,A17,A18,A19,Def2; end; hence thesis by A1,A5,A7,WAYBEL_0:66; suppose S is empty or T is empty; then reconsider s = S, t = T as empty TopSpace by A4,A5,YELLOW14:19; Omega s is empty & Omega t is empty; hence thesis by WAYBEL_0:def 38; end; theorem Th19: for S, T being TopSpace st S, T are_homeomorphic holds Omega S, Omega T are_isomorphic proof let S, T be TopSpace; assume S,T are_homeomorphic; then consider h being map of S, T such that A1: h is_homeomorphism by T_0TOPSP:def 1; the carrier of S = the carrier of Omega S & the carrier of T = the carrier of Omega T by Lm1; then reconsider f = h as map of Omega S, Omega T ; take f; thus thesis by A1,Th18; end; Lm4: for S, T being non empty RelStr, f being map of S, S, g being map of T, T st the RelStr of S = the RelStr of T & f = g & f is projection holds g is projection proof let S, T be non empty RelStr, f be map of S,S, g be map of T,T; assume the RelStr of S = the RelStr of T & f = g & f is idempotent monotone; hence g is idempotent monotone by WAYBEL_9:1; end; ::p.124 proposition 3.7 ::p.124 theorem 3.8 (ii, part a) theorem Th20: for T being injective T_0-TopSpace holds Omega T is complete continuous LATTICE proof set S = Sierpinski_Space, B = BoolePoset 1; let T be injective T_0-TopSpace; consider M being non empty set such that A1: T is_Retract_of product (M --> S) by WAYBEL18:20; consider f being map of product(M --> S), product(M --> S) such that A2: f is continuous and A3: f*f = f and A4: Image f, T are_homeomorphic by A1,WAYBEL18:def 8; consider TL being Scott TopAugmentation of product(M --> B); A5: the topology of TL = the topology of product (M --> S) by WAYBEL18:16; A6: the RelStr of TL = the RelStr of product(M --> B) by YELLOW_9:def 4; A7: the carrier of TL = the carrier of product(M --> S) by Th3; then reconsider ff = f as map of TL, TL ; the TopStruct of the TopStruct of TL = the TopStruct of TL implies Omega the TopStruct of TL = Omega TL by Th13; then A8: the RelStr of Omega the TopStruct of product(M --> S) = the RelStr of product (M --> B) by A5,A7,Th16; ff is continuous by A2,A5,A7,YELLOW12:36; then A9: ff is directed-sups-preserving by WAYBEL17:22; ff is projection proof thus ff is idempotent monotone by A3,A9,QUANTAL1:def 9,WAYBEL17:3; end; then reconsider g = ff as projection map of product (M --> B), product (M --> B) by A6,Lm4; g is directed-sups-preserving by A6,A9,WAYBEL21:6; then A10: Image g is complete continuous LATTICE by WAYBEL15:17,YELLOW_2:37; A11: the RelStr of Omega Image f, Omega Image f are_isomorphic by WAYBEL13:26; Omega Image f, Omega T are_isomorphic by A4,Th19; then A12: the RelStr of Omega Image f, Omega T are_isomorphic by A11,WAYBEL_1:8 ; A13: the carrier of Image g = rng g by YELLOW_2:11 .= the carrier of Image f by WAYBEL18:10 .= the carrier of Omega Image f by Lm1; A14: the InternalRel of Image g = (the InternalRel of (product (M --> B)))|_2 the carrier of Image g by YELLOW_0:def 14; Omega Image f is full SubRelStr of Omega product (M --> S) by Th17; then the InternalRel of Omega Image f = (the InternalRel of (Omega product (M --> S)))|_2 the carrier of Omega Image f by YELLOW_0:def 14; hence thesis by A8,A10,A12,A13,A14,WAYBEL15:11,WAYBEL20:18,YELLOW14:12,13; end; definition let T be injective T_0-TopSpace; cluster Omega T -> complete continuous; coherence by Th20; end; theorem Th21: for X, Y being non empty TopSpace, f being continuous map of Omega X, Omega Y holds f is monotone proof let X, Y be non empty TopSpace, f be continuous map of Omega X, Omega Y; let x, y be Element of Omega X; assume x <= y; then consider A being Subset of X such that A1: A = {y} and A2: x in Cl A by Def2; A3: the carrier of Y = the carrier of Omega Y by Lm1; then reconsider Z = {f.y} as Subset of Y; for G being Subset of Y st G is open holds f.x in G implies Z meets G proof let G be Subset of Y such that A4: G is open and A5: f.x in G; the carrier of X = the carrier of Omega X by Lm1; then reconsider g = f as map of X, Y by A3; the TopStruct of X = the TopStruct of Omega X & the TopStruct of Y = the TopStruct of Omega Y by Def2; then g is continuous by YELLOW12:36; then A6: g"G is open by A4,TOPS_2:55; x in g"G by A5,FUNCT_2:46; then A meets g"G by A2,A6,PRE_TOPC:def 13; then consider m being set such that A7: m in A /\ g"G by XBOOLE_0:4; A8: m in A & m in g"G by A7,XBOOLE_0:def 3; then m = y by A1,TARSKI:def 1; then f.y in Z & f.y in G by A8,FUNCT_2:46,TARSKI:def 1; then Z /\ G <> {}Y by XBOOLE_0:def 3; hence Z meets G by XBOOLE_0:def 7; end; then f.x in Cl Z by A3,PRE_TOPC:def 13; hence f.x <= f.y by Def2; end; definition let X, Y be non empty TopSpace; cluster continuous -> monotone map of Omega X, Omega Y; coherence by Th21; end; theorem Th22: for T being non empty TopSpace, x being Element of Omega T holds Cl {x} = downarrow x proof let T be non empty TopSpace, x be Element of Omega T; A1: the TopStruct of T = the TopStruct of Omega T by Def2; hereby let a be set; assume A2: a in Cl {x}; then reconsider b = a as Element of Omega T; reconsider Z = {x} as Subset of T by A1; a in Cl Z by A1,A2,TOPS_3:80; then b <= x by Def2; hence a in downarrow x by WAYBEL_0:17; end; let a be set; assume A3: a in downarrow 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; end; definition let T be non empty TopSpace, x be Element of Omega T; cluster Cl {x} -> non empty lower directed; coherence proof reconsider y = x as Element of Omega T; Cl {y} = downarrow y by Th22; hence thesis; end; cluster downarrow x -> closed; coherence proof Cl {x} = downarrow x by Th22; hence thesis; end; end; theorem Th23: for X being TopSpace, A being open Subset of Omega X holds A is upper proof let X be TopSpace, A be open Subset of Omega X; let x, y be Element of Omega X such that A1: x in A; assume x <= y; then consider Z being Subset of X such that A2: Z = {y} & x in Cl Z by Def2; X is non empty proof thus the carrier of X is non empty by A2; end; then reconsider X as non empty TopSpace; reconsider y as Element of Omega X; the TopStruct of X = the TopStruct of Omega X by Def2; then x in Cl {y} by A2,TOPS_3:80; then A meets {y} by A1,PRE_TOPC:def 13; hence thesis by ZFMISC_1:56; end; definition let T be TopSpace; cluster open -> upper Subset of Omega T; coherence by Th23; end; Lm5: now let X, Y be non empty TopSpace, N be net of ContMaps(X,Omega Y); A1:the mapping of N in Funcs(the carrier of N, the carrier of ContMaps(X,Omega Y)) by FUNCT_2:11; A2: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; assume f in the carrier of ContMaps(X,Omega Y); then ex x being map of X, Omega Y st x = f & x is continuous by WAYBEL24: def 3; hence thesis by A2,FUNCT_2:11; end; then 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:63; hence the mapping of N in Funcs(the carrier of N, Funcs(the carrier of X, the carrier of Y)) by A1; end; definition let I be non empty set, S, T be non empty RelStr, N be net of T, i be Element of I such that A1: the carrier of T c= the carrier of S |^ I; func commute(N,i,S) -> strict net of S means :Def3: the RelStr of it = the RelStr of N & the mapping of it = (commute the mapping of N).i; existence proof A2: the mapping of N in Funcs(the carrier of N, the carrier of T) by FUNCT_2:11; the carrier of T c= Funcs(I, the carrier of S) by A1,YELLOW_1:28; then Funcs(the carrier of N, the carrier of T) c= Funcs(the carrier of N, Funcs(I, the carrier of S)) by FUNCT_5:63; then dom ((commute the mapping of N).i) = the carrier of N & rng ((commute the mapping of N).i) c= the carrier of S by A2,EQUATION:3; then reconsider f = (commute(the mapping of N)).i as Function of the carrier of N, the carrier of S by FUNCT_2:def 1,RELSET_1:11; set A = NetStr (#the carrier of N, the InternalRel of N, f#); A3: the RelStr of A = the RelStr of N; A is directed proof A4: [#]N is directed by WAYBEL_0:def 6; [#]N = the carrier of N by PRE_TOPC:12 .= [#]A by PRE_TOPC:12; hence [#]A is directed by A3,A4,WAYBEL_0:3; end; then reconsider A as strict net of S by A3,WAYBEL_8:13; take A; thus thesis; end; uniqueness; end; theorem Th24: for X, Y being non empty TopSpace, N being net of ContMaps(X,Omega Y), i being Element of N, 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, N be net of ContMaps(X,Omega Y), i be Element of N, x be Point of X; A1: the mapping of N in Funcs(the carrier of N, Funcs(the carrier of X, the carrier of Y)) by Lm5; 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,PRALG_2:5; end; theorem Th25: for X, Y being non empty TopSpace, N being eventually-directed net of ContMaps(X,Omega Y), x being Point of X holds commute(N,x,Omega Y) is eventually-directed proof let X, Y be non empty TopSpace, N be eventually-directed net of ContMaps(X,Omega Y), x be Point of X; set M = commute(N,x,Omega Y), L = (Omega Y) |^ the carrier of X; for i being Element of M ex j being Element of M st for k being Element of M st j <= k holds M.i <= M.k proof let i be Element of M; A1: ContMaps(X,Omega Y) is SubRelStr of L 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: the RelStr of N = the RelStr of M 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 M by A2; take j; let k be Element of M; reconsider c = k as Element of N by A2; reconsider Na = N.a, Nc = N.c as Element of L by A1,YELLOW_0:59; reconsider A = Na, C = Nc as Element of product((the carrier of X) --> Omega Y) by YELLOW_1:def 5; assume j <= k; then b <= c by A2,YELLOW_0:1; then N.a <= N.c by A3; then Na <= Nc by A1,YELLOW_0:60; then A <= C by YELLOW_1:def 5; then A4: A.x <= C.x by WAYBEL_3:28; A5: (the mapping of M).a = (the mapping of N).i.x & (the mapping of M).c = (the mapping of N).k.x by Th24; M.i = (the mapping of M).a & M.k = (the mapping of M).c & A.x = (the mapping of N).i.x & C.x = (the mapping of N).k.x by WAYBEL_0:def 8; hence M.i <= M.k by A4,A5,FUNCOP_1:13; end; hence thesis by WAYBEL_0:11; end; definition let X, Y be non empty TopSpace, N be eventually-directed net of ContMaps(X,Omega Y), x be Point of X; cluster commute(N,x,Omega Y) -> eventually-directed; coherence by Th25; end; definition let X, Y be non empty TopSpace; cluster -> Function-yielding net of ContMaps(X,Omega Y); coherence; end; Lm6: now let X, Y be non empty TopSpace, N be net of ContMaps(X,Omega Y), i be Element of N; thus A1: (the mapping of N).i is map of X, Omega Y by WAYBEL24:21; the carrier of Y = the carrier of Omega Y by Lm1; hence (the mapping of N).i is map of X, Y by A1; end; Lm7: now let X, Y be non empty TopSpace, N be net of ContMaps(X,Omega Y), x be Point of X; 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:the RelStr of N = the RelStr 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; end; theorem Th26: for X being non empty TopSpace, Y being T_0-TopSpace, 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, Y be T_0-TopSpace, N be net of ContMaps(X,Omega Y) such that A1: for x being Point of X holds ex_sup_of commute(N,x,Omega Y); set n = the mapping of N, L = (Omega Y) |^ the carrier of X; deffunc F(Element of X) = sup commute(N,$1,Omega Y); 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 = F(u) from LambdaD; reconsider a = f as Element of L by WAYBEL24:19; ex a being Element of L st rng n is_<=_than a & for b being Element of L st rng n is_<=_than b holds a <= b proof A3: dom n = the carrier of N by FUNCT_2:def 1; A4: L = product ((the carrier of X) --> Omega Y) by YELLOW_1:def 5; take a; thus rng n is_<=_than a proof let k be Element of L; assume k in rng n; then consider i being set such that A5: i in dom n and A6: k = n.i by FUNCT_1:def 5; reconsider i as Point of N by A5; reconsider k' = k, a' = a as Element of product ((the carrier of X) --> Omega Y) by YELLOW_1:def 5; for u being Element of X holds k'.u <= a'.u proof let u be Element of X; A7: Omega Y = ((the carrier of X) --> Omega Y).u by FUNCOP_1:13; 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: dom the mapping of commute(N,u,Omega Y) = the carrier of N by A3,Lm7; A10: a'.u = sup commute(N,u,Omega Y) by A2 .= Sup the mapping of commute(N,u,Omega Y) by WAYBEL_2:def 1 .= sup rng the mapping of commute(N,u,Omega Y) by YELLOW_2:def 5; k'.u = (the mapping of commute(N,u,Omega Y)).i by A6,Th24; then k'.u in rng the mapping of commute(N,u,Omega Y) by A9,FUNCT_1: def 5; hence k'.u <= a'.u by A7,A8,A10,YELLOW_4:1; end; hence k <= a by A4,WAYBEL_3:28; end; let b be Element of L such that A11: for k being Element of L st k in rng n holds k <= b; reconsider a' = a, b' = b as Element of product ((the carrier of X) --> Omega Y) by YELLOW_1:def 5; for u being Element of X holds a'.u <= b'.u proof let u be Element of X; A12: Omega Y = ((the carrier of X) --> Omega Y).u by FUNCOP_1:13; A13: a'.u = sup commute(N,u,Omega Y) by A2 .= Sup the mapping of commute(N,u,Omega Y) by WAYBEL_2:def 1 .= sup rng the mapping of commute(N,u,Omega Y) by YELLOW_2:def 5; ex_sup_of commute(N,u,Omega Y) by A1; then A14: ex_sup_of rng the mapping of commute(N,u,Omega Y), Omega Y by WAYBEL_9:def 3; rng the mapping of commute(N,u,Omega Y) is_<=_than b.u proof let s be Element of Omega Y; assume s in rng the mapping of commute(N,u,Omega Y); 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 5; reconsider i as Point of N by A3,A15,Lm7; A17: s = n.i.u by A16,Th24; A18: n.i in rng n by A3,FUNCT_1:def 5; n.i is map of X, Omega Y by WAYBEL24:21; then reconsider k = n.i as Element of L by WAYBEL24:19; reconsider k' = k as Element of product ((the carrier of X) --> Omega Y) by YELLOW_1:def 5; k <= b by A11,A18; then k' <= b' by YELLOW_1:def 5; hence s <= b.u by A12,A17,WAYBEL_3:28; end; hence a'.u <= b'.u by A12,A13,A14,YELLOW_0:30; end; hence a <= b by A4,WAYBEL_3:28; end; hence ex_sup_of rng n, L by YELLOW_0:15; end; begin :: Monotone convergence topological spaces ::p.125 definition 3.9 definition let T be non empty TopSpace; attr T is monotone-convergence means :Def4: 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; theorem Th27: for S, T being non empty TopSpace st the TopStruct of S = the TopStruct of T & S is monotone-convergence holds T is monotone-convergence proof let S, T be non empty TopSpace such that A1: the TopStruct of S = the TopStruct 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; let E be non empty directed Subset of Omega T; A3: Omega S = Omega T by A1,Th13; hence ex_sup_of E,Omega T by A2; let V be open Subset of T such that A4: sup E in V; reconsider W = V as Subset of S by A1; reconsider D = E as Subset of Omega S by A3; W is open & sup D in W by A1,A4,Th13,TOPS_3:76; hence E meets V by A2,A3; end; Lm8: now let T be non empty 1-sorted, D be non empty Subset of T, d be Element of T such that A1: the carrier of T = {d}; thus D ={d} proof thus D c= {d} by A1; let a be set; assume a in {d}; then A2: a = d by TARSKI:def 1; consider x being Element of D; x in D; hence thesis by A1,A2,TARSKI:def 1; end; end; definition cluster trivial -> monotone-convergence T_0-TopSpace; coherence proof let T be T_0-TopSpace; assume T is trivial; then consider d being Element of T such that A1: the carrier of T = {d} by TEX_1:def 1; let D be non empty directed Subset of Omega T; A2: the carrier of T = the carrier of Omega T by Lm1; then reconsider d as Element of Omega T; D = {d} by A1,A2,Lm8; hence ex_sup_of D,Omega T by YELLOW_0:38; let V be open Subset of T; assume sup D in V; then A3: V = {d} by A1,Lm8; {d} meets {d}; hence D meets V by A1,A2,A3,Lm8; end; end; definition cluster strict trivial non empty TopSpace; existence proof consider A being strict trivial non empty TopSpace; take A; thus thesis; end; end; theorem for S being monotone-convergence T_0-TopSpace, T being T_0-TopSpace st S, T are_homeomorphic holds T is monotone-convergence proof let S be monotone-convergence T_0-TopSpace, T be T_0-TopSpace; given h being map of S, T such that A1: h is_homeomorphism; let D be non empty directed Subset of Omega T; A2: the carrier of S = the carrier of Omega S by Lm1; the carrier of T = the carrier of Omega T by Lm1; then reconsider f = h as map of Omega S, Omega T by A2; A3: f is isomorphic by A1,Th18; then A4: f" is isomorphic by YELLOW14:11; A5: rng f = the carrier of Omega T by A3,WAYBEL_0:66; A6: rng h = [#]T & h is one-to-one by A1,TOPS_2:def 5; A7: rng f = [#]Omega T by A5,PRE_TOPC:12; f" is monotone by A4,WAYBEL_0:def 38; then f".:D is directed by YELLOW_2:17; then A8: f"D is non empty directed Subset of Omega S by A6,A7,TOPS_2:68; then ex_sup_of f"D,Omega S by Def4; then ex_sup_of f.:f"D,Omega T by A3,YELLOW14:17; hence A9: ex_sup_of D,Omega T by A5,FUNCT_1:147; let V be open Subset of T; A10: h"V is open by A1,TOPGRP_1:26; f" is sups-preserving by A4,WAYBEL13:20; then A11: f" preserves_sup_of D by WAYBEL_0:def 33; assume sup D in V; then h".sup D in h".:V by FUNCT_2:43; then h".sup D in h"V by A6,TOPS_2:68; then h qua Function".sup D in h"V by A6,TOPS_2:def 4; then f".sup D in h"V by A6,A7,TOPS_2:def 4; then sup (f".:D) in h"V by A9,A11,WAYBEL_0:def 31; then sup (f"D) in h"V by A6,A7,TOPS_2:68; then f"D meets h"V by A8,A10,Def4; then consider a being set such that A12: a in f"D & a in h"V by XBOOLE_0:3; reconsider a as Element of S by A12; now take b = h.a; thus b in D & b in V by A12,FUNCT_2:46; end; hence thesis by XBOOLE_0:3; end; theorem Th29: for S being Scott complete TopLattice holds S is monotone-convergence proof let S be Scott complete TopLattice; let D be non empty directed Subset of Omega S; thus A1: ex_sup_of D,Omega S by YELLOW_0:17; let V be open Subset of S such that A2: sup D in V; A3: Omega S = the TopRelStr of S by Th15; then A4: the RelStr of Omega S = the RelStr of S; reconsider E = D as Subset of S by A3; A5: E is non empty directed Subset of S by A4,WAYBEL_0:3; sup E in V by A1,A2,A4,YELLOW_0:26; hence D meets V by A5,WAYBEL11:def 1; end; definition let L be complete LATTICE; cluster -> monotone-convergence (Scott TopAugmentation of L); coherence by Th29; end; definition let L be complete LATTICE, S be Scott TopAugmentation of L; cluster the TopStruct of S -> monotone-convergence; coherence by Th27; end; theorem Th30: for X being monotone-convergence T_0-TopSpace holds Omega X is up-complete proof let X be monotone-convergence T_0-TopSpace; for A being non empty directed Subset of Omega X holds ex_sup_of A,Omega X by Def4; hence thesis by WAYBEL_0:75; end; definition let X be monotone-convergence T_0-TopSpace; cluster Omega X -> up-complete; coherence by Th30; end; theorem Th31: for X being monotone-convergence (non empty TopSpace), N being eventually-directed prenet of Omega X holds ex_sup_of N proof let X be monotone-convergence (non empty TopSpace), N be eventually-directed prenet of Omega X; rng netmap (N,Omega X) is directed by WAYBEL_2:18; then rng the mapping of N is non empty directed by WAYBEL_0:def 7; hence ex_sup_of rng the mapping of N,Omega X by Def4; end; theorem Th32: for X being monotone-convergence (non empty TopSpace), N being eventually-directed net of Omega X holds sup N in Lim N proof let X be monotone-convergence (non empty TopSpace), N be eventually-directed net of Omega X; 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 by WAYBEL_0:def 7; for V being a_neighborhood of sup N holds N is_eventually_in V proof let V be a_neighborhood of sup N; A1: the TopStruct of X = the TopStruct of Omega X by Def2; then reconsider I = Int V as Subset of X; A2: I is open by A1,TOPS_3:76; sup N in I by CONNSP_2:def 1; then Sup the mapping of N in I by WAYBEL_2:def 1; then sup D in I by YELLOW_2:def 5; then D meets I by A2,Def4; then consider y being set such that A3: y in D and A4: y in I by XBOOLE_0:3; reconsider y as Point of X by A4; consider x being set such that A5: x in dom the mapping of N and A6: (the mapping of N).x = y by A3,FUNCT_1:def 5; reconsider x as Element of N by A5; consider j being Element of N such that A7: for k being Element of N st j <= k holds N.x <= N.k by WAYBEL_0:11; take j; let k be Element of N; assume j <= k; then N.x <= N.k by A7; then consider Y being Subset of X such that A8: Y = {N.k} and A9: N.x in Cl Y by Def2; y in Cl Y by A6,A9,WAYBEL_0:def 8; then Y meets I by A2,A4,PRE_TOPC:def 13; then consider m being set such that A10: m in Y /\ I by XBOOLE_0:4; A11: m in Y & m in I by A10,XBOOLE_0:def 3; then A12: m = N.k by A8,TARSKI:def 1; Int V c= V by TOPS_1:44; hence N.k in V by A11,A12; end; hence thesis by YELLOW_6:def 18; end; theorem Th33: for X being monotone-convergence (non empty TopSpace), N being eventually-directed net of Omega X holds N is convergent proof let X be monotone-convergence (non empty TopSpace), N be eventually-directed net of Omega X; thus Lim N <> {} by Th32; end; definition let X be monotone-convergence (non empty TopSpace); cluster -> convergent (eventually-directed net of Omega X); coherence by Th33; end; theorem 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 such that A1: for N being eventually-directed net of Omega X holds ex_sup_of N & sup N in Lim N; let D be non empty directed Subset of Omega X; A2: ex_sup_of Net-Str D by A1; Net-Str D = NetStr (#D, (the InternalRel of (Omega X))|_2 D, (id the carrier of (Omega X))|D#) by WAYBEL17:def 4; then A3: rng the mapping of Net-Str D = D by YELLOW14:2; hence ex_sup_of D,Omega X by A2,WAYBEL_9:def 3; let V be open Subset of X such that A4: sup D in V; A5: sup Net-Str D in Lim Net-Str D by A1; reconsider Z = V as Subset of Omega X by Lm2; Z is a_neighborhood of sup Net-Str D proof A6: sup Net-Str D = Sup the mapping of Net-Str D by WAYBEL_2:def 1 .= sup rng the mapping of Net-Str D by YELLOW_2:def 5; the TopStruct of X = the TopStruct of Omega X by Def2; then Int Z = Int V by TOPS_3:77; hence sup Net-Str D in Int Z by A3,A4,A6,TOPS_1:55; end; then Net-Str D is_eventually_in V by A5,YELLOW_6:def 18; then consider i being Element of Net-Str D such that A7: for j being Element of Net-Str D st i <= j holds (Net-Str D).j in V by WAYBEL_0:def 11; now take a = (Net-Str D).i; dom the mapping of Net-Str D = the carrier of Net-Str D by FUNCT_2:def 1 ; then (the mapping of Net-Str D).i in rng the mapping of Net-Str D by FUNCT_1:def 5; hence a in D by A3,WAYBEL_0:def 8; thus a in V by A7; end; hence thesis by XBOOLE_0:3; end; ::p.125 lemma 3.10 theorem Th35: for X being monotone-convergence (non empty TopSpace), Y being T_0-TopSpace, f being continuous map of Omega X, Omega Y holds f is directed-sups-preserving proof let X be monotone-convergence (non empty TopSpace), Y be T_0-TopSpace, f be continuous map of Omega X, Omega Y; let D be non empty directed Subset of Omega X; assume A1: ex_sup_of D,Omega X; A2: the TopStruct of X = the TopStruct of Omega X by Def2; A3: the TopStruct of Y = the TopStruct 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; D is_<=_than sup D by A1,YELLOW_0:def 9; hence f.:D is_<=_than a by YELLOW_2:16; let b be Element of Omega Y such that A4: for c being Element of Omega Y st c in f.:D holds c <= b; reconsider Z = {b} as Subset of Y by Lm2; for G being Subset of Y st G is open holds a in G implies Z meets G proof let G be Subset of Y such that A5: G is open and A6: a in G; A7: b in {b} by TARSKI:def 1; reconsider H = G as open Subset of Omega Y by A3,A5,TOPS_3:76; f"H is open by TOPS_2:55; then A8: f"H is open Subset of X by A2,TOPS_3:76; sup D in f"H by A6,FUNCT_2:46; 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 as Point of Omega X by A9; f.c in f.:D by A9,FUNCT_2:43; then A11: f.c <= b by A4; f.c in H by A10,FUNCT_2:46; then b in G by A11,WAYBEL_0:def 20; hence Z meets G by A7,XBOOLE_0:3; end; then a in Cl Z by A3,PRE_TOPC:def 13; hence a <= b by Def2; end; hence A12: ex_sup_of f.:D,Omega Y by YELLOW_0:15; assume A13: sup (f.:D) <> f.sup D; set V = (downarrow sup (f.:D))`; A14: f"V is open by TOPS_2:55; reconsider fV = f"V as Subset of X by A2; reconsider fV as open Subset of X by A2,A14,TOPS_3:76; sup (f.:D) <= sup (f.:D); then A15: sup (f.:D) in downarrow sup (f.:D) by WAYBEL_0:17; sup (f.:D) <= f.sup D by A1,A12,WAYBEL17:15; then not f.sup D <= sup (f.:D) by A13,ORDERS_1:25; then not f.sup D in downarrow sup (f.:D) by WAYBEL_0:17; then f.sup D in V by YELLOW_6:10; then sup D in fV by FUNCT_2:46; then D meets fV by Def4; then consider d being set such that A16: d in D and A17: d in fV by XBOOLE_0:3; reconsider d as Element of Omega X by A16; A18: f.d in V by A17,FUNCT_2:46; f.d in f.:D by A16,FUNCT_2:43; then f.d <= sup (f.:D) by A12,YELLOW_4:1; then sup (f.:D) in V by A18,WAYBEL_0:def 20; hence contradiction by A15,YELLOW_6:10; end; definition let X be monotone-convergence (non empty TopSpace), Y be T_0-TopSpace; cluster continuous -> directed-sups-preserving map of Omega X, Omega Y; coherence by Th35; end; theorem Th36: for T being monotone-convergence T_0-TopSpace, 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, R be T_0-TopSpace; given c being continuous map of R, T, r being continuous map of T, R such that A1: r * c = id R; let D be non empty directed Subset of Omega R; A2: the TopStruct of T = the TopStruct of Omega T by Def2; A3: the TopStruct of R = the TopStruct of Omega R by Def2; then reconsider DR = D as non empty Subset of R; reconsider f = c*r as map of Omega T, Omega T by A2; reconsider cc = c as map of Omega R, Omega T by A2,A3; reconsider rr = r as map of Omega T, Omega R by A2,A3; cc is continuous by A2,A3,YELLOW12:36; then cc is monotone by Th21; then A4: cc.:D is directed by YELLOW_2:17; then A5: ex_sup_of cc.:D, Omega T by Def4; A6: r.:(c.:D) = (r*c).:DR by RELAT_1:159 .= D by A1,WAYBEL15:3; rr is continuous by A2,A3,YELLOW12:36; then rr is directed-sups-preserving by Th35; then A7: rr preserves_sup_of cc.:D by A4,WAYBEL_0:def 37; hence ex_sup_of D, Omega R by A5,A6,WAYBEL_0:def 31; let V be open Subset of R such that A8: sup D in V; A9: c.:V c= r"V proof let a be set; assume a in c.:V; then consider x being set such that A10: x in the carrier of R and A11: x in V and A12: a = c.x by FUNCT_2:115; reconsider x as Point of R by A10; A13: a = c.x by A12; r.a = (r*c).x by A12,FUNCT_2:21 .= x by A1,GRCAT_1:11; hence a in r"V by A11,A13,FUNCT_2:46; end; A14: r"V is open by TOPS_2:55; f is continuous by A2,YELLOW12:36; then f is directed-sups-preserving by Th35; then A15: f preserves_sup_of cc.:D by A4,WAYBEL_0:def 37; A16: c.sup D = c.(r.sup(cc.:D)) by A5,A6,A7,WAYBEL_0:def 31 .= f.sup(cc.:D) by A2,FUNCT_2:21 .= sup(f.:(cc.:D)) by A5,A15,WAYBEL_0:def 31 .= sup (cc.:D) by A6,RELAT_1:159; c.sup D in c.:V by A8,FUNCT_2:43; then c.:D meets r"V by A4,A9,A14,A16,Def4; then consider d being set such that A17: d in cc.:D and A18: d in r"V by XBOOLE_0:3; now take a = r.d; thus a in D by A6,A17,FUNCT_2:43; thus a in V by A18,FUNCT_2:46; end; hence thesis by XBOOLE_0:3; end; ::p.124 theorem 3.8 (ii, part b) theorem Th37: for T being injective T_0-TopSpace, S being Scott TopAugmentation of Omega T holds the TopStruct of S = the TopStruct of T proof let T be injective T_0-TopSpace, S be Scott TopAugmentation of Omega T; set SS = Sierpinski_Space, B = BoolePoset 1; consider M being non empty set such that A1: T is_Retract_of product (M --> SS) by WAYBEL18:20; consider c being continuous map of T, product (M --> SS), r being continuous map of product (M --> SS), T such that A2: r * c = id T by A1,Def1; consider S_2M being Scott TopAugmentation of product (M --> B); A3: the topology of S_2M = the topology of product (M --> SS) by WAYBEL18:16; A4: the carrier of S_2M = the carrier of product (M --> SS) by Th3; then reconsider rr = r as map of S_2M, T ; A5: the RelStr of S_2M = the RelStr of product (M --> B) by YELLOW_9:def 4; A6: the TopStruct of T = the TopStruct of Omega T by Def2; then reconsider r1 = r as map of product (M --> B), Omega T by A4,A5; reconsider c1 = c as map of Omega T, product (M --> B) by A4,A5,A6; A7: the TopStruct of product (M --> SS) = the TopStruct of Omega product (M --> SS) by Def2; then reconsider c1a = c as map of Omega T, Omega product (M --> SS) by A6; A8: the RelStr of S = the RelStr of Omega T by YELLOW_9:def 4; then reconsider r2 = r1 as map of S_2M, S by A5; reconsider c2 = c1 as map of S, S_2M by A5,A8; A9: the RelStr of Omega S_2M = the RelStr of product (M --> B) by Th16; then reconsider rr1 = r1 as map of Omega S_2M, Omega T ; A10: the TopStruct of T = the TopStruct of T; then A11: rr is continuous by A3,A4,YELLOW12:36; the TopStruct of Omega S_2M = the TopStruct of S_2M by Def2; then rr1 is continuous by A3,A4,A6,YELLOW12:36; then rr1 is directed-sups-preserving by Th35; then r2 is directed-sups-preserving by A5,A8,A9,WAYBEL21:6; then A12: r2 is continuous by WAYBEL17:22; reconsider r3 = r2 as map of product (M --> SS), S by A4; the TopStruct of S = the TopStruct of S; then A13: r3 is continuous by A3,A4,A12,YELLOW12:36; T is_Retract_of S_2M by A1,A3,A4,A10,Th8; then reconsider W = T as monotone-convergence (non empty TopSpace) by Th36; reconsider c1a as continuous map of Omega W, Omega product (M --> SS) by A6,A7,YELLOW12:36; Omega product (M --> SS) = Omega S_2M by A3,A4,Th13; then A14: the RelStr of Omega product (M --> SS) = the RelStr of product (M --> B) by Th16 .= the RelStr of S_2M by YELLOW_9:def 4; c2 = c1a; then c2 is directed-sups-preserving by A8,A14,WAYBEL21:6; then c2 is continuous by WAYBEL17:22; then r3 * c is continuous & rr * c2 is continuous by A11,A13,TOPS_2:58; hence thesis by A2,YELLOW14:34; end; theorem for T being injective T_0-TopSpace holds T is compact locally-compact sober proof let T be injective T_0-TopSpace; consider S being Scott TopAugmentation of Omega T; A1: the TopStruct of S = the TopStruct of T by Th37; S is compact locally-compact sober by WAYBEL14:32; hence thesis by A1,YELLOW14:27,28,29; end; theorem Th39: for T being injective T_0-TopSpace holds T is monotone-convergence proof let T be injective T_0-TopSpace; consider S being Scott TopAugmentation of Omega T; the TopStruct of S = the TopStruct of T by Th37; hence T is monotone-convergence by Th27; end; definition cluster injective -> monotone-convergence T_0-TopSpace; coherence by Th39; end; theorem Th40: for X being non empty TopSpace, Y being monotone-convergence T_0-TopSpace, N being net of ContMaps(X,Omega Y), f, g being map 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, Y be monotone-convergence T_0-TopSpace, N be net of ContMaps(X,Omega Y), f, g be map of X, Omega Y; set m = the mapping of N, L = (Omega Y) |^ the carrier of X, s = "\/"(rng m,L); assume that A1: f = "\/"(rng the mapping of N, (Omega Y) |^ the carrier of X) and A2: ex_sup_of rng m,L and A3: g in rng the mapping of N; reconsider g1 = g as Element of L by WAYBEL24:19; rng m is_<=_than s by A2,YELLOW_0:def 9; then g1 <= s by A3,LATTICE3:def 9; hence g <= f by A1,WAYBEL10:12; end; theorem Th41: for X being non empty TopSpace, Y being monotone-convergence T_0-TopSpace, N being net of ContMaps(X,Omega Y), x being Point of X, f being map 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, Y be monotone-convergence T_0-TopSpace, N be net of ContMaps(X,Omega Y), x be Point of X, f be map of X, Omega Y such 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); set n = the mapping of N, m = the mapping of commute(N,x,Omega Y), L = (Omega Y) |^ the carrier of X; A3: dom n = the carrier of N by FUNCT_2:def 1; then A4: dom m = the carrier of N by Lm7; for x being Point of X holds ex_sup_of commute(N,x,Omega Y) proof let x be Point of X; commute(N,x,Omega Y) is eventually-directed by A1; hence thesis by Th31; end; then A5: ex_sup_of rng n,L by Th26; A6: rng m is_<=_than f.x proof let w be Element of Omega Y; assume w in rng m; then consider i being set such that A7: i in dom m and A8: m.i = w by FUNCT_1:def 5; reconsider i as Point of N by A3,A7,Lm7; reconsider g = n.i as map of X, Omega Y by Lm6; g in rng n by A3,FUNCT_1:def 5; then g <= f by A2,A5,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 A8,Th24; end; for a being Element of Omega Y st rng m is_<=_than a holds f.x <= a proof let a be Element of Omega Y; assume A9: for e being Element of Omega Y st e in rng m holds e <= a; defpred P[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)); A10: for e being Element of X ex u being Element of Omega Y st P[e,u] proof let e be Element of X; per cases; suppose e = x; hence thesis; suppose A11: e <> x; reconsider e as Element of X; take sup commute(N,e,Omega Y); thus thesis by A11; end; consider t being Function of the carrier of X, the carrier of Omega Y such that A12: for u being Element of X holds P[u,t.u] from FuncExD(A10); reconsider t as map of X, Omega Y ; reconsider tt = t as Element of L by WAYBEL24:19; tt is_>=_than rng n proof let s be Element of L; assume s in rng n; then consider i being set such that A13: i in dom n and A14: s = n.i by FUNCT_1:def 5; reconsider i as Point of N by A13; reconsider ss = s as map of X, Omega Y by WAYBEL24:19; A15: L = product ((the carrier of X) --> Omega Y) by YELLOW_1:def 5; reconsider s' = s, t' = tt as Element of product ((the carrier of X) --> Omega Y) by YELLOW_1:def 5; for j being Element of X holds s'.j <= t'.j proof let j be Element of X; A16: ss.j = (the mapping of commute(N,j,Omega Y)).i by A14,Th24; A17: Omega Y = ((the carrier of X) --> Omega Y).j by FUNCOP_1:13; per cases; suppose j <> x; then ex u being Element of X st j = u & t.j = sup commute(N,u,Omega Y) by A12; then A18: t'.j = Sup the mapping of commute(N,j,Omega Y) by WAYBEL_2:def 1 .= sup rng the mapping of commute(N,j,Omega Y) by YELLOW_2:def 5; 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,Lm7; then ss.j in rng the mapping of commute(N,j,Omega Y) by A16,FUNCT_1: def 5; hence thesis by A17,A18,A19,YELLOW_4:1; suppose A20: j = x; A21: ss.x = m.i by A14,Th24; m.i in rng m by A4,FUNCT_1:def 5; then ss.x <= a by A9,A21; hence thesis by A12,A17,A20; end; hence s <= tt by A15,WAYBEL_3:28; end; then A22: "\/"(rng n,L) <= tt by A5,YELLOW_0:30; A23: tt.x = a by A12; reconsider p = "\/"(rng n,L), q = tt as Element of product ((the carrier of X) --> Omega Y) by YELLOW_1:def 5; A24: Omega Y = ((the carrier of X) --> Omega Y).x by FUNCOP_1:13; p <= q by A22,YELLOW_1:def 5; hence f.x <= a by A2,A23,A24,WAYBEL_3:28; end; hence f.x = sup rng the mapping of commute(N,x,Omega Y) by A6,YELLOW_0:30 .= Sup the mapping of commute(N,x,Omega Y) by YELLOW_2:def 5 .= sup commute(N,x,Omega Y) by WAYBEL_2:def 1; end; ::p.125 lemma 3.11 theorem Th42: for X being non empty TopSpace, Y being monotone-convergence T_0-TopSpace, 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 map of X, Y proof let X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace, N be net of ContMaps(X,Omega Y) such that A1: for x being Point of X holds commute(N,x,Omega Y) is eventually-directed; set m = the mapping of N, L = (Omega Y) |^ the carrier of X; A2: the TopStruct of Y = the TopStruct of Omega Y by Def2; reconsider fo = "\/"(rng m,L) as map of X, Omega Y by WAYBEL24:19; reconsider f = fo as map of X, Y by A2; A3: dom m = the carrier of N by FUNCT_2:def 1; for V being Subset of Y st V is open holds f"V is open proof let V be Subset of Y such that A4: V is open; set M = {A where A is Subset of X: ex i being Element of N, g being map of X, Omega Y st g = N.i & A = g"V}; for x being set holds x in f"V iff x in union M proof let x be set; thus x in f"V implies x in union M proof assume A5: x in f"V; then A6: f.x in V by FUNCT_2:46; reconsider x as Point of X by A5; set NET = commute(N,x,Omega Y); A7: m in Funcs(the carrier of N, Funcs(the carrier of X, the carrier of Y)) by Lm5; ContMaps(X,Omega Y) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3; then A8: the carrier of ContMaps(X,Omega Y) c= the carrier of (Omega Y) |^ the carrier of X by YELLOW_0:def 13; then A9: the RelStr of NET = the RelStr of N by Def3; NET is eventually-directed by A1; then reconsider W = rng netmap(NET,Omega Y) as non empty directed Subset of Omega Y by WAYBEL_2:18; f.x = sup NET by A1,Th41 .= Sup the mapping of NET by WAYBEL_2:def 1 .= sup rng the mapping of NET by YELLOW_2:def 5 .= sup W by WAYBEL_0:def 7; then W meets V by A4,A6,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(NET,Omega Y) and A13: k = netmap(NET,Omega Y).i by A10,FUNCT_1:def 5; reconsider i as Element of N by A9,A12; A14: netmap(NET,Omega Y).i = (the mapping of NET).i by WAYBEL_0:def 7 .= (commute the mapping of N).x.i by A8,Def3 .= ((the mapping of N).i).x by A7,PRALG_2:5; reconsider g = N.i as map of X, Omega Y by WAYBEL24:21; A15: k = g.x by A13,A14,WAYBEL_0:def 8; dom g = the carrier of X by FUNCT_2:def 1; then A16: x in g"V by A11,A15,FUNCT_1:def 13; g"V in M; hence thesis by A16,TARSKI:def 4; end; assume x in union M; then consider Z being set such that A17: x in Z and A18: Z in M by TARSKI:def 4; consider A being Subset of X such that A19: Z = A and A20: ex i being Element of N, g being map of X, Omega Y st g = N.i & A = g"V by A18; consider i being Element of N, g being map 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 13; A24: dom f = the carrier of X by FUNCT_2:def 1; reconsider x as Element of X by A17,A19; for x being Point of X holds ex_sup_of commute(N,x,Omega Y) proof let x be Point of X; commute(N,x,Omega Y) is eventually-directed by A1; hence thesis by Th31; end; then A25: ex_sup_of rng m,L by Th26; m.i in rng m by A3,FUNCT_1:def 5; then N.i in rng m by WAYBEL_0:def 8; then g <= fo by A21,A25,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 A26: O = {f.x} and A27: g.x in Cl O by Def2; V meets O by A4,A23,A27,PRE_TOPC:def 13; then consider w being set such that A28: w in V /\ O by XBOOLE_0:4; A29: w in V & w in O by A28,XBOOLE_0:def 3; then w = f.x by A26,TARSKI:def 1; hence thesis by A24,A29,FUNCT_1:def 13; end; then A30: f"V = union M by TARSKI:2; M c= bool the carrier of X proof let m be set; assume m in M; then ex A being Subset of X st m = A & ex i being Element of N, g being map of X, Omega Y st g = N.i & A = g"V; hence thesis; end; then reconsider M as Subset-Family of X by SETFAM_1:def 7; reconsider M as Subset-Family of X; M is open proof let P be Subset of X; assume P in M; then consider A being Subset of X such that A31: P = A and A32: ex i being Element of N, g being map of X, Omega Y st g = N.i & A = g"V; consider i being Element of N, g being map of X, Omega Y such that A33: g = N.i and A34: A = g"V by A32; A35: the TopStruct of X = the TopStruct of X; g in the carrier of ContMaps(X,Omega Y) by A33; then consider g' being map of X, Omega Y such that A36: g = g' & g' is continuous by WAYBEL24:def 3; reconsider g'' = g' as continuous map of X, Y by A2,A35,A36,YELLOW12:36; g''"V is open by A4,TOPS_2:55; hence P is open by A31,A34,A36; end; hence f"V is open by A30,TOPS_2:26; end; hence thesis by TOPS_2:55; end; ::p.126 lemma 3.12 (i) theorem for X being non empty TopSpace, 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, Y be monotone-convergence T_0-TopSpace; set L = (Omega Y) |^ the carrier of X; reconsider C = ContMaps(X,Omega Y) as non empty full SubRelStr of L by WAYBEL24:def 3; C is directed-sups-inheriting proof let D be directed Subset of C such that A1: D <> {} and ex_sup_of D,L; reconsider D as non empty directed Subset of C by A1; set N = Net-Str D; A2: the TopStruct of Y = the TopStruct of Omega Y by Def2; A3: the TopStruct of X = the TopStruct of X; for x being Point of X holds commute(N,x,Omega Y) is eventually-directed by Th25; then "\/"(rng the mapping of N, (Omega Y) |^ the carrier of X) is continuous map of X, Y by Th42; then "\/"(rng the mapping of N, (Omega Y) |^ the carrier of X) is continuous map of X, Omega Y by A2,A3,YELLOW12:36; then A4: "\/"(rng the mapping of N, (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 thesis by A4,YELLOW14:2; end; hence thesis; end;

Back to top