:: Injective Spaces, Part { II }
:: by Artur Korni{\l}owicz and Jaros{\l}aw Gryko
::
:: Received July 3, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PRE_TOPC, WAYBEL18, CARD_1, RCOMP_1, STRUCT_0, SUBSET_1,
XBOOLE_0, TARSKI, REWRITE1, WAYBEL11, WAYBEL_9, FUNCTOR0, T_0TOPSP,
YELLOW_9, CARD_3, FUNCOP_1, YELLOW_1, RELAT_1, RLVECT_2, FUNCT_1,
ZFMISC_1, ORDERS_2, WAYBEL_0, CAT_1, TOPS_2, WELLORD1, ORDINAL2, GROUP_6,
WAYBEL_1, FUNCT_3, BORSUK_1, EQREL_1, XXREAL_0, LATTICE3, YELLOW_0,
WAYBEL_3, RELAT_2, PROB_1, BINOP_1, SEQM_3, WAYBEL24, FUNCT_2, NEWTON,
FUNCT_6, YELLOW_2, ORDINAL1, CONNSP_2, TOPS_1, SEQ_2, YELLOW_8, SETFAM_1,
WAYBEL25;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, FUNCT_3, NATTRA_1,
TOLER_1, QUANTAL1, CARD_3, PRALG_1, FUNCT_6, FUNCOP_1, WAYBEL18,
DOMAIN_1, STRUCT_0, PRE_TOPC, CONNSP_2, TOPS_1, TOPS_2, COMPTS_1,
BORSUK_1, TMAP_1, T_0TOPSP, BORSUK_3, ORDERS_2, 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 TOLER_1, FUNCT_6, TOPS_1, TOPS_2, NATTRA_1, BORSUK_1, TMAP_1,
CANTOR_1, MONOID_0, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_8, YELLOW_8,
WAYBEL17, YELLOW_9, BORSUK_3, WAYBEL24, YELLOW14, COMPTS_1, WAYBEL_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, TEX_1, TSP_1,
BORSUK_2, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_8,
WAYBEL10, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL19, WAYBEL21, WAYBEL24,
YELLOW14, RELSET_1;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_2, ORDERS_2, RELAT_1, RELAT_2,
STRUCT_0, WAYBEL_1, T_0TOPSP, WAYBEL18, LATTICE3, YELLOW_6, WAYBEL_0,
WAYBEL_9, YELLOW14;
equalities SUBSET_1, RELAT_1, STRUCT_0, WAYBEL18, WAYBEL_0, YELLOW_2,
WELLORD1;
expansions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_2, ORDERS_2, WAYBEL_1, T_0TOPSP,
WAYBEL18, LATTICE3, WAYBEL_0, WAYBEL_9, YELLOW_2;
theorems TARSKI, PRE_TOPC, ZFMISC_1, ORDERS_2, T_0TOPSP, FUNCT_1, FUNCT_2,
QUANTAL1, RELAT_1, FINSEQ_5, TEX_1, PRALG_1, FUNCOP_1, CARD_3, BORSUK_1,
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, WAYBEL10, WAYBEL13, WAYBEL15, WAYBEL17, WAYBEL18,
WAYBEL20, WAYBEL24, CONNSP_2, WAYBEL_3, FUNCT_5, WAYBEL_8, TSEP_1,
EQUATION, TOPGRP_1, WAYBEL21, ENUMSET1, YELLOW14, RELSET_1, XBOOLE_0,
XBOOLE_1, FUNCT_6, YELLOW_8, PARTFUN1;
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;
A1: the carrier of S = {0,1} by WAYBEL18:def 9;
assume
A2: p = 0;
A3: [#]S \ {p} = {1}
proof
thus [#]S \ {p} c= {1}
proof
let a be object;
assume
A4: a in [#]S \ {p};
then not a in {p} by XBOOLE_0:def 5;
then a <> 0 by A2,TARSKI:def 1;
then a = 1 by A1,A4,TARSKI:def 2;
hence thesis by TARSKI:def 1;
end;
let a be object;
assume a in {1};
then
A5: a = 1 by TARSKI:def 1;
then
A6: not a in {p} by A2,TARSKI:def 1;
a in [#]S by A1,A5,TARSKI:def 2;
hence thesis by A6,XBOOLE_0:def 5;
end;
the topology of S = {{}, {1}, {0,1}} by WAYBEL18:def 9;
hence [#]S \ {p} in the topology of S by A3,ENUMSET1:def 1;
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;
A1: the carrier of S = {0,1} by WAYBEL18:def 9;
assume
A2: p = 1;
A3: [#]S \ {p} = {0}
proof
thus [#]S \ {p} c= {0}
proof
let a be object;
assume
A4: a in [#]S \ {p};
then not a in {p} by XBOOLE_0:def 5;
then a <> 1 by A2,TARSKI:def 1;
then a = 0 by A1,A4,TARSKI:def 2;
hence thesis by TARSKI:def 1;
end;
let a be object;
assume a in {0};
then
A5: a = 0 by TARSKI:def 1;
then
A6: not a in {p} by A2,TARSKI:def 1;
a in [#]S by A1,A5,TARSKI:def 2;
hence thesis by A6,XBOOLE_0:def 5;
end;
A7: {0} <> {1} by ZFMISC_1:3;
A8: {0} <> {0,1} by ZFMISC_1:5;
the topology of S = {{}, {1}, {0,1}} by WAYBEL18:def 9;
hence not [#]S \ {p} in the topology of S by A7,A8,A3,ENUMSET1:def 1;
end;
registration
cluster Sierpinski_Space -> non T_1;
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 YELLOW_8:26;
end;
end;
registration
cluster complete Scott -> T_0 for TopLattice;
coherence by WAYBEL11:10;
end;
registration
cluster injective strict for T_0-TopSpace;
existence
proof
take Sierpinski_Space;
thus thesis;
end;
end;
registration
cluster complete Scott strict for TopLattice;
existence
proof
set T = the 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{0})
holds the carrier of T = the carrier of product(I
--> Sierpinski_Space)
proof
set S = Sierpinski_Space, B = BoolePoset{0};
let I be non empty set, T be Scott TopAugmentation of product(I -->
BoolePoset{0});
A1: dom Carrier (I --> B) = I by PARTFUN1:def 2;
A2: dom Carrier (I --> S) = I by PARTFUN1:def 2;
A3: for x being object
st x in dom Carrier (I --> S) holds (Carrier (I --> B)).
x = (Carrier (I --> S)).x
proof
let x be object;
assume
A4: x in dom Carrier (I --> S);
then
A5: ex T being 1-sorted st T = (I --> S).x & (Carrier (I --> S)).x = the
carrier of T by PRALG_1:def 15;
ex R being 1-sorted st R = (I --> B).x & (Carrier (I --> B)).x = the
carrier of R by A4,PRALG_1:def 15;
hence (Carrier (I --> B)).x = the carrier of B by A4,FUNCOP_1:7
.= bool {0} by WAYBEL_7:2
.= the carrier of S by WAYBEL18:def 9,YELLOW14:1
.= (Carrier (I --> S)).x by A4,A5,FUNCOP_1:7;
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:2
.= 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 Function of L1, L2, H
being Function of T1, T2 st h = H & h is isomorphic holds H is
being_homeomorphism
proof
let L1, L2 be complete LATTICE, T1 be Scott TopAugmentation of L1, T2 be
Scott TopAugmentation of L2, h be Function of L1, L2, H be Function of T1, T2
such that
A1: h = H and
A2: h is isomorphic;
A3: the RelStr of L2 = the RelStr of T2 by YELLOW_9:def 4;
A4: the RelStr of L1 = the RelStr of T1 by YELLOW_9:def 4;
then reconsider H9 = h" as Function of T2, T1 by A3;
consider g being Function of L2,L1 such that
A5: g = h";
g = (h qua Function)" by A2,A5,TOPS_2:def 4;
then g is isomorphic by A2,WAYBEL_0:68;
then reconsider h2 = h" as sups-preserving Function of L2,L1 by A5,
WAYBEL13:20;
A6: rng H = [#]T2 by A1,A2,A3,WAYBEL_0:66;
A7: for x being object st x in dom H9 holds H9.x = H".x
proof
let x be object;
assume x in dom H9;
A8: H is onto by A6,FUNCT_2:def 3;
thus H9.x = (h qua Function)".x by A2,TOPS_2:def 4
.= H".x by A1,A2,A8,TOPS_2:def 4;
end;
h2 is directed-sups-preserving;
then
A9: H9 is directed-sups-preserving by A4,A3,WAYBEL21:6;
dom (H") = the carrier of T2 by FUNCT_2:def 1
.= dom H9 by FUNCT_2:def 1;
then
A10: H" = H9 by A7,FUNCT_1:2;
reconsider h1 = h as sups-preserving Function of L1,L2 by A2,WAYBEL13:20;
h1 is directed-sups-preserving;
then
A11: H is directed-sups-preserving by A1,A4,A3,WAYBEL21:6;
dom H = [#]T1 by FUNCT_2:def 1;
hence thesis by A1,A2,A11,A9,A6,A10;
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 Function of L1, L2 such that
A1: h is isomorphic;
A2: the RelStr of L2 = the RelStr of T2 by YELLOW_9:def 4;
the RelStr of L1 = the RelStr of T1 by YELLOW_9:def 4;
then reconsider H = h as Function of T1, T2 by A2;
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 Function of S,T such that
A3: p is being_homeomorphism by A2;
let X be non empty TopSpace, f be Function of X, T;
assume
A4: f is continuous;
let Y be non empty TopSpace;
assume
A5: X is SubSpace of Y;
then
A6: [#]X c= [#]Y by PRE_TOPC:def 4;
A7: p is one-to-one by A3;
set F = p"*f;
p" is continuous by A3;
then consider G being Function of Y,S such that
A8: G is continuous and
A9: G|(the carrier of X) = F by A1,A4,A5;
take g = p*G;
A10: rng p = [#]T by A3;
A11: for x being object st x in dom f holds g.x = f.x
proof
let x be object;
assume
A12: x in dom f;
then
A13: f.x in rng f by FUNCT_1:def 3;
then f.x in the carrier of T;
then
A14: f.x in dom (p") by FUNCT_2:def 1;
x in the carrier of X by A12;
then x in the carrier of Y by A6;
then x in dom G by FUNCT_2:def 1;
hence g.x = p.(G.x) by FUNCT_1:13
.= p.((p"*f).x) by A9,A12,FUNCT_1:49
.= p.(p".(f.x)) by A12,FUNCT_1:13
.= (p*p").(f.x) by A14,FUNCT_1:13
.= (id the carrier of T).(f.x) by A10,A7,TOPS_2:52
.= f.x by A13,FUNCT_1:17;
end;
p is continuous by A3;
hence g is continuous by A8;
dom f = the carrier of X by FUNCT_2:def 1
.= (the carrier of Y) /\ (the carrier of X) by A6,XBOOLE_1:28
.= dom g /\ (the carrier of X) by FUNCT_2:def 1;
hence thesis by A11,FUNCT_1:46;
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 by Th5,Th6;
definition
let X, Y be non empty TopSpace;
redefine pred X is_Retract_of Y means :: redefines is_Retract_of (WAYBEL18, definition)
ex c being continuous Function
of X, Y, r being continuous Function of Y, X st r * c = id X;
compatibility
proof
thus X is_Retract_of Y implies ex c being continuous Function of X, Y, r
being continuous Function of Y, X st r * c = id X
proof
given f being Function of Y, Y such that
A1: f is continuous and
A2: f*f = f and
A3: Image f, X are_homeomorphic;
consider h being Function of Image f, X such that
A4: h is being_homeomorphism by A3;
A5: corestr f is continuous by A1,WAYBEL18:10;
h" is continuous by A4;
then reconsider c = incl Image f * h" as continuous Function of X, Y;
h is continuous by A4;
then reconsider r = h * corestr f as continuous Function of Y, X by A5;
take c, r;
A6: rng h = [#]X by A4;
A7: h is one-to-one by A4;
thus r * c = h * (corestr f * (incl Image f * h")) by RELAT_1:36
.= h * (corestr f * incl Image f * h") by RELAT_1:36
.= h * (id Image f * h") by A2,YELLOW14:35
.= h * h" by FUNCT_2:17
.= id X by A6,A7,TOPS_2:52;
end;
given c being continuous Function of X, Y, r being continuous Function of
Y, X such that
A8: r * c = id X;
take f = c * r;
A9: dom c = the carrier of X by FUNCT_2:def 1
.= rng r by A8,FUNCT_2:18;
then reconsider cf = corestr c as Function of X, Image f by RELAT_1:28;
A10: Image f = Image c by A9,RELAT_1:28;
the carrier of Image c c= the carrier of Y by BORSUK_1:1;
then
id Image c is Function of the carrier of Image c, the carrier of Y by
FUNCT_2:7;
then reconsider q = r * id Image c as Function of Image f, X by A10;
A11: [#]X <> {};
A12: for P being Subset of X st P is open holds q"P is open
proof
let P be Subset of X;
A13: dom id Image c = [#]Image c;
A14: (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 object;
assume
A15: a in (id Image c)"(r"P);
then (id Image c).a in r"P by FUNCT_1:def 7;
then a in r"P by A15,FUNCT_1:18;
hence thesis by A15,XBOOLE_0:def 4;
end;
let a be object;
assume
A16: a in (r"P) /\ [#]Image c;
then a in r"P by XBOOLE_0:def 4;
then (id Image c).a in r"P by A16,FUNCT_1:18;
hence thesis by A13,A16,FUNCT_1:def 7;
end;
assume P is open;
then r"P is open by A11,TOPS_2:43;
then
A17: r"P in the topology of Y;
q"P = (id Image c)"(r"P) by RELAT_1:146;
hence q"P in the topology of Image f by A10,A17,A14,PRE_TOPC:def 4;
end;
A18: r * (cf * cf") = id X * cf" by A8,RELAT_1:36;
thus f is continuous;
thus f * f = c * (r * (c * r)) by RELAT_1:36
.= c * (id X * r) by A8,RELAT_1:36
.= f by FUNCT_2:17;
take h = cf";
thus dom h = [#]Image f by FUNCT_2:def 1;
A19: rng corestr c = [#]Image c by FUNCT_2:def 3;
A20: c is one-to-one by A8,FUNCT_2:23;
hence rng h = [#]X by A10,A19,TOPS_2:49;
(corestr c) qua Function" is one-to-one by A20;
hence h is one-to-one by A10,A20,TOPS_2:def 4;
corestr c is one-to-one by A8,FUNCT_2:23;
then r * id the carrier of Image c = id X * cf" by A10,A19,A18,TOPS_2:52;
then r * id Image c = cf" by FUNCT_2:17;
hence h is continuous by A11,A12,TOPS_2:43;
corestr c is continuous by WAYBEL18:10;
hence thesis by A10,A19,A20,TOPS_2:51;
end;
end;
theorem
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 Function of S, X, r being continuous Function of X,
S such that
A3: r * c = id S;
reconsider rr = r as continuous Function of Y, T by A1,A2,YELLOW12:36;
reconsider cc = c as continuous Function of T, Y by A1,A2,YELLOW12:36;
take cc, rr;
thus 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 Function of S1,S2 such that
A3: G is being_homeomorphism by A1;
consider H being Function of T,T such that
A4: H is continuous and
A5: H*H = H and
A6: Image H, S1 are_homeomorphic by A2;
take H;
consider F being Function of Image H,S1 such that
A7: F is being_homeomorphism by A6;
G*F is being_homeomorphism by A3,A7,TOPS_2:57;
hence thesis by A4,A5;
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 Function of T,T such that
A3: h is continuous and
A4: h*h = h and
A5: Image h, S are_homeomorphic by A2;
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:9;
then ex x being object st x in dom h & W = h.x by FUNCT_1:def 3;
hence thesis by A4,FUNCT_1:13;
end;
then
A6: F is being_a_retraction by BORSUK_1:def 16;
corestr h is continuous by A3,WAYBEL18:10;
then Image h is_a_retract_of T by A6,BORSUK_1:def 17;
then Image h is injective by A1,WAYBEL18:8;
hence thesis by A5,Th6;
end;
theorem ::p.126 exercise 3.13, 1 => 2
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 Function of Y, J such that
A2: f is continuous and
A3: f|(the carrier of J) = id J by WAYBEL18:def 5;
A4: the carrier of J c= the carrier of Y by A1,BORSUK_1:1;
then reconsider ff = f as Function of Y, Y by FUNCT_2:7;
ex ff being Function of Y, Y st ff is continuous & ff*ff = ff & Image ff
, J are_homeomorphic
proof
reconsider M = [#]J as non empty Subset of Y by A1,BORSUK_1:1;
take ff;
thus ff is continuous by A1,A2,PRE_TOPC:26;
A5: dom f = the carrier of Y by FUNCT_2:def 1;
A6: for x being object st x in the carrier of Y holds (f*f).x = f.x
proof
let x be object;
assume
A7: x in the carrier of Y;
hence (f*f).x = f.(f.x) by A5,FUNCT_1:13
.= (id J).(f.x) by A3,A7,FUNCT_1:49,FUNCT_2:5
.= f.x by A7,FUNCT_1:18,FUNCT_2:5;
end;
dom (ff*ff) = the carrier of Y by FUNCT_2:def 1;
hence ff*ff = ff by A5,A6,FUNCT_1:2;
A8: rng f = the carrier of J
proof
thus rng f c= the carrier of J;
let y be object;
assume
A9: y in the carrier of J;
then y in the carrier of Y by A4;
then
A10: y in dom f by FUNCT_2:def 1;
f.y = (f|(the carrier of J)).y by A9,FUNCT_1:49
.= y by A3,A9,FUNCT_1:18;
hence thesis by A10,FUNCT_1:def 3;
end;
the carrier of Y|M = [#](Y|M) .= the carrier of J by PRE_TOPC:def 5;
then Image ff = the TopStruct of J by A1,A8,TSEP_1:5;
hence thesis by YELLOW14:19;
end;
hence thesis;
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 Function 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 FUNCT_2:sch 4;
reconsider g as Function of Y, T;
take g;
A4: dom f = the carrier of X by FUNCT_2:def 1;
A5: for P being Subset of T st P is open holds g"P is open
proof
let P be Subset of T;
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
A6: x in g"P;
then reconsider y = x as Point of Y;
set A = {inf (f.: (V /\ the carrier of X)) where V is open Subset of Y
: y in V};
A c= the carrier of T
proof
let a be object;
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;
A7: inf (f.:([#]Y /\ the carrier of X)) in A;
A8: 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
A9: a = inf (f.:(Va /\ the carrier of X)) and
A10: y in Va;
assume b in A;
then consider Vb being open Subset of Y such that
A11: b = inf (f.:(Vb /\ the carrier of X)) and
A12: y in Vb;
take inf (f.:(Va /\ Vb /\ the carrier of X));
y in Va /\ Vb by A10,A12,XBOOLE_0:def 4;
hence inf (f.:(Va /\ Vb /\ the carrier of X)) in A;
Va /\ Vb /\ the carrier of X c= Vb /\ the carrier of X by XBOOLE_1:17
,26;
then
A13: f.:(Va /\ Vb /\ the carrier of X) c= f.:(Vb /\ the carrier of X
) by RELAT_1:123;
Va /\ Vb /\ the carrier of X c= Va /\ the carrier of X by XBOOLE_1:17
,26;
then
f.:(Va /\ Vb /\ the carrier of X) c= f.:(Va /\ the carrier of X
) by RELAT_1:123;
hence thesis by A9,A11,A13,WAYBEL_7:1;
end;
A14: g.y = sup A by A3;
g.y in P by A6,FUNCT_2:38;
then A meets P by A14,A7,A8,WAYBEL11:def 1;
then consider b being object such that
A15: b in A and
A16: b in P by XBOOLE_0:3;
consider B being open Subset of Y such that
A17: b = inf (f.:(B /\ the carrier of X)) and
A18: y in B by A15;
reconsider b as Element of T by A17;
take B;
thus B is open;
thus B c= g"P
proof
let a be object;
assume
A19: a in B;
then reconsider a as Point of Y;
A20: 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 A17,A19;
then b <= g.a by A20,YELLOW_2:22;
then g.a in P by A16,WAYBEL_0:def 20;
hence thesis by FUNCT_2:38;
end;
thus thesis by A18;
end;
thus thesis;
end;
hence thesis by TOPS_1:25;
end;
set gX = g|(the carrier of X);
A21: the carrier of X c= the carrier of Y by A2,BORSUK_1:1;
A22: for a being object st a in the carrier of X holds gX.a = f.a
proof
let a be object;
assume
a in the carrier of X;
then reconsider x = a as Point of X;
reconsider y = x as Point of Y by A21;
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 object;
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 4;
hence z <= f.x by A24,A26,FUNCT_2:35,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;
V in the topology of X by PRE_TOPC:def 2;
then consider Q being Subset of Y such that
A30: Q in the topology of Y and
A31: V = Q /\ [#]X by A2,PRE_TOPC:def 4;
reconsider Q as open Subset of Y by A30,PRE_TOPC:def 2;
assume x in V;
then y in Q by A31,XBOOLE_0:def 4;
then inf (f.:(Q /\ the carrier of X)) in A;
hence thesis by A28,A31;
end;
A32: b is_>=_than waybelow f.x
proof
let w be Element of T;
A33: wayabove w is open by WAYBEL11:36;
A34: ex_inf_of f.:f"wayabove w,T by YELLOW_0:17;
A35: w <= inf wayabove w by WAYBEL14:9;
ex_inf_of wayabove w,T by YELLOW_0:17;
then inf wayabove w <= inf (f.:f"wayabove w) by A34,FUNCT_1:75
,YELLOW_0:35;
then
A36: w <= inf (f.:f"wayabove w) by A35,ORDERS_2:3;
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
A37: x in f"wayabove w by FUNCT_2:38;
[#]T <> {};
then f"wayabove w is open by A1,A33,TOPS_2:43;
then inf (f.:f"wayabove w) <= b by A29,A37;
hence w <= b by A36,ORDERS_2:3;
end;
f.x = sup waybelow f.x by WAYBEL_3:def 5;
hence thesis by A32,YELLOW_0:32;
end;
thus gX.a = g.y by FUNCT_1:49
.= F(y) by A3
.= f.a by A23,A27,YELLOW_0:30;
end;
[#]T <> {};
hence g is continuous by A5,TOPS_2:43;
dom gX = dom g /\ the carrier of X by RELAT_1:61
.= (the carrier of Y) /\ the carrier of X by FUNCT_2:def 1
.= the carrier of X by A2,BORSUK_1:1,XBOOLE_1:28;
hence thesis by A4,A22,FUNCT_1:2;
end;
registration
let L be complete continuous LATTICE;
cluster Scott -> injective for TopAugmentation of L;
coherence by Th12;
end;
registration
let T be injective non empty TopSpace;
cluster the TopStruct of T -> injective;
coherence by WAYBEL18:16;
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[object, object] 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 object holds [x,y] in R iff x in the carrier of T & y
in the carrier of T & P[x,y] from RELSET_1:sch 1;
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
by A1;
end;
uniqueness
proof
let R1,R2 be strict TopRelStr such that
A2: the TopStruct of R1 = the TopStruct of T and
A3: 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
A4: the TopStruct of R2 = the TopStruct of T and
A5: 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 object;
hereby
assume
A6: [x,y] in the InternalRel of R1;
then reconsider x1 = x, y1 = y as Element of R1 by ZFMISC_1:87;
reconsider x2 = x, y2 = y as Element of R2 by A2,A4,A6,ZFMISC_1:87;
x1 <= y1 by A6;
then ex Y being Subset of T st Y = {y1} & x1 in Cl Y by A3;
then x2 <= y2 by A5;
hence [x,y] in the InternalRel of R2;
end;
assume
A7: [x,y] in the InternalRel of R2;
then reconsider x2 = x, y2 = y as Element of R2 by ZFMISC_1:87;
reconsider x1 = x, y1 = y as Element of R1 by A2,A4,A7,ZFMISC_1:87;
x2 <= y2 by A7;
then ex Y being Subset of T st Y = {y2} & x2 in Cl Y by A5;
then x1 <= y1 by A3;
hence thesis;
end;
hence thesis by A2,A4;
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 thesis;
end;
registration
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;
registration
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;
registration
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;
registration
let T be TopStruct;
cluster Omega T -> reflexive;
coherence
proof
let x be object;
assume
A1: x in the carrier of Omega T;
then reconsider T9 = T as non empty TopStruct;
reconsider a = x as Element of Omega T by A1;
reconsider t9 = x as Element of T9 by A1,Lm1;
consider Y being Subset of T such that
A2: Y = {t9};
A3: Y c= Cl Y by PRE_TOPC:18;
a in Y by A2,TARSKI:def 1;
then a <= a by A2,A3,Def2;
hence thesis;
end;
end;
Lm2: 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 that
A1: X = {x} and
A2: 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 A2,
YELLOW14:21;
hence Cl X c= Cl Y by A1,A2,YELLOW14:22;
end;
assume Cl X c= Cl Y;
hence thesis by A1,YELLOW14:20;
end;
registration
let T be TopStruct;
cluster Omega T -> transitive;
coherence
proof
let x, y, z be object;
assume that
A1: x in the carrier of Omega T and
A2: y in the carrier of Omega T and
A3: z in the carrier of Omega T and
A4: [x,y] in the InternalRel of Omega T and
A5: [y,z] in the InternalRel of Omega T;
reconsider a = x, b = y, c = z as Element of Omega T by A1,A2,A3;
a <= b by A4;
then consider Y2 being Subset of T such that
A6: Y2 = {b} and
A7: a in Cl Y2 by Def2;
the TopStruct of Omega T = the TopStruct of T by Def2;
then reconsider t3=z as Element of T by A3;
b <= c by A5;
then consider Y3 being Subset of T such that
A8: Y3 = {c} and
A9: b in Cl Y3 by Def2;
Y3 = {t3} by A8;
then Cl Y2 c= Cl Y3 by A6,A9,Lm2;
then a <= c by A7,A8,Def2;
hence thesis;
end;
end;
registration
let T be T_0-TopSpace;
cluster Omega T -> antisymmetric;
coherence
proof
let x, y be object;
assume that
A1: x in the carrier of Omega T and
A2: y in the carrier of Omega T and
A3: [x,y] in the InternalRel of Omega T and
A4: [y,x] in the InternalRel of Omega T;
reconsider a = x, b = y as Element of Omega T by A1,A2;
b <= a by A4;
then
A5: ex Y1 being Subset of T st Y1 = {a} & b in Cl Y1 by Def2;
the TopStruct of Omega T = the TopStruct of T by Def2;
then reconsider t1 = x, t2 = y as Element of T by A1,A2;
a <= b by A3;
then ex Y2 being Subset of T st Y2 = {b} & a in Cl Y2 by Def2;
then
for V being Subset of T holds not V is open or (t1 in V implies t2 in
V) & (t2 in V implies t1 in V) by A5,YELLOW14:21;
hence thesis 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 object;
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 reconsider s1 = a, s2 = b as Element of Omega S by ZFMISC_1:87;
reconsider t1 = s1, t2 = s2 as Element of Omega T by A2;
s1 <= s2 by A3;
then consider Y being Subset of S such that
A4: Y = {s2} and
A5: s1 in Cl Y by Def2;
reconsider Z = Y as Subset of T by A1;
t1 in Cl Z by A1,A5,TOPS_3:80;
then t1 <= t2 by A4,Def2;
hence thesis;
end;
assume
A6: [a,b] in the InternalRel of Omega T;
then reconsider s1 = a, s2 = b as Element of Omega T by ZFMISC_1:87;
reconsider t1 = s1, t2 = s2 as Element of Omega S by A2;
s1 <= s2 by A6;
then consider Y being Subset of T such that
A7: Y = {s2} and
A8: s1 in Cl Y by Def2;
reconsider Z = Y as Subset of S by A1;
t1 in Cl Z by A1,A8,TOPS_3:80;
then t1 <= t2 by A7,Def2;
hence thesis;
end;
hence thesis 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 PARTFUN1:def 2
.= dom Carrier (M --> Omega T) by PARTFUN1:def 2;
A2: for i being object
st i in dom Carrier (M --> T) holds (Carrier (M --> T)).
i = (Carrier (M --> Omega T)).i
proof
let i be object;
assume i in dom Carrier (M --> T);
then
A3: i in M;
then consider R1 being 1-sorted such that
A4: R1 = (M --> T).i and
A5: (Carrier (M --> T)).i = the carrier of R1 by PRALG_1:def 15;
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 15;
the carrier of R1 = the carrier of T by A3,A4,FUNCOP_1:7
.= the carrier of Omega T by Lm1
.= the carrier of R2 by A3,A6,FUNCOP_1:7;
hence thesis 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:2;
A9: the carrier of Omega product (M --> T) = the carrier of product (M -->
T) by Lm1;
the InternalRel of Omega product(M --> T) = the InternalRel of product
(M --> Omega T)
proof
let x, y be object;
hereby
assume
A10: [x,y] in the InternalRel of Omega product(M --> T);
then
A11: y in the carrier of Omega product(M --> T) by ZFMISC_1:87;
A12: x in the carrier of Omega product(M --> T) by A10,ZFMISC_1:87;
then reconsider
xp = x, yp = y as Element of product(M --> Omega T) by A8,A11,
YELLOW_1:def 4;
reconsider p1 = x, p2 = y as Element of product(M --> T) by A12,A11,Lm1;
reconsider xo = x, yo = y as Element of Omega product(M --> T) by A10,
ZFMISC_1:87;
A13: xp in product Carrier (M --> Omega T) by A8,A10,ZFMISC_1:87;
then consider f being Function such that
A14: xp = f and
dom f = dom Carrier (M --> Omega T) and
for i being object st i in dom Carrier (M --> Omega T) holds f.i in
Carrier (M --> Omega T).i by CARD_3:def 5;
yp in product Carrier (M --> Omega T) by A8,A10,ZFMISC_1:87;
then consider g being Function such that
A15: yp = g and
dom g = dom Carrier (M --> Omega T) and
for i being object st i in dom Carrier (M --> Omega T) holds g.i in
Carrier (M --> Omega T).i by CARD_3:def 5;
xo <= yo by A10;
then
A16: ex Yp being Subset of product(M --> T) st Yp = {p2} & p1 in Cl Yp
by Def2;
for i being object 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 object;
assume
A17: i in M;
then reconsider j = i as Element of M;
set t1 = p1.j, t2 = p2.j;
reconsider xi = t1, yi = t2 as Element of Omega T by Lm1;
take Omega T, xi, yi;
thus Omega T = (M --> Omega T).i by A17,FUNCOP_1:7;
thus xi = f.i by A14;
thus yi = g.i by A15;
p1.j in Cl {p2.j} by A16,YELLOW14:30;
hence xi <= yi by Def2;
end;
then xp <= yp by A13,A14,A15,YELLOW_1:def 4;
hence [x,y] in the InternalRel of product (M --> Omega T);
end;
assume
A18: [x,y] in the InternalRel of product (M --> Omega T);
then reconsider xp = x, yp = y as Element of product(M --> Omega T) by
ZFMISC_1:87;
A19: xp <= yp by A18;
A20: x in the carrier of product (M --> Omega T) by A18,ZFMISC_1:87;
then xp in product Carrier (M --> Omega T) by YELLOW_1:def 4;
then consider f, g being Function such that
A21: f = xp and
A22: g = yp and
A23: for i being object 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 A19,
YELLOW_1:def 4;
A24: y in the carrier of product (M --> Omega T) by A18,ZFMISC_1:87;
then reconsider
xo = x, yo = y as Element of Omega product(M --> T) by A8,A20,
YELLOW_1:def 4;
reconsider p1 = x, p2 = y as Element of product(M --> T) by A8,A9,A20,A24,
YELLOW_1:def 4;
for i being Element of M holds p1.i in Cl {p2.i}
proof
let i be Element of M;
consider R1 being RelStr, xi, yi being Element of R1 such that
A25: R1 = (M --> Omega T).i and
A26: xi = f.i and
A27: yi = g.i and
A28: xi <= yi by A23;
reconsider xi, yi as Element of Omega T by A25;
xi <= yi by A25,A28;
then ex Y being Subset of T st Y = {yi} & xi in Cl Y by Def2;
hence thesis by A21,A22,A26,A27;
end;
then p1 in Cl {p2} by YELLOW14:30;
then xo <= yo by Def2;
hence thesis;
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;
A1: 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 object;
hereby
assume
A2: [x,y] in the InternalRel of Omega S;
then
A3: y in the carrier of Omega S by ZFMISC_1:87;
x in the carrier of Omega S by A2,ZFMISC_1:87;
then reconsider t1 = x, t2 = y as Element of S by A3,Lm1;
reconsider o1 = x, o2 = y as Element of Omega S by A2,ZFMISC_1:87;
o1 <= o2 by A2;
then ex Y2 being Subset of S st Y2 = {o2} & o1 in Cl Y2 by Def2;
then t1 in downarrow t2 by WAYBEL11:9;
then ex t3 being Element of S st t3 >= t1 & t3 in {t2} by WAYBEL_0:def 15
;
then t1 <= t2 by TARSKI:def 1;
hence [x,y] in the InternalRel of S;
end;
assume
A4: [x,y] in the InternalRel of S;
then reconsider t1 = x, t2 = y as Element of S by ZFMISC_1:87;
reconsider o1 = x, o2 = y as Element of Omega S by A1,A4,ZFMISC_1:87;
A5: t2 in {t2} by TARSKI:def 1;
t1 <= t2 by A4;
then t1 in downarrow t2 by A5,WAYBEL_0:def 15;
then t1 in Cl {t2} by WAYBEL11:9;
then o1 <= o2 by Def2;
hence thesis;
end;
hence thesis by A1;
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;
registration
let S be Scott complete TopLattice;
cluster Omega S -> complete;
coherence
proof
set T = the 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:1;
A2: the carrier of Omega S = the carrier of S by Lm1;
A3: the InternalRel of Omega S c= the InternalRel of Omega T
proof
let x, y be object;
assume
A4: [x,y] in the InternalRel of Omega S;
then reconsider o1 = x, o2 = y as Element of Omega S by ZFMISC_1:87;
A5: y in the carrier of Omega S by A4,ZFMISC_1:87;
then reconsider s2 = y as Element of S by Lm1;
x in the carrier of Omega S by A4,ZFMISC_1:87;
then reconsider o3 = x, o4 = y as Element of Omega T by A1,A2,A5,Lm1;
reconsider t2 = y as Element of T by A1,A2,A5;
Cl {s2} = (Cl {t2}) /\ ([#]S) by PRE_TOPC:17;
then
A6: Cl {s2} c= Cl {t2} by XBOOLE_1:17;
o1 <= o2 by A4;
then ex Y2 being Subset of S st Y2 = {o2} & o1 in Cl Y2 by Def2;
then o3 <= o4 by A6,Def2;
hence thesis;
end;
A7: the InternalRel of Omega S = (the InternalRel of Omega T)|_2 the
carrier of Omega S
proof
let x, y be object;
thus [x,y] in the InternalRel of Omega S implies [x,y] in (the InternalRel
of Omega T)|_2 the carrier of Omega S by A3,XBOOLE_0:def 4;
assume
A8: [x,y] in (the InternalRel of Omega T)|_2 the carrier of Omega S;
then
A9: y in the carrier of Omega S by ZFMISC_1:87;
A10: x in the carrier of Omega S by A8,ZFMISC_1:87;
then reconsider t1 = x, t2 = y as Element of T by A1,A2,A9;
reconsider o1 = x, o2 = y as Element of Omega T by A1,A2,A10,A9,Lm1;
[x,y] in the InternalRel of Omega T by A8,XBOOLE_0:def 4;
then o1 <= o2;
then
A11: ex Y being Subset of T st Y = {t2} & t1 in Cl Y by Def2;
reconsider s1 = x, s2 = y as Element of S by A10,A9,Lm1;
reconsider o3 = x, o4 = y as Element of Omega S by A8,ZFMISC_1:87;
Cl {s2} = (Cl {t2}) /\ [#]S by PRE_TOPC:17;
then s1 in Cl {s2} by A11,XBOOLE_0:def 4;
then o3 <= o4 by Def2;
hence thesis;
end;
the carrier of Omega S c= the carrier of Omega T by A1,A2,Lm1;
hence thesis by A3,A7,YELLOW_0:def 13,def 14;
end;
theorem Th18:
for S, T being TopSpace, h being Function of S, T, g being
Function of Omega S, Omega T st h = g & h is being_homeomorphism holds g is
isomorphic
proof
let S, T be TopSpace, h be Function of S, T, g be Function of Omega S, Omega
T;
assume that
A1: h = g and
A2: h is being_homeomorphism;
A3: dom h = [#]S by A2;
A4: rng h = [#]T by A2;
A5: the carrier of T = the carrier of Omega T by Lm1;
A6: the carrier of S = the carrier of Omega S by Lm1;
A7: h is one-to-one by A2;
per cases;
suppose
A8: S is non empty & T is non empty;
then reconsider s = S, t = T as non empty TopSpace;
reconsider f = g as Function of Omega s, Omega t;
for x, y being Element of Omega s holds x <= y iff f.x <= f.y
proof
let x, y be Element of Omega s;
A9: dom f = [#]S by A1,A2
.= the carrier of S;
reconsider Z = {f".(f.y)} as Subset of s by Lm1;
A10: h" is being_homeomorphism by A2,A8,TOPS_2:56;
A11: f is onto by A1,A4,A5,FUNCT_2:def 3;
then
A12: f" = f qua Function" by A1,A7,TOPS_2:def 4;
A13: dom h = the carrier of Omega s by A3,Lm1;
then
A14: y = (h qua Function)".(h.y) by A7,FUNCT_1:34
.= f".(f.y) by A11,A1,A7,TOPS_2:def 4;
hereby
reconsider Z = {f.y} as Subset of t by Lm1;
assume x <= y;
then consider Y being Subset of s such that
A15: Y = {y} and
A16: x in Cl Y by Def2;
A17: Im(h,y) = Z by A1,A13,FUNCT_1:59;
f.x in f.:Cl Y by A16,FUNCT_2:35;
then h.x in Cl (h.:Y) by A1,A2,TOPS_2:60;
hence f.x <= f.y by A1,A15,A17,Def2;
end;
assume f.x <= f.y;
then consider Y being Subset of t such that
A18: Y = {f.y} and
A19: f.x in Cl Y by Def2;
A20: f" = h" by A1,A5,A6;
A21: x = f".(f.x) by A1,A7,A12,A13,FUNCT_1:34;
f".(f.x) in f".:Cl Y by A19,FUNCT_2:35;
then
A22: h".(h.x) in Cl (h".:Y) by A1,A10,A20,TOPS_2:60;
f".:Y = f"Y by A1,A7,A12,FUNCT_1:85
.= Z by A1,A6,A7,A18,A14,A9,FINSEQ_5:4;
hence thesis by A1,A20,A22,A21,A14,Def2;
end;
hence thesis by A1,A5,A7,A4,WAYBEL_0:66;
end;
suppose
S is empty or T is empty;
then reconsider s = S, t = T as empty TopSpace by A3,A4;
A23: Omega t is empty;
Omega s is empty;
hence thesis by A23,WAYBEL_0:def 38;
end;
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 Function of S, T such that
A1: h is being_homeomorphism;
A2: the carrier of T = the carrier of Omega T by Lm1;
the carrier of S = the carrier of Omega S by Lm1;
then reconsider f = h as Function of Omega S, Omega T by A2;
take f;
thus thesis by A1,Th18;
end;
Lm3: for S, T being non empty RelStr, f being Function of S, S, g being
Function of T, T st the RelStr of S = the RelStr of T & f = g & f is projection
holds g is projection
by WAYBEL_9:1;
::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
let T be injective T_0-TopSpace;
set S = Sierpinski_Space, B = BoolePoset{0};
consider M being non empty set such that
A1: T is_Retract_of product (M --> S) by WAYBEL18:19;
consider f being Function 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;
A5: 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
A6: the RelStr of Omega Image f, Omega T are_isomorphic by A5,WAYBEL_1:7;
Omega Image f is full SubRelStr of Omega product (M --> S) by Th17;
then
A7: 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;
set TL = the Scott TopAugmentation of product(M --> B);
A8: the RelStr of TL = the RelStr of product(M --> B) by YELLOW_9:def 4;
A9: the carrier of TL = the carrier of product(M --> S) by Th3;
then reconsider ff = f as Function of TL, TL;
A10: the topology of TL = the topology of product (M --> S) by WAYBEL18:15;
then
A11: ff is continuous by A2,A9,YELLOW12:36;
then ff is idempotent monotone by A3,QUANTAL1:def 9;
then ff is projection;
then reconsider
g = ff as projection Function of product (M --> B), product (M
--> B) by A8,Lm3;
A12: the InternalRel of Image g = (the InternalRel of (product (M --> B)))
|_2 the carrier of Image g by YELLOW_0:def 14;
the TopStruct of the TopStruct of TL = the TopStruct of TL implies Omega
the TopStruct of TL = Omega TL by Th13;
then
A13: the RelStr of Omega the TopStruct of product(M --> S) = the RelStr of
product (M --> B) by A10,A9,Th16;
g is directed-sups-preserving by A8,A11,WAYBEL21:6;
then
A14: Image g is complete continuous LATTICE by WAYBEL15:15,YELLOW_2:35;
the carrier of Image g = rng g by YELLOW_0:def 15
.= the carrier of Image f by WAYBEL18:9
.= the carrier of Omega Image f by Lm1;
hence thesis by A13,A14,A6,A12,A7,WAYBEL15:9,WAYBEL20:18,YELLOW14:11,12;
end;
registration
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 Function
of Omega X, Omega Y holds f is monotone
proof
let X, Y be non empty TopSpace, f be continuous Function of Omega X, Omega Y;
let x, y be Element of Omega X;
reconsider Z = {f.y} as Subset of Y by Lm1;
assume x <= y;
then consider A being Subset of X such that
A1: A = {y} and
A2: x in Cl A by Def2;
A3: for G being Subset of Y st G is open holds f.x in G implies Z meets G
proof
the carrier of X = the carrier of Omega X by Lm1;
then reconsider g = f as Function of X, Y by Lm1;
let G be Subset of Y such that
A4: G is open and
A5: f.x in G;
A6: x in g"G by A5,FUNCT_2:38;
A7: the TopStruct of Y = the TopStruct of Omega Y by Def2;
A8: f.y in Z by TARSKI:def 1;
the TopStruct of X = the TopStruct of Omega X by Def2;
then
A9: g is continuous by A7,YELLOW12:36;
[#]Y <> {};
then g"G is open by A4,A9,TOPS_2:43;
then A meets g"G by A2,A6,PRE_TOPC:def 7;
then consider m being object such that
A10: m in A /\ g"G by XBOOLE_0:4;
m in A by A10,XBOOLE_0:def 4;
then
A11: m = y by A1,TARSKI:def 1;
m in g"G by A10,XBOOLE_0:def 4;
then f.y in G by A11,FUNCT_2:38;
then Z /\ G <> {}Y by A8,XBOOLE_0:def 4;
hence thesis;
end;
the carrier of Y = the carrier of Omega Y by Lm1;
then f.x in Cl Z by A3,PRE_TOPC:def 7;
hence f.x <= f.y by Def2;
end;
registration
let X, Y be non empty TopSpace;
cluster continuous -> monotone for Function 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
reconsider Z = {x} as Subset of T by A1;
let a be object;
assume
A2: a in Cl {x};
then reconsider b = a as Element of Omega T;
a in Cl Z by A1,A2,TOPS_3:80;
then b <= x by Def2;
hence a in downarrow x by WAYBEL_0:17;
end;
let a be object;
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 thesis by A1,TOPS_3:80;
end;
registration
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
A2: ex Z being Subset of X st Z = {y} & x in Cl Z by Def2;
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 7;
hence thesis by ZFMISC_1:50;
end;
registration
let T be TopSpace;
cluster open -> upper for Subset of Omega T;
coherence by Th23;
end;
Lm4: now
let X, Y be non empty TopSpace, N be net of ContMaps(X,Omega Y);
A1: the carrier of Y = the carrier of Omega Y by Lm1;
the carrier of ContMaps(X,Omega Y) c= Funcs(the carrier of X, the
carrier of Y)
proof
let f be object;
assume f in the carrier of ContMaps(X,Omega Y);
then ex x being Function of X, Omega Y st x = f & x is continuous by
WAYBEL24:def 3;
hence thesis by A1,FUNCT_2:8;
end;
then
A2: Funcs(the carrier of N, the carrier of ContMaps(X,Omega Y)) c= Funcs(the
carrier of N, Funcs(the carrier of X, the carrier of Y)) by FUNCT_5:56;
the mapping of N in Funcs(the carrier of N, the carrier of ContMaps(X,
Omega Y)) by FUNCT_2:8;
hence
the mapping of N in Funcs(the carrier of N, Funcs(the carrier of X, the
carrier of Y)) by A2;
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
the carrier of T c= Funcs(I, the carrier of S) by A1,YELLOW_1:28;
then
A2: Funcs(the carrier of N, the carrier of T) c= Funcs(the carrier of N,
Funcs(I, the carrier of S)) by FUNCT_5:56;
A3: the mapping of N in Funcs(the carrier of N, the carrier of T) by FUNCT_2:8;
then
A4: rng ((commute the mapping of N).i) c= the carrier of S by A2,EQUATION:3;
dom ((commute the mapping of N).i) = the carrier of N by A3,A2,EQUATION:3;
then reconsider
f = (commute(the mapping of N)).i as Function of the carrier of
N, the carrier of S by A4,FUNCT_2:def 1,RELSET_1:4;
set A = NetStr (#the carrier of N, the InternalRel of N, f#);
A5: the RelStr of A = the RelStr of N;
[#]N is directed by WAYBEL_0:def 6;
then [#]A is directed by A5,WAYBEL_0:3;
then reconsider A as strict net of S by A5,WAYBEL_0:def 6,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 Lm4;
ContMaps(X,Omega Y) is SubRelStr of (Omega Y) |^ the carrier of X by
WAYBEL24:def 3;
then the carrier of ContMaps(X,Omega Y) c= the carrier of (Omega Y) |^ the
carrier of X by YELLOW_0:def 13;
hence
(the mapping of commute(N,x,Omega Y)).i = (commute the mapping of N).x.
i by Def3
.= ((the mapping of N).i).x by A1,FUNCT_6:56;
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:58;
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;
then N.a <= N.c by A3;
then Na <= Nc by A1,YELLOW_0:59;
then A <= C by YELLOW_1:def 5;
then
A4: A.x <= C.x by WAYBEL_3:28;
A5: (the mapping of M).c = (the mapping of N).k.x by Th24;
(the mapping of M).a = (the mapping of N).i.x by Th24;
hence thesis by A4,A5;
end;
hence thesis by WAYBEL_0:11;
end;
registration
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;
registration
let X, Y be non empty TopSpace;
cluster -> Function-yielding for net of ContMaps(X,Omega Y);
coherence;
end;
Lm5: now
let X, Y be non empty TopSpace, N be net of ContMaps(X,Omega Y), i be
Element of N;
thus (the mapping of N).i is Function 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 Function of X, Y by WAYBEL24:21;
end;
Lm6: 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);
deffunc F(Element of X) = sup commute(N,$1,Omega Y);
set n = the mapping of N, L = (Omega Y) |^ the carrier of X;
consider f being Function of the carrier of X, the carrier of Omega Y such
that
A2: for u being Element of X holds f.u = F(u) from FUNCT_2:sch 4;
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
take a;
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;
thus rng n is_<=_than a
proof
let k be Element of L;
reconsider k9 = k, a9 = a as Element of product ((the carrier of X) -->
Omega Y) by YELLOW_1:def 5;
assume k in rng n;
then consider i being object such that
A5: i in dom n and
A6: k = n.i by FUNCT_1:def 3;
reconsider i as Point of N by A5;
for u being Element of X holds k9.u <= a9.u
proof
let u be Element of X;
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;
A9: k9.u = (the mapping of commute(N,u,Omega Y)).i by A6,Th24;
dom the mapping of commute(N,u,Omega Y) = the carrier of N by A3,Lm6;
then
A10: k9.u in rng the mapping of commute(N,u,Omega Y) by A9,FUNCT_1:def 3;
a9.u = sup commute(N,u,Omega Y) by A2
.= Sup the mapping of commute(N,u,Omega Y) by WAYBEL_2:def 1
.= sup rng the mapping of commute(N,u,Omega Y);
hence thesis by 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 a9 = a, b9 = b as Element of product ((the carrier of X) -->
Omega Y) by YELLOW_1:def 5;
for u being Element of X holds a9.u <= b9.u
proof
let u be Element of X;
ex_sup_of commute(N,u,Omega Y) by A1;
then
A12: ex_sup_of rng the mapping of commute(N,u,Omega Y), Omega Y;
A13: Omega Y = ((the carrier of X) --> Omega Y).u;
A14: 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 object such that
A15: i in dom the mapping of commute(N,u,Omega Y) and
A16: (the mapping of commute(N,u,Omega Y)).i = s by FUNCT_1:def 3;
reconsider i as Point of N by A3,A15,Lm6;
n.i is Function of X, Omega Y by WAYBEL24:21;
then reconsider k = n.i as Element of L by WAYBEL24:19;
reconsider k9 = k as Element of product ((the carrier of X) --> Omega
Y) by YELLOW_1:def 5;
n.i in rng n by A3,FUNCT_1:def 3;
then k <= b by A11;
then
A17: k9 <= b9 by YELLOW_1:def 5;
s = n.i.u by A16,Th24;
hence s <= b.u by A13,A17,WAYBEL_3:28;
end;
a9.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);
hence thesis by A12,A14,YELLOW_0:30;
end;
hence thesis by A4,WAYBEL_3:28;
end;
hence thesis 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;
W is open by A1,TOPS_3:76;
hence thesis by A2,A3,A4;
end;
Lm7: 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;
set x = the Element of D;
let a be object;
assume a in {d};
then
A2: a = d by TARSKI:def 1;
x in D;
hence thesis by A1,A2,TARSKI:def 1;
end;
end;
registration
cluster trivial -> monotone-convergence for 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;
reconsider d as Element of Omega T by Lm1;
let D be non empty directed Subset of Omega T;
A2: the carrier of T = the carrier of Omega T by Lm1;
then D = {d} by A1,Lm7;
hence ex_sup_of D,Omega T by YELLOW_0:38;
let V be open Subset of T;
A3: {d} meets {d};
assume sup D in V;
then V = {d} by A1,Lm7;
hence thesis by A1,A2,A3,Lm7;
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 Function of S, T such that
A1: h is being_homeomorphism;
the carrier of S = the carrier of Omega S by Lm1;
then reconsider f = h as Function of Omega S, Omega T by Lm1;
f is isomorphic by A1,Th18;
then
A2: rng f = the carrier of Omega T by WAYBEL_0:66;
let D be non empty directed Subset of Omega T;
A3: f" is isomorphic by A1,Th18,YELLOW14:10;
then f" is sups-preserving by WAYBEL13:20;
then
A4: f" preserves_sup_of D;
A5: rng h = [#]T by A1;
A6: h is one-to-one by A1;
A7: h is onto by A5,FUNCT_2:def 3;
f".:D is directed by A3,YELLOW_2:15;
then
A8: f"D is non empty directed Subset of Omega S by A2,A5,A6,TOPS_2:55;
then ex_sup_of f"D,Omega S by Def4;
then ex_sup_of f.:f"D,Omega T by A1,Th18,YELLOW14:16;
hence
A9: ex_sup_of D,Omega T by A2,FUNCT_1:77;
let V be open Subset of T;
assume sup D in V;
then h".sup D in h".:V by FUNCT_2:35;
then h".sup D in h"V by A5,A6,TOPS_2:55;
then h qua Function".sup D in h"V by A7,A6,TOPS_2:def 4;
then f".sup D in h"V by A2,A6,A7,A5,TOPS_2:def 4;
then sup (f".:D) in h"V by A9,A4;
then
A10: sup (f"D) in h"V by A2,A5,A6,TOPS_2:55;
h"V is open by A1,TOPGRP_1:26;
then f"D meets h"V by A8,A10,Def4;
then consider a being object such that
A11: a in f"D and
A12: 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 A11,A12,FUNCT_2:38;
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 ex_sup_of D,Omega S by YELLOW_0:17;
A1: Omega S = the TopRelStr of S by Th15;
then
A2: the RelStr of Omega S = the RelStr of S;
reconsider E = D as Subset of S by A1;
let V be open Subset of S;
assume sup D in V;
then
A3: sup E in V by A2,YELLOW_0:17,26;
E is non empty directed Subset of S by A2,WAYBEL_0:3;
hence thesis by A3,WAYBEL11:def 1;
end;
registration
let L be complete LATTICE;
cluster -> monotone-convergence for Scott TopAugmentation of L;
coherence by Th29;
end;
registration
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;
registration
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;
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;
for V being a_neighborhood of sup N holds N is_eventually_in V
proof
let V be a_neighborhood of sup N;
A1: Int V c= V by TOPS_1:16;
A2: the TopStruct of X = the TopStruct of Omega X by Def2;
then reconsider I = Int V as Subset of X;
A3: I is open by A2,TOPS_3:76;
sup N in I by CONNSP_2:def 1;
then Sup the mapping of N in I by WAYBEL_2:def 1;
then D meets I by A3,Def4;
then consider y being object such that
A4: y in D and
A5: y in I by XBOOLE_0:3;
reconsider y as Point of X by A5;
consider x being object such that
A6: x in dom the mapping of N and
A7: (the mapping of N).x = y by A4,FUNCT_1:def 3;
reconsider x as Element of N by A6;
consider j being Element of N such that
A8: for k being Element of N st j <= k holds N.x <= N.k by WAYBEL_0:11;
take j;
let k be Element of N;
assume j <= k;
then N.x <= N.k by A8;
then consider Y being Subset of X such that
A9: Y = {N.k} and
A10: N.x in Cl Y by Def2;
Y meets I by A3,A5,A7,A10,PRE_TOPC:def 7;
then consider m being object such that
A11: m in Y /\ I by XBOOLE_0:4;
m in Y by A11,XBOOLE_0:def 4;
then
A12: m = N.k by A9,TARSKI:def 1;
m in I by A11,XBOOLE_0:def 4;
hence thesis by A12,A1;
end;
hence thesis by YELLOW_6:def 15;
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;
registration
let X be monotone-convergence non empty TopSpace;
cluster -> convergent for 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;
Net-Str D = NetStr (#D, (the InternalRel of (Omega X))|_2 D, (id the
carrier of (Omega X))|D#) by WAYBEL17:def 4;
then
A2: rng the mapping of Net-Str D = D by YELLOW14:2;
ex_sup_of Net-Str D by A1;
hence ex_sup_of D,Omega X by A2;
let V be open Subset of X such that
A3: sup D in V;
reconsider Z = V as Subset of Omega X by Lm1;
A4: sup Net-Str D = Sup the mapping of Net-Str D by WAYBEL_2:def 1
.= sup rng the mapping of Net-Str D;
the TopStruct of X = the TopStruct of Omega X by Def2;
then Int Z = Int V by TOPS_3:77;
then sup Net-Str D in Int Z by A2,A3,A4,TOPS_1:23;
then
A5: Z is a_neighborhood of sup Net-Str D by CONNSP_2:def 1;
sup Net-Str D in Lim Net-Str D by A1;
then Net-Str D is_eventually_in V by A5,YELLOW_6:def 15;
then consider i being Element of Net-Str D such that
A6: for j being Element of Net-Str D st i <= j holds (Net-Str D).j in V;
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;
hence a in D by A2,FUNCT_1:def 3;
thus a in V by A6;
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 Function 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 Function of Omega X, Omega Y;
let D be non empty directed Subset of Omega X;
assume
A1: ex_sup_of D,Omega X;
set V = (downarrow sup (f.:D))`;
A2: the TopStruct of X = the TopStruct of Omega X by Def2;
then reconsider fV = f"V as Subset of X;
[#]Omega Y <> {};
then f"V is open by TOPS_2:43;
then reconsider fV as open Subset of X by A2,TOPS_3:76;
sup (f.:D) <= sup (f.:D);
then
A3: sup (f.:D) in downarrow sup (f.:D) by WAYBEL_0:17;
A4: 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:14;
let b be Element of Omega Y such that
A5: for c being Element of Omega Y st c in f.:D holds c <= b;
reconsider Z = {b} as Subset of Y by Lm1;
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
A6: G is open and
A7: a in G;
reconsider H = G as open Subset of Omega Y by A4,A6,TOPS_3:76;
[#]Omega Y <> {};
then f"H is open by TOPS_2:43;
then
A8: f"H is open Subset of X by A2,TOPS_3:76;
sup D in f"H by A7,FUNCT_2:38;
then D meets f"H by A8,Def4;
then consider c being object 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;
A11: f.c in H by A10,FUNCT_2:38;
f.c <= b by A5,A9,FUNCT_2:35;
then
A12: b in G by A11,WAYBEL_0:def 20;
b in {b} by TARSKI:def 1;
hence thesis by A12,XBOOLE_0:3;
end;
then a in Cl Z by A4,PRE_TOPC:def 7;
hence thesis by Def2;
end;
hence
A13: ex_sup_of f.:D,Omega Y by YELLOW_0:15;
assume
A14: sup (f.:D) <> f.sup D;
sup (f.:D) <= f.sup D by A1,A13,WAYBEL17:15;
then not f.sup D <= sup (f.:D) by A14,ORDERS_2:2;
then not f.sup D in downarrow sup (f.:D) by WAYBEL_0:17;
then f.sup D in V by XBOOLE_0:def 5;
then sup D in fV by FUNCT_2:38;
then D meets fV by Def4;
then consider d being object such that
A15: d in D and
A16: d in fV by XBOOLE_0:3;
reconsider d as Element of Omega X by A15;
A17: f.d in V by A16,FUNCT_2:38;
f.d <= sup (f.:D) by A13,A15,FUNCT_2:35,YELLOW_4:1;
then sup (f.:D) in V by A17,WAYBEL_0:def 20;
hence contradiction by A3,XBOOLE_0:def 5;
end;
registration
let X be monotone-convergence non empty TopSpace, Y be T_0-TopSpace;
cluster continuous -> directed-sups-preserving for
Function 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 Function of R, T, r being continuous Function of T,
R such that
A1: r * c = id R;
let D be non empty directed Subset of Omega R;
A2: the TopStruct of R = the TopStruct of Omega R by Def2;
then reconsider DR = D as non empty Subset of R;
A3: the TopStruct of T = the TopStruct of Omega T by Def2;
then reconsider f = c*r as Function of Omega T, Omega T;
reconsider rr = r as Function of Omega T, Omega R by A3,A2;
A4: r.:(c.:D) = (r*c).:DR by RELAT_1:126
.= D by A1,FUNCT_1:92;
reconsider cc = c as Function of Omega R, Omega T by A3,A2;
cc is continuous by A3,A2,YELLOW12:36;
then
A5: cc.:D is directed by YELLOW_2:15;
then
A6: ex_sup_of cc.:D, Omega T by Def4;
f is continuous by A3,YELLOW12:36;
then
A7: f preserves_sup_of cc.:D by A5,WAYBEL_0:def 37;
rr is continuous by A3,A2,YELLOW12:36;
then
A8: rr preserves_sup_of cc.:D by A5,WAYBEL_0:def 37;
hence ex_sup_of D, Omega R by A6,A4;
A9: c.sup D = c.(r.sup(cc.:D)) by A6,A4,A8
.= f.sup(cc.:D) by A3,FUNCT_2:15
.= sup(f.:(cc.:D)) by A6,A7
.= sup (cc.:D) by A4,RELAT_1:126;
let V be open Subset of R;
assume sup D in V;
then
A10: c.sup D in c.:V by FUNCT_2:35;
A11: c.:V c= r"V
proof
let a be object;
assume a in c.:V;
then consider x being object such that
A12: x in the carrier of R and
A13: x in V and
A14: a = c.x by FUNCT_2:64;
reconsider x as Point of R by A12;
A15: a = c.x by A14;
r.a = (r*c).x by A14,FUNCT_2:15
.= x by A1;
hence thesis by A13,A15,FUNCT_2:38;
end;
[#]R <> {};
then r"V is open by TOPS_2:43;
then c.:D meets r"V by A5,A11,A9,A10,Def4;
then consider d being object such that
A16: d in cc.:D and
A17: d in r"V by XBOOLE_0:3;
now
take a = r.d;
thus a in D by A4,A16,FUNCT_2:35;
thus a in V by A17,FUNCT_2:38;
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
set SS = Sierpinski_Space, B = BoolePoset{0};
let T be injective T_0-TopSpace, S be Scott TopAugmentation of Omega T;
consider M being non empty set such that
A1: T is_Retract_of product (M --> SS) by WAYBEL18:19;
consider c being continuous Function of T, product (M --> SS), r being
continuous Function of product (M --> SS), T such that
A2: r * c = id T by A1;
A3: the TopStruct of T = the TopStruct of Omega T by Def2;
A4: the TopStruct of product (M --> SS) = the TopStruct of Omega product (M
--> SS) by Def2;
then reconsider
c1a = c as Function of Omega T, Omega product (M --> SS) by A3;
set S2M = the Scott TopAugmentation of product (M --> B);
A5: the TopStruct of S = the TopStruct of S;
A6: the RelStr of S2M = the RelStr of product (M --> B) by YELLOW_9:def 4;
then reconsider c1 = c as Function of Omega T, product (M --> B) by A3,Th3;
A7: the RelStr of S = the RelStr of Omega T by YELLOW_9:def 4;
then reconsider c2 = c1 as Function of S, S2M by A6;
A8: the carrier of S2M = the carrier of product (M --> SS) by Th3;
then reconsider rr = r as Function of S2M, T;
A9: the topology of S2M = the topology of product (M --> SS) by WAYBEL18:15;
then reconsider W = T as monotone-convergence non empty TopSpace by A1,A8
,Th36;
Omega product (M --> SS) = Omega S2M by A9,A8,Th13;
then
A10: the RelStr of Omega product (M --> SS) = the RelStr of product (M --> B
) by Th16
.= the RelStr of S2M by YELLOW_9:def 4;
reconsider r1 = r as Function of product (M --> B), Omega T by A8,A6,A3;
A11: the RelStr of Omega S2M = the RelStr of product (M --> B) by Th16;
then reconsider rr1 = r1 as Function of Omega S2M, Omega T;
reconsider r2 = r1 as Function of S2M, S by A6,A7;
reconsider r3 = r2 as Function of product (M --> SS), S by Th3;
the TopStruct of Omega S2M = the TopStruct of S2M by Def2;
then rr1 is continuous by A9,A8,A3,YELLOW12:36;
then r2 is directed-sups-preserving by A6,A7,A11,WAYBEL21:6;
then r3 is continuous by A9,A8,A5,YELLOW12:36;
then
A12: r3 * c is continuous;
reconsider c1a as continuous Function of Omega W, Omega product (M --> SS)
by A3,A4,YELLOW12:36;
c2 = c1a;
then
A13: c2 is directed-sups-preserving by A7,A10,WAYBEL21:6;
the TopStruct of T = the TopStruct of T;
then rr is continuous by A9,A8,YELLOW12:36;
then rr * c2 is continuous by A13;
hence thesis by A2,A12,YELLOW14:33;
end;
theorem
for T being injective T_0-TopSpace holds T is compact locally-compact sober
proof
let T be injective T_0-TopSpace;
set S = the Scott TopAugmentation of Omega T;
A1: S is compact locally-compact sober by WAYBEL14:32;
the TopStruct of S = the TopStruct of T by Th37;
hence thesis by A1,YELLOW14:26,27,28;
end;
theorem Th39:
for T being injective T_0-TopSpace holds T is monotone-convergence
proof
let T be injective T_0-TopSpace;
set S = the Scott TopAugmentation of Omega T;
the TopStruct of S = the TopStruct of T by Th37;
hence thesis by Th27;
end;
registration
cluster injective -> monotone-convergence for 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 Function of X,
Omega Y st f = "\/"(rng the mapping of N, (Omega Y) |^ the carrier of X) &
ex_sup_of rng the mapping of N, (Omega Y) |^ the carrier of X & g in rng the
mapping of N holds g <= f
proof
let X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace, N be
net of ContMaps(X,Omega Y), f, g be Function 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;
hence thesis by A1,WAYBEL10:11;
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
Function of X, Omega Y st (for a being Point of X holds commute(N,a,Omega Y) is
eventually-directed) & f = "\/"(rng the mapping of N, (Omega Y) |^ the carrier
of X) holds f.x = sup commute(N,x,Omega Y)
proof
let X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace, N be
net of ContMaps(X,Omega Y), x be Point of X, f be Function 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: 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
A4: ex_sup_of rng n,L by Th26;
A5: dom n = the carrier of N by FUNCT_2:def 1;
then
A6: dom m = the carrier of N by Lm6;
A7: 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;
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));
A8: Omega Y = ((the carrier of X) --> Omega Y).x;
A9: 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;
end;
suppose
A10: e <> x;
reconsider e as Element of X;
take sup commute(N,e,Omega Y);
thus thesis by A10;
end;
end;
consider t being Function of the carrier of X, the carrier of Omega Y such
that
A11: for u being Element of X holds P[u,t.u] from FUNCT_2:sch 3(A9);
reconsider t as Function of X, Omega Y;
reconsider tt = t as Element of L by WAYBEL24:19;
reconsider p = "\/"(rng n,L), q = tt as Element of product ((the carrier
of X) --> Omega Y) by YELLOW_1:def 5;
assume
A12: for e being Element of Omega Y st e in rng m holds e <= a;
tt is_>=_than rng n
proof
let s be Element of L;
reconsider ss = s as Function of X, Omega Y by WAYBEL24:19;
reconsider s9 = s, t9 = tt as Element of product ((the carrier of X) -->
Omega Y) by YELLOW_1:def 5;
assume s in rng n;
then consider i being object such that
A13: i in dom n and
A14: s = n.i by FUNCT_1:def 3;
reconsider i as Point of N by A13;
A15: for j being Element of X holds s9.j <= t9.j
proof
let j be Element of X;
A17: ss.j = (the mapping of commute(N,j,Omega Y)).i by A14,Th24;
per cases;
suppose
j <> x;
then ex u being Element of X st j = u & t.j = sup commute(N,u,Omega
Y) by A11;
then
A18: t9.j = Sup the mapping of commute(N,j,Omega Y) by WAYBEL_2:def 1
.= sup rng the mapping of commute(N,j,Omega Y);
commute(N,j,Omega Y) is eventually-directed by A1;
then ex_sup_of commute(N,j,Omega Y) by Th31;
then
A19: ex_sup_of rng the mapping of commute(N,j,Omega Y), Omega Y;
i in dom the mapping of commute(N,j,Omega Y) by A13,Lm6;
then ss.j in rng the mapping of commute(N,j,Omega Y) by A17,
FUNCT_1:def 3;
hence thesis by A18,A19,YELLOW_4:1;
end;
suppose
A20: j = x;
A21: m.i in rng m by A6,FUNCT_1:def 3;
ss.x = m.i by A14,Th24;
then ss.x <= a by A12,A21;
hence thesis by A11,A20;
end;
end;
L = product ((the carrier of X) --> Omega Y) by YELLOW_1:def 5;
hence s <= tt by A15,WAYBEL_3:28;
end;
then "\/"(rng n,L) <= tt by A4,YELLOW_0:30;
then
A22: p <= q by YELLOW_1:def 5;
tt.x = a by A11;
hence thesis by A2,A8,A22,WAYBEL_3:28;
end;
rng m is_<=_than f.x
proof
let w be Element of Omega Y;
assume w in rng m;
then consider i being object such that
A23: i in dom m and
A24: m.i = w by FUNCT_1:def 3;
reconsider i as Point of N by A5,A23,Lm6;
reconsider g = n.i as Function of X, Omega Y by Lm5;
g in rng n by A5,FUNCT_1:def 3;
then g <= f by A2,A3,Th26,Th40;
then ex a, b being Element of Omega Y st a = g.x & b = f.x & a <= b;
hence w <= f.x by A24,Th24;
end;
hence f.x = Sup the mapping of commute(N,x,Omega Y) by A7,YELLOW_0:30
.= 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 Function 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;
reconsider fo = "\/"(rng m,L) as Function of X, Omega Y by WAYBEL24:19;
A2: the TopStruct of Y = the TopStruct of Omega Y by Def2;
then reconsider f = fo as Function of X, Y;
A3: dom m = the carrier of N by FUNCT_2:def 1;
A4: for V being Subset of Y st V is open holds f"V is open
proof
let V be Subset of Y such that
A5: V is open;
set M = {A where A is Subset of X: ex i being Element of N, g being
Function of X, Omega Y st g = N.i & A = g"V};
for x being object holds x in f"V iff x in union M
proof
let x be object;
A6: dom f = the carrier of X by FUNCT_2:def 1;
thus x in f"V implies x in union M
proof
A7: m in Funcs(the carrier of N, Funcs(the carrier of X, the carrier
of Y)) by Lm4;
assume
A8: x in f"V;
then
A9: f.x in V by FUNCT_2:38;
reconsider x as Point of X by A8;
set NET = commute(N,x,Omega Y);
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 W;
then W meets V by A5,A9,Def4;
then consider k being object such that
A10: k in W and
A11: k in V by XBOOLE_0:3;
consider i being object such that
A12: i in dom netmap(NET,Omega Y) and
A13: k = netmap(NET,Omega Y).i by A10,FUNCT_1:def 3;
ContMaps(X,Omega Y) is SubRelStr of (Omega Y) |^ the carrier of X
by WAYBEL24:def 3;
then
A14: the carrier of ContMaps(X,Omega Y) c= the carrier of (Omega Y) |^
the carrier of X by YELLOW_0:def 13;
then the RelStr of NET = the RelStr of N by Def3;
then reconsider i as Element of N by A12;
reconsider g = N.i as Function of X, Omega Y by WAYBEL24:21;
A15: dom g = the carrier of X by FUNCT_2:def 1;
A16: g"V in M;
netmap(NET,Omega Y).i = (commute the mapping of N).x.i by A14,Def3
.= ((the mapping of N).i).x by A7,FUNCT_6:56;
then x in g"V by A11,A13,A15,FUNCT_1:def 7;
hence 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 Function of X, Omega Y st g =
N.i & A = g"V by A18;
consider i being Element of N, g being Function of X, Omega Y such that
A21: g = N.i and
A22: A = g"V by A20;
A23: g.x in V by A17,A19,A22,FUNCT_1:def 7;
A24: for x being Point of X holds ex_sup_of commute(N,x,Omega Y)
proof
let x be Point of X;
commute(N,x,Omega Y) is eventually-directed by A1;
hence thesis by Th31;
end;
reconsider x as Element of X by A17,A19;
m.i in rng m by A3,FUNCT_1:def 3;
then g <= fo by A21,A24,Th26,Th40;
then ex a, b being Element of Omega Y st a = g.x & b = fo.x & a <= b;
then consider O being Subset of Y such that
A25: O = {f.x} and
A26: g.x in Cl O by Def2;
V meets O by A5,A23,A26,PRE_TOPC:def 7;
then consider w being object such that
A27: w in V /\ O by XBOOLE_0:4;
w in O by A27,XBOOLE_0:def 4;
then
A28: w = f.x by A25,TARSKI:def 1;
w in V by A27,XBOOLE_0:def 4;
hence thesis by A6,A28,FUNCT_1:def 7;
end;
then
A29: f"V = union M by TARSKI:2;
M c= bool the carrier of X
proof
let m be object;
assume m in M;
then ex A being Subset of X st m = A & ex i being Element of N, g being
Function of X, Omega Y st g = N.i & A = g"V;
hence thesis;
end;
then reconsider M as Subset-Family of X;
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
A30: P = A and
A31: ex i being Element of N, g being Function of X, Omega Y st g =
N.i & A = g"V;
consider i being Element of N, g being Function of X, Omega Y such that
A32: g = N.i and
A33: A = g"V by A31;
consider g9 being Function of X, Omega Y such that
A34: g = g9 and
A35: g9 is continuous by A32,WAYBEL24:def 3;
the TopStruct of X = the TopStruct of X;
then reconsider g99 = g9 as continuous Function of X, Y by A2,A35,
YELLOW12:36;
[#]Y <> {};
then g99"V is open by A5,TOPS_2:43;
hence thesis by A30,A33,A34;
end;
hence thesis by A29,TOPS_2:19;
end;
[#]Y <> {};
hence thesis by A4,TOPS_2:43;
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 X = the TopStruct of X;
for x being Point of X holds commute(N,x,Omega Y) is eventually-directed;
then
A3: "\/"(rng the mapping of N, (Omega Y) |^ the carrier of X) is
continuous Function of X, Y by Th42;
the TopStruct of Y = the TopStruct of Omega Y by Def2;
then "\/"(rng the mapping of N, (Omega Y) |^ the carrier of X) is
continuous Function 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;