Copyright (c) 1999 Association of Mizar Users
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;