Copyright (c) 1999 Association of Mizar Users
environ
vocabulary YELLOW_1, PBOOLE, CARD_3, WAYBEL_3, MONOID_0, FUNCT_1, WAYBEL18,
PRE_TOPC, ORDERS_1, WAYBEL24, WAYBEL25, RELAT_2, TSP_1, ORDINAL2, CAT_1,
YELLOW_0, GROUP_1, BOOLE, YELLOW_9, WAYBEL11, FUNCT_3, RELAT_1, WELLORD1,
SEQ_1, T_0TOPSP, WAYBEL_0, SEQM_3, BINOP_1, QUANTAL1, FUNCOP_1, SUBSET_1,
BORSUK_1, GROUP_6, YELLOW16, TOPS_2, BHSP_3, REALSET1, URYSOHN1,
LATTICE3, LATTICES, FUNCTOR0, WAYBEL_1, PRALG_2, RLVECT_2, FUNCT_2,
PROB_1, CANTOR_1, FUNCT_4, WAYBEL_9, MCART_1, FINSET_1, FUNCT_5,
SETFAM_1, TARSKI, WAYBEL26;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, MCART_1, FINSET_1,
RELAT_1, FUNCT_1, RELSET_1, TOPS_2, FUNCT_3, FUNCT_4, FUNCT_5, STRUCT_0,
REALSET1, PROB_1, CARD_3, ZF_FUND1, PBOOLE, MONOID_0, PRALG_1, PRALG_2,
PRALG_3, PRE_CIRC, FUNCT_7, WELLORD1, ORDERS_1, LATTICE3, FUNCT_2,
GRCAT_1, PRE_TOPC, TSP_1, CANTOR_1, URYSOHN1, T_0TOPSP, BORSUK_1,
QUANTAL1, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_9,
WAYBEL_3, WAYBEL_9, WAYBEL11, WAYBEL18, WAYBEL24, WAYBEL25, YELLOW16;
constructors ENUMSET1, SEQM_3, ORDERS_3, WAYBEL_5, WAYBEL_1, WAYBEL17,
ZF_FUND1, QUANTAL1, GRCAT_1, CANTOR_1, TOPS_2, TSP_1, TDLAT_3, YELLOW_9,
URYSOHN1, NATTRA_1, TOLER_1, PRALG_3, FUNCT_7, WAYBEL18, WAYBEL24,
WAYBEL25, YELLOW16, MONOID_0, PROB_1;
clusters STRUCT_0, WAYBEL_0, WAYBEL_3, RELSET_1, YELLOW_1, LATTICE3, BORSUK_2,
WAYBEL10, WAYBEL17, YELLOW_9, YELLOW_0, FUNCT_1, SUBSET_1, MONOID_0,
PRE_TOPC, TOPS_1, TSP_1, YELLOW_2, YELLOW_6, WAYBEL_2, YELLOW14,
WAYBEL18, WAYBEL24, WAYBEL25, FINSET_1, YELLOW16, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, RELAT_1, MONOID_0, YELLOW_0, BORSUK_1, WAYBEL_0, WAYBEL_1,
T_0TOPSP, YELLOW16, URYSOHN1, XBOOLE_0;
theorems YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, PRE_TOPC, BORSUK_1,
TOPMETR, ORDERS_1, YELLOW12, WAYBEL10, WAYBEL24, WAYBEL25, RELAT_1,
FUNCT_2, FUNCT_1, TOPS_2, TOPS_3, ENUMSET1, FUNCT_3, WAYBEL_3, PBOOLE,
FUNCOP_1, CARD_3, TARSKI, ZFMISC_1, RELSET_1, WELLORD1, TSP_1, TOPS_1,
WAYBEL21, GRCAT_1, QUANTAL1, CANTOR_1, FUNCT_7, YELLOW_9, WAYBEL18,
WAYBEL20, MCART_1, YELLOW14, WAYBEL11, FINSET_1, WAYBEL15, REALSET1,
PRALG_1, PRALG_2, YELLOW16, WAYBEL14, FUNCT_5, CARD_5, PRALG_3, SETFAM_1,
XBOOLE_0, XBOOLE_1;
schemes FUNCT_1, PRALG_2, COMPTS_1;
begin
definition
let I be set;
let J be RelStr-yielding ManySortedSet of I;
redefine func product J; synonym I-POS_prod J;
end;
definition
let I be set;
let J be RelStr-yielding non-Empty ManySortedSet of I;
cluster I-POS_prod J -> constituted-Functions;
coherence
proof let a be Element of I-POS_prod J;
thus a is Function;
end;
end;
definition
let I be set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
redefine func product J; synonym I-TOP_prod J;
end;
:: 4.1. DEFINITION (a)
definition
let X,Y be non empty TopSpace;
func oContMaps(X, Y) -> non empty strict RelStr equals:
Def1:
ContMaps(X, Omega Y);
coherence;
end;
definition
let X,Y be non empty TopSpace;
cluster oContMaps(X, Y) -> reflexive transitive constituted-Functions;
coherence
proof oContMaps(X, Y) = ContMaps(X, Omega Y) by Def1;
hence thesis;
end;
end;
definition
let X be non empty TopSpace;
let Y be non empty T_0 TopSpace;
cluster oContMaps(X, Y) -> antisymmetric;
coherence
proof oContMaps(X, Y) = ContMaps(X, Omega Y) by Def1;
hence thesis;
end;
end;
theorem Th1:
for X,Y being non empty TopSpace
for a being set holds
a is Element of oContMaps(X, Y) iff a is continuous map of X, Omega Y
proof let X,Y be non empty TopSpace;
let a be set;
A1: oContMaps(X, Y) = ContMaps(X, Omega Y) by Def1;
hereby assume a is Element of oContMaps(X,Y);
then a in the carrier of ContMaps(X, Omega Y) by A1;
then ex f being map of X, Omega Y st a = f & f is continuous
by WAYBEL24:def 3;
hence a is continuous map of X, Omega Y;
end;
assume a is continuous map of X, Omega Y;
then a in the carrier of ContMaps(X, Omega Y) by WAYBEL24:def 3;
hence thesis by A1;
end;
theorem Th2:
for X,Y being non empty TopSpace
for a being set holds
a is Element of oContMaps(X, Y) iff a is continuous map of X, Y
proof let X,Y be non empty TopSpace;
let a be set;
A1: the TopStruct of Omega Y = the TopStruct of Y by WAYBEL25:def 2;
A2: the TopStruct of X = the TopStruct of X;
hereby assume a is Element of oContMaps(X,Y);
then a is continuous map of X, Omega Y by Th1;
hence a is continuous map of X, Y by A1,A2,YELLOW12:36;
end;
assume
a is continuous map of X, Y;
then a is continuous map of X, Omega Y by A1,A2,YELLOW12:36
;
hence thesis by Th1;
end;
theorem Th3: :: see yellow14:9
for X,Y being non empty TopSpace
for a,b being Element of oContMaps(X,Y)
for f,g being map of X, Omega Y
st a = f & b = g holds a <= b iff f <= g
proof let X,Y be non empty TopSpace;
let a,b be Element of oContMaps(X,Y);
let f,g be map of X, Omega Y such that
A1: a = f & b = g;
oContMaps(X,Y) = ContMaps(X, Omega Y) by Def1;
then A2: oContMaps(X,Y) is full SubRelStr of (Omega Y)|^the carrier of X
by WAYBEL24:def 3;
then reconsider x = a, y = b as Element of (Omega Y)|^the carrier of X
by YELLOW_0:59;
a <= b iff x <= y by A2,YELLOW_0:60,61;
hence thesis by A1,WAYBEL10:12;
end;
definition
let X,Y be non empty TopSpace;
let x be Point of X;
let A be Subset of oContMaps(X,Y);
redefine func pi(A,x) -> Subset of Omega Y;
coherence
proof set XY = oContMaps(X, Y);
XY = ContMaps(X, Omega Y) by Def1;
then XY is SubRelStr of (Omega Y)|^the carrier of X by WAYBEL24:def 3;
then the carrier of XY c= the carrier of (Omega Y)|^the carrier of X
by YELLOW_0:def 13;
then A c= the carrier of (Omega Y)|^the carrier of X by XBOOLE_1:1;
then reconsider A as Subset of (Omega Y)|^the carrier of X;
pi(A,x) is Subset of Omega Y;
hence thesis;
end;
end;
definition
let X,Y be non empty TopSpace;
let x be set;
let A be non empty Subset of oContMaps(X,Y);
cluster pi(A,x) -> non empty;
coherence
proof set XY = oContMaps(X, Y);
XY = ContMaps(X, Omega Y) by Def1;
then XY is SubRelStr of (Omega Y)|^the carrier of X by WAYBEL24:def 3;
then the carrier of XY c= the carrier of (Omega Y)|^the carrier of X
by YELLOW_0:def 13;
then A c= the carrier of (Omega Y)|^the carrier of X by XBOOLE_1:1;
then reconsider A as non empty Subset of (Omega Y)|^the carrier of X
;
pi(A,x) <> {};
hence thesis;
end;
end;
theorem Th4:
Omega Sierpinski_Space is TopAugmentation of BoolePoset 1
proof
BoolePoset 1 = InclPoset bool 1 by YELLOW_1:4;
then A1: the carrier of BoolePoset 1 = {0,1} by YELLOW14:1,YELLOW_1:1;
A2: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
consider S being strict Scott TopAugmentation of BoolePoset 1;
the topology of S = the topology of Sierpinski_Space &
the RelStr of S = BoolePoset 1 by WAYBEL18:13,YELLOW_9:def 4;
then Omega Sierpinski_Space = Omega S by A1,A2,WAYBEL25:13 .= S by WAYBEL25
:15;
hence thesis;
end;
theorem Th5:
for X being non empty TopSpace
ex f being map of InclPoset the topology of X, oContMaps(X, Sierpinski_Space)
st f is isomorphic &
for V being open Subset of X holds f.V = chi(V, the carrier of X)
proof let X be non empty TopSpace;
deffunc F(set) = chi($1, the carrier of X);
consider f being Function such that
A1: dom f = the topology of X and
A2: for a being set st a in the topology of X holds f.a = F(a) from Lambda;
A3: the carrier of InclPoset the topology of X = the topology of X
by YELLOW_1:1;
rng f c= the carrier of oContMaps(X, Sierpinski_Space)
proof let x be set; assume x in rng f;
then consider a being set such that
A4: a in dom f & x = f.a by FUNCT_1:def 5;
reconsider a as Subset of X by A1,A4;
a is open by A1,A4,PRE_TOPC:def 5;
then chi(a, the carrier of X) is continuous map of X, Sierpinski_Space
by YELLOW16:48;
then x is continuous map of X, Sierpinski_Space by A1,A2,A4;
then x is Element of oContMaps(X, Sierpinski_Space) by Th2;
hence thesis;
end;
then f is Function of the topology of X, the carrier of
oContMaps(X, Sierpinski_Space) by A1,FUNCT_2:4;
then reconsider f as map of InclPoset the topology of X,
oContMaps(X, Sierpinski_Space) by A3;
take f;
set S = InclPoset the topology of X;
set T = oContMaps(X, Sierpinski_Space);
A5: f is one-to-one
proof let x,y be Element of S;
x in the topology of X & y in the topology of X by A3;
then reconsider V = x, W = y as Subset of X;
f.x = chi(V, the carrier of X) & f.y = chi(W, the carrier of X)
by A2,A3;
hence thesis by FUNCT_3:47;
end;
A6: rng f = the carrier of T
proof thus rng f c= the carrier of T;
let t be set; assume t in the carrier of T;
then t is Element of T;
then reconsider g = t as continuous map of X, Sierpinski_Space by Th2;
the topology of Sierpinski_Space = {{}, {1}, {0,1}}
by WAYBEL18:def 9;
then {1} in the topology of Sierpinski_Space by ENUMSET1:14;
then reconsider V = {1} as open Subset of Sierpinski_Space
by PRE_TOPC:def 5;
A7: g"V is open by TOPS_2:55;
then A8: g"V in the topology of X by PRE_TOPC:def 5;
then A9: f.(g"V) = chi(g"V, the carrier of X) by A2;
reconsider c = chi(g"V, the carrier of X) as map of X, Sierpinski_Space
by A7,YELLOW16:48;
now let x be Element of X;
the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
then A10: g.x = 0 or g.x = 1 by TARSKI:def 2;
x in g"V or not x in g"V;
then g.x in V & c.x = 1 or not g.x in V & c.x = 0
by FUNCT_2:46,FUNCT_3:def 3;
hence g.x = c.x by A10,TARSKI:def 1;
end;
then g = c by YELLOW_2:9;
hence thesis by A1,A8,A9,FUNCT_1:def 5;
end;
now let x,y be Element of S;
x in the topology of X & y in the topology of X by A3;
then reconsider V = x, W = y as open Subset of X
by PRE_TOPC:def 5;
set cx = chi(V, the carrier of X), cy = chi(W, the carrier of X);
A11: f.x = cx & f.y = cy by A2,A3;
cx is continuous map of X, Sierpinski_Space &
cy is continuous map of X, Sierpinski_Space by YELLOW16:48;
then cx is Element of oContMaps(X,Sierpinski_Space) &
cy is Element of oContMaps(X,Sierpinski_Space) by Th2;
then reconsider cx, cy as continuous map of X, Omega Sierpinski_Space by
Th1;
x <= y iff V c= W by YELLOW_1:3;
then x <= y iff cx <= cy by Th4,YELLOW16:51;
hence x <= y iff f.x <= f.y by A11,Th3;
end;
hence f is isomorphic by A5,A6,WAYBEL_0:66;
let V be open Subset of X;
V in the topology of X by PRE_TOPC:def 5;
hence thesis by A2;
end;
theorem Th6:
for X being non empty TopSpace holds
InclPoset the topology of X, oContMaps(X, Sierpinski_Space) are_isomorphic
proof let X be non empty TopSpace;
consider f being map of InclPoset the topology of X,
oContMaps(X, Sierpinski_Space) such that
A1: f is isomorphic and
for V being open Subset of X holds f.V = chi(V, the carrier of X)
by Th5;
take f; thus thesis by A1;
end;
:: 4.1. DEFINITION (b)
definition
let X,Y,Z be non empty TopSpace;
let f be continuous map of Y,Z;
func oContMaps(X, f) -> map of oContMaps(X, Y), oContMaps(X, Z) means:
Def2:
for g being continuous map of X,Y holds it.g = f*g;
uniqueness
proof let G1,G2 be map of oContMaps(X, Y), oContMaps(X, Z) such that
A1: for g being continuous map of X,Y holds G1.g = f*g and
A2: for g being continuous map of X,Y holds G2.g = f*g;
now thus the carrier of oContMaps(X, Z) <> {};
let x be Element of oContMaps(X, Y);
reconsider g = x as continuous map of X, Y by Th2;
thus G1.x = f*g by A1 .= G2.x by A2;
end;
hence thesis by FUNCT_2:113;
end;
existence
proof
deffunc F(set) = $1(#)f;
consider F being Function such that
A3: dom F = the carrier of oContMaps(X, Y) and
A4: for x being set st x in the carrier of oContMaps(X, Y) holds F.x = F(x)
from Lambda;
rng F c= the carrier of oContMaps(X, Z)
proof let y be set; assume y in rng F;
then consider x being set such that
A5: x in dom F & y = F.x by FUNCT_1:def 5;
x is Element of oContMaps(X,Y) by A3,A5;
then reconsider g = x as continuous map of X,Y by Th2;
y = g(#)f by A3,A4,A5 .= f*g by YELLOW16:1;
then y is Element of oContMaps(X,Z) by Th2;
hence thesis;
end;
then F is Function of the carrier of oContMaps(X, Y),
the carrier of oContMaps(X, Z) by A3,FUNCT_2:4;
then reconsider F as map of oContMaps(X, Y), oContMaps(X, Z);
take F; let g be continuous map of X,Y;
g is Element of oContMaps(X,Y) by Th2;
hence F.g = g(#)f by A4 .= f*g by YELLOW16:1;
end;
func oContMaps(f, X) -> map of oContMaps(Z, X), oContMaps(Y, X) means:
Def3:
for g being continuous map of Z, X holds it.g = g*f;
uniqueness
proof let G1,G2 be map of oContMaps(Z, X), oContMaps(Y, X) such that
A6: for g being continuous map of Z,X holds G1.g = g*f and
A7: for g being continuous map of Z,X holds G2.g = g*f;
now thus the carrier of oContMaps(Y, X) <> {};
let x be Element of oContMaps(Z, X);
reconsider g = x as continuous map of Z, X by Th2;
thus G1.x = g*f by A6 .= G2.x by A7;
end;
hence thesis by FUNCT_2:113;
end;
existence
proof
deffunc F(set) = f(#)$1;
consider F being Function such that
A8: dom F = the carrier of oContMaps(Z, X) and
A9: for x being set st x in the carrier of oContMaps(Z, X)
holds F.x = F(x) from Lambda;
rng F c= the carrier of oContMaps(Y, X)
proof let y be set; assume y in rng F;
then consider x being set such that
A10: x in dom F & y = F.x by FUNCT_1:def 5;
x is Element of oContMaps(Z,X) by A8,A10;
then reconsider g = x as continuous map of Z,X by Th2;
y = f(#)g by A8,A9,A10 .= g*f by YELLOW16:1;
then y is Element of oContMaps(Y,X) by Th2;
hence thesis;
end;
then F is Function of the carrier of oContMaps(Z, X),
the carrier of oContMaps(Y, X) by A8,FUNCT_2:4;
then reconsider F as map of oContMaps(Z, X), oContMaps(Y, X);
take F; let g be continuous map of Z,X;
g is Element of oContMaps(Z,X) by Th2;
hence F.g = f(#)g by A9 .= g*f by YELLOW16:1;
end;
end;
:: 4.2. LEMMA (i)
theorem Th7:
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace
holds oContMaps(X,Y) is directed-sups-inheriting
SubRelStr of (Omega Y)|^the carrier of X
proof let X be non empty TopSpace;
let Y be monotone-convergence T_0-TopSpace;
ContMaps(X,Omega Y) is directed-sups-inheriting
SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL25:43;
hence thesis by Def1;
end;
theorem Th8:
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace
holds oContMaps(X, Y) is up-complete
proof let X be non empty TopSpace;
let Y be monotone-convergence T_0-TopSpace;
A1: ContMaps(X, Omega Y) is directed-sups-inheriting
full SubRelStr of (Omega Y) |^ the carrier of X
by WAYBEL24:def 3,WAYBEL25:43;
oContMaps(X, Y) = ContMaps(X, Omega Y) by Def1;
hence thesis by A1,YELLOW16:5;
end;
theorem Th9:
for X,Y,Z being non empty TopSpace
for f being continuous map of Y,Z
holds oContMaps(X, f) is monotone
proof let X,Y,Z be non empty TopSpace;
let f be continuous map of Y,Z;
the TopStruct of Y = the TopStruct of Omega Y &
the TopStruct of Z = the TopStruct of Omega Z by WAYBEL25:def 2;
then reconsider f' = f as continuous map of Omega Y, Omega Z by YELLOW12:36;
set Xf = oContMaps(X, f);
let a,b be Element of oContMaps(X, Y);
reconsider g1 = a, g2 = b as continuous map of X, Omega Y by Th1;
assume a <= b;
then A1: g1 <= g2 by Th3;
g1 is continuous map of X,Y & g2 is continuous map of X,Y by Th2;
then A2: Xf.a = f'*g1 & Xf.b = f'*g2 by Def2;
reconsider fg1 = f'*g1, fg2 = f'*g2 as map of X, Omega Z;
now let x be set; assume x in the carrier of X;
then reconsider x' = x as Element of X;
ex a, b being Element of Omega Y
st a = g1.x' & b = g2.x' & a <= b by A1,YELLOW_2:def 1;
then (f'*g1).x' = f'.(g1.x') & (f'*g2).x' = f'.(g2.x') & g1.x' <= g2.x'
by FUNCT_2:21;
then (f'*g1).x' <= (f'*g2).x' by WAYBEL_1:def 2;
hence ex a,b being Element of Omega Z
st a = (f'*g1).x & b = (f'*g2).x & a <= b;
end;
then fg1 <= fg2 by YELLOW_2:def 1;
hence Xf.a <= Xf.b by A2,Th3;
end;
theorem
for X,Y being non empty TopSpace
for f being continuous map of Y,Y st f is idempotent
holds oContMaps(X, f) is idempotent
proof let X,Y be non empty TopSpace;
let f be continuous map of Y,Y such that
A1: f is idempotent;
set Xf = oContMaps(X, f);
now let g be Element of oContMaps(X, Y);
reconsider h = g as continuous map of X,Y by Th2;
thus (Xf*Xf).g = Xf.(Xf.g) by FUNCT_2:21 .= Xf.(f*h) by Def2
.= f*(f*h) by Def2 .= (f*f)*h by RELAT_1:55
.= f*h by A1,QUANTAL1:def 9 .= Xf.g by Def2;
end;
then Xf*Xf = Xf by YELLOW_2:9;
hence thesis by QUANTAL1:def 9;
end;
theorem Th11:
for X,Y,Z being non empty TopSpace
for f being continuous map of Y,Z
holds oContMaps(f, X) is monotone
proof let X,Y,Z be non empty TopSpace;
let f be continuous map of Y,Z;
the TopStruct of Y = the TopStruct of Omega Y &
the TopStruct of Z = the TopStruct of Omega Z by WAYBEL25:def 2;
then reconsider f' = f as continuous map of Omega Y, Omega Z by YELLOW12:36;
set Xf = oContMaps(f, X);
let a,b be Element of oContMaps(Z, X);
reconsider g1 = a, g2 = b as continuous map of Z, Omega X by Th1;
assume a <= b;
then A1: g1 <= g2 by Th3;
g1 is continuous map of Z,X & g2 is continuous map of Z,X by Th2;
then A2: Xf.a = g1*f' & Xf.b = g2*f' by Def3;
then reconsider fg1 = g1*f', fg2 = g2*f' as map of Y, Omega X by Th1;
now let x be set; assume x in the carrier of Y;
then reconsider x' = x as Element of Y;
(g1*f).x' = g1.(f.x') & (g2*f).x' = g2.(f.x') by FUNCT_2:21;
hence ex a, b being Element of Omega X
st a = (g1*f).x & b = (g2*f).x & a <= b by A1,YELLOW_2:def 1;
end;
then fg1 <= fg2 by YELLOW_2:def 1;
hence Xf.a <= Xf.b by A2,Th3;
end;
theorem Th12:
for X,Y being non empty TopSpace
for f being continuous map of Y,Y st f is idempotent
holds oContMaps(f, X) is idempotent
proof let X,Y be non empty TopSpace;
let f be continuous map of Y,Y such that
A1: f is idempotent;
set fX = oContMaps(f, X);
now let g be Element of oContMaps(Y, X);
reconsider h = g as continuous map of Y,X by Th2;
thus (fX*fX).g = fX.(fX.g) by FUNCT_2:21 .= fX.(h*f) by Def3
.= h*f*f by Def3 .= h*(f*f) by RELAT_1:55
.= h*f by A1,QUANTAL1:def 9 .= fX.g by Def3;
end;
then fX*fX = fX by YELLOW_2:9;
hence thesis by QUANTAL1:def 9;
end;
theorem Th13:
for X,Y,Z being non empty TopSpace
for f being continuous map of Y,Z
for x being Element of X, A being Subset of oContMaps(X, Y)
holds pi(oContMaps(X,f).:A, x) = f.:pi(A, x)
proof let X,Y,Z be non empty TopSpace;
let f be continuous map of Y,Z;
set Xf = oContMaps(X,f);
let x be Element of X, A be Subset of oContMaps(X, Y);
thus pi(Xf.:A,x) c= f.:pi(A,x)
proof let a be set; assume a in pi(Xf.:A,x);
then consider h being Function such that
A1: h in Xf.:A & a = h.x by CARD_3:def 6;
consider g being set such that
A2: g in the carrier of oContMaps(X,Y) & g in A & h = Xf.g
by A1,FUNCT_2:115;
g is Element of oContMaps(X,Y) by A2;
then reconsider g as continuous map of X,Y by Th2;
h = f*g by A2,Def2;
then a = f.(g.x) & g.x in pi(A,x) & the carrier of Z <> {}
by A1,A2,CARD_3:def 6,FUNCT_2:21;
hence thesis by FUNCT_2:43;
end;
let a be set; assume a in f.:pi(A,x);
then consider b being set such that
A3: b in the carrier of Y & b in pi(A,x) & a = f.b by FUNCT_2:115;
consider g being Function such that
A4: g in A & b = g.x by A3,CARD_3:def 6;
g is Element of oContMaps(X,Y) by A4;
then reconsider g as continuous map of X,Y by Th2;
A5: a = (f*g).x by A3,A4,FUNCT_2:21;
f*g = Xf.g & the carrier of oContMaps(X,Z) <> {} by Def2;
then f*g in Xf.:A by A4,FUNCT_2:43;
hence thesis by A5,CARD_3:def 6;
end;
:: 4.2. LEMMA (ii)
theorem Th14:
for X being non empty TopSpace
for Y,Z being monotone-convergence T_0-TopSpace
for f being continuous map of Y,Z
holds oContMaps(X, f) is directed-sups-preserving
proof let X be non empty TopSpace;
let Y,Z be monotone-convergence T_0-TopSpace;
A1: oContMaps(X, Z) is up-complete by Th8;
let f be continuous map of Y,Z;
the TopStruct of Y = the TopStruct of Omega Y &
the TopStruct of Z = the TopStruct of Omega Z by WAYBEL25:def 2;
then reconsider f' = f as continuous map of Omega Y, Omega Z by YELLOW12:36;
let A be Subset of oContMaps(X, Y); assume A is non empty directed;
then reconsider A' = A as non empty directed Subset of oContMaps(X, Y);
oContMaps(X,Y) = ContMaps(X, Omega Y) by Def1;
then reconsider XY = oContMaps(X, Y) as directed-sups-inheriting non empty
full SubRelStr of (Omega Y) |^ the carrier of X by Th7,WAYBEL24:def 3;
reconsider B = A' as non empty directed Subset of XY;
reconsider B' = B as non empty directed Subset of
(Omega Y) |^ the carrier of X by YELLOW_2:7;
A2: ex_sup_of B', (Omega Y) |^ the carrier of X by WAYBEL_0:75;
then A3: sup B' = sup A by WAYBEL_0:7;
set Xf = oContMaps(X, f);
Xf is monotone by Th9;
then reconsider fA' = Xf.:A' as
non empty directed Subset of oContMaps(X, Z) by YELLOW_2:17;
oContMaps(X,Z) = ContMaps(X, Omega Z) by Def1;
then reconsider XZ = oContMaps(X, Z) as directed-sups-inheriting non empty
full SubRelStr of (Omega Z) |^ the carrier of X by Th7,WAYBEL24:def 3;
reconsider fB = fA' as non empty directed Subset of XZ;
reconsider fB' = fB as non empty directed Subset of
(Omega Z) |^ the carrier of X by YELLOW_2:7;
ex_sup_of fB', (Omega Z) |^ the carrier of X by WAYBEL_0:75;
then A4: sup fB' = sup (oContMaps(X, f).:A) by WAYBEL_0:7;
assume ex_sup_of A, oContMaps(X, Y);
fA' is directed;
hence ex_sup_of oContMaps(X, f).:A, oContMaps(X, Z) by A1,WAYBEL_0:75;
reconsider sfA = sup (Xf.:A), XfsA = Xf.sup A as map of X, Omega Z by Th1;
set I = the carrier of X;
set J1 = I --> Omega Y;
set J2 = I --> Omega Z;
A5: (Omega Z) |^ I = I-POS_prod J2 by YELLOW_1:def 5;
then reconsider fB'' = fB' as non empty directed Subset of I-POS_prod J2;
A6: (Omega Y) |^ the carrier of X = I-POS_prod J1 by YELLOW_1:def 5;
then reconsider B'' = B' as non empty directed Subset of I-POS_prod J1;
reconsider sA = sup A as continuous map of X,Y by Th2;
now let x be Element of X;
J2.x = Omega Z & pi(fB'',x) is directed by FUNCOP_1:13,YELLOW16:37;
hence ex_sup_of pi(fB'',x), J2.x by WAYBEL_0:75;
end;
then A7: ex_sup_of fB'', I-POS_prod J2 by YELLOW16:33;
now let x be Element of X;
A8: (sup B'').x = sup pi(B'',x) by A2,A6,YELLOW16:35;
A9: J1.x = Omega Y & J2.x = Omega Z by FUNCOP_1:13;
then reconsider Bx = pi(B'',x) as directed non empty Subset of Omega Y by
YELLOW16:37;
A10: ex_sup_of Bx, Omega Y & f' preserves_sup_of Bx by WAYBEL_0:75,def 37;
A11: pi(fB'',x) = f'.:Bx by Th13;
thus sfA.x = sup pi(fB'',x) by A4,A5,A7,YELLOW16:35
.= f.sup Bx by A9,A10,A11,WAYBEL_0:def 31
.= (f*sA).x by A3,A6,A8,A9,FUNCT_2:21
.= XfsA.x by Def2;
end;
hence sup (oContMaps(X, f).:A) = oContMaps(X, f).sup A by YELLOW_2:9;
end;
theorem Th15:
for X,Y,Z being non empty TopSpace
for f being continuous map of Y,Z
for x being Element of Y, A being Subset of oContMaps(Z, X)
holds pi(oContMaps(f, X).:A, x) = pi(A, f.x)
proof let X,Y,Z be non empty TopSpace;
let f be continuous map of Y,Z;
set fX = oContMaps(f, X);
let x be Element of Y, A be Subset of oContMaps(Z, X);
thus pi(fX.:A,x) c= pi(A,f.x)
proof let a be set; assume a in pi(fX.:A,x);
then consider h being Function such that
A1: h in fX.:A & a = h.x by CARD_3:def 6;
consider g being set such that
A2: g in the carrier of oContMaps(Z,X) & g in A & h = fX.g
by A1,FUNCT_2:115;
g is Element of oContMaps(Z,X) by A2;
then reconsider g as continuous map of Z,X by Th2;
h = g*f by A2,Def3;
then a = g.(f.x) by A1,FUNCT_2:21;
hence thesis by A2,CARD_3:def 6;
end;
let a be set; assume a in pi(A,f.x);
then consider g being Function such that
A3: g in A & a = g.(f.x) by CARD_3:def 6;
g is Element of oContMaps(Z,X) by A3;
then reconsider g as continuous map of Z,X by Th2;
A4: a = (g*f).x by A3,FUNCT_2:21;
g*f = fX.g & the carrier of oContMaps(Y,X) <> {} by Def3;
then g*f in fX.:A by A3,FUNCT_2:43;
hence thesis by A4,CARD_3:def 6;
end;
theorem Th16:
for Y,Z being non empty TopSpace
for X being monotone-convergence T_0-TopSpace
for f being continuous map of Y,Z
holds oContMaps(f, X) is directed-sups-preserving
proof let Y,Z be non empty TopSpace;
let X be monotone-convergence T_0-TopSpace;
A1: oContMaps(Y, X) is up-complete by Th8;
let f be continuous map of Y,Z;
let A be Subset of oContMaps(Z, X); assume A is non empty directed;
then reconsider A' = A as non empty directed Subset of oContMaps(Z, X);
oContMaps(Z,X) = ContMaps(Z, Omega X) by Def1;
then reconsider ZX = oContMaps(Z, X) as directed-sups-inheriting non empty
full SubRelStr of (Omega X) |^ the carrier of Z by Th7,WAYBEL24:def 3;
reconsider B = A' as non empty directed Subset of ZX;
reconsider B' = B as non empty directed Subset of
(Omega X) |^ the carrier of Z by YELLOW_2:7;
A2: ex_sup_of B', (Omega X) |^ the carrier of Z by WAYBEL_0:75;
then A3: sup B' = sup A by WAYBEL_0:7;
set fX = oContMaps(f, X);
fX is monotone by Th11;
then reconsider fA' = fX.:A' as
non empty directed Subset of oContMaps(Y, X) by YELLOW_2:17;
oContMaps(Y,X) = ContMaps(Y, Omega X) by Def1;
then reconsider YX = oContMaps(Y, X) as directed-sups-inheriting non empty
full SubRelStr of (Omega X) |^ the carrier of Y by Th7,WAYBEL24:def 3;
reconsider fB = fA' as non empty directed Subset of YX;
reconsider fB' = fB as non empty directed Subset of
(Omega X) |^ the carrier of Y by YELLOW_2:7;
ex_sup_of fB', (Omega X) |^ the carrier of Y by WAYBEL_0:75;
then A4: sup fB' = sup (oContMaps(f, X).:A) by WAYBEL_0:7;
assume ex_sup_of A, oContMaps(Z, X);
fA' is directed;
hence ex_sup_of oContMaps(f, X).:A, oContMaps(Y, X) by A1,WAYBEL_0:75;
reconsider sfA = sup (fX.:A), XfsA = fX.sup A as map of Y, Omega X by Th1;
set I1 = the carrier of Z, I2 = the carrier of Y;
set J1 = I1 --> Omega X;
set J2 = I2 --> Omega X;
A5: (Omega X) |^ I2 = I2-POS_prod J2 by YELLOW_1:def 5;
then reconsider fB'' = fB' as non empty directed Subset of I2-POS_prod J2;
A6: (Omega X) |^ I1 = I1-POS_prod J1 by YELLOW_1:def 5;
then reconsider B'' = B' as non empty directed Subset of I1-POS_prod J1;
reconsider sA = sup A as continuous map of Z,X by Th2;
now let x be Element of Y;
J2.x = Omega X & pi(fB'',x) is directed by FUNCOP_1:13,YELLOW16:37;
hence ex_sup_of pi(fB'',x), J2.x by WAYBEL_0:75;
end;
then A7: ex_sup_of fB'', I2-POS_prod J2 by YELLOW16:33;
now let x be Element of Y;
A8: J1.(f.x) = Omega X & J2.x = Omega X by FUNCOP_1:13;
A9: pi(fB'',x) = pi(B'',f.x) by Th15;
thus sfA.x = sup pi(fB'',x) by A4,A5,A7,YELLOW16:35
.= (sup B'').(f.x) by A2,A6,A8,A9,YELLOW16:35
.= (sA*f).x by A3,A6,FUNCT_2:21
.= XfsA.x by Def3;
end;
hence sup (oContMaps(f, X).:A) = oContMaps(f, X).sup A by YELLOW_2:9;
end;
:: 4.3. LEMMA (i) genralized
theorem Th17:
for X,Z being non empty TopSpace
for Y being non empty SubSpace of Z
holds oContMaps(X, Y) is full SubRelStr of oContMaps(X, Z)
proof let X,Z be non empty TopSpace, Y be non empty SubSpace of Z;
set XY = oContMaps(X, Y), XZ = oContMaps(X, Z);
A1: [#]Y c= [#]Z by PRE_TOPC:def 9;
A2: [#]Y = the carrier of Y & [#]Z = the carrier of Z by PRE_TOPC:12;
A3: Omega Y is full SubRelStr of Omega Z by WAYBEL25:17;
XY is SubRelStr of XZ
proof
thus
A4: the carrier of XY c= the carrier of XZ
proof let x be set; assume x in the carrier of XY;
then x is Element of XY;
then reconsider f = x as continuous map of X, Y by Th2;
A5: dom f = the carrier of X & rng f c= the carrier of Y
by FUNCT_2:def 1;
rng f c= the carrier of Z by A1,A2,XBOOLE_1:1;
then f is Function of the carrier of X, the carrier of Z
by A5,FUNCT_2:4;
then x is continuous map of X,Z by TOPMETR:7;
then x is Element of XZ & XZ is non empty by Th2;
hence thesis;
end;
let x,y be set; assume
A6: [x,y] in the InternalRel of XY;
then A7: x in the carrier of XY & y in the carrier of XY by ZFMISC_1:106;
then reconsider x, y as Element of XY;
reconsider a = x, b = y as Element of XZ by A4,A7;
reconsider f = x, g = y as continuous map of X, Omega Y by Th1;
reconsider f' = a, g' = b as continuous map of X, Omega Z by Th1;
x <= y by A6,ORDERS_1:def 9;
then f <= g by Th3;
then f' <= g' by A3,YELLOW16:2;
then a <= b by Th3;
hence thesis by ORDERS_1:def 9;
end;
then reconsider XY as non empty SubRelStr of XZ;
A8: (the InternalRel of XZ)|_2 the carrier of XY =
(the InternalRel of XZ) /\ [:the carrier of XY, the carrier of XY:]
by WELLORD1:def 6;
the InternalRel of XY = ((the InternalRel of XZ)|_2 the carrier of XY)
qua set
proof
the InternalRel of XY c= the InternalRel of XZ by YELLOW_0:def 13;
hence the InternalRel of XY c= (the InternalRel of XZ)|_2
the carrier of XY
by A8,XBOOLE_1:19;
let x,y be set; assume
A9: [x,y] in (the InternalRel of XZ)|_2 the carrier of XY;
then [x,y] in
[:the carrier of XY, the carrier of XY:] by A8,XBOOLE_0:def 3;
then A10: x in the carrier of XY & y in the carrier of XY by ZFMISC_1:106;
then reconsider x,y as Element of XY;
the carrier of XY c= the carrier of XZ by YELLOW_0:def 13;
then reconsider a = x, b = y as Element of XZ by A10;
reconsider f = x, g = y as continuous map of X, Omega Y by Th1;
reconsider f' = a, g' = b as continuous map of X, Omega Z by Th1;
[a,b] in the InternalRel of XZ by A8,A9,XBOOLE_0:def 3;
then a <= b by ORDERS_1:def 9;
then f' <= g' by Th3;
then f <= g by A3,YELLOW16:3;
then x <= y by Th3;
hence thesis by ORDERS_1:def 9;
end;
hence thesis by YELLOW_0:def 14;
end;
theorem Th18:
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous map of Z,Y st f is_a_retraction
holds Omega Y is directed-sups-inheriting SubRelStr of Omega Z
proof
let Z be monotone-convergence T_0-TopSpace;
let Y be non empty SubSpace of Z;
reconsider OZ = Omega Z as non empty up-complete (non empty Poset);
reconsider OY = Omega Y as full non empty SubRelStr of Omega Z
by WAYBEL25:17;
let f be continuous map of Z,Y; assume
A1: f is_a_retraction;
A2: dom f = the carrier of Z & rng f c= the carrier of Y by FUNCT_2:def 1;
[#]Y c= [#]Z & [#]Y = the carrier of Y & [#]Z = the carrier of Z
by PRE_TOPC:12,def 9;
then rng f c= the carrier of Z by XBOOLE_1:1;
then f is Function of the carrier of Z, the carrier of Z
by A2,FUNCT_2:def 1,RELSET_1:11;
then A3: f is continuous map of Z,Z by TOPMETR:7;
the TopStruct of Omega Z = the TopStruct of Z by WAYBEL25:def 2;
then reconsider f' = f as continuous map of Omega Z, Omega Z
by A3,YELLOW12:36;
reconsider g = f' as map of OZ, OZ;
g is idempotent directed-sups-preserving by A1,YELLOW16:47;
then A4: Image g is directed-sups-inheriting by YELLOW16:6;
A5: rng f = the carrier of Y by A1,YELLOW16:46;
A6: the TopStruct of Omega Y = the TopStruct of Y &
the TopStruct of Omega Z = the TopStruct of Z by WAYBEL25:def 2;
A7: Image g = subrelstr rng g & rng g = the carrier of subrelstr rng g
by YELLOW_0:def 15,YELLOW_2:def 2;
the RelStr of OZ = the RelStr of Omega Z;
then OY is directed-sups-inheriting by A4,A5,A6,A7,WAYBEL21:22;
hence thesis;
end;
Lm1:
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous map of Z,Y st f is_a_retraction
holds Y is monotone-convergence
proof
let Z be monotone-convergence T_0-TopSpace;
let Y be non empty SubSpace of Z;
let f be continuous map of Z,Y; assume
f is_a_retraction;
then Y is_a_retract_of Z by BORSUK_1:def 20;
then Y is_Retract_of Z by YELLOW16:58;
hence thesis by WAYBEL25:36;
end;
theorem Th19:
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous map of Z,Y st f is_a_retraction
holds
oContMaps(X, f) is_a_retraction_of oContMaps(X, Z), oContMaps(X, Y)
proof let X be non empty TopSpace;
let Z be monotone-convergence T_0-TopSpace;
let Y be non empty SubSpace of Z;
set XY = oContMaps(X, Y), XZ = oContMaps(X, Z);
reconsider uXZ = XZ as up-complete (non empty Poset) by Th8;
reconsider sXY = XY as full non empty SubRelStr of uXZ by Th17;
let f be continuous map of Z,Y; assume
A1: f is_a_retraction;
set F = oContMaps(X, f);
reconsider Y' = Y as monotone-convergence T_0-TopSpace by A1,Lm1;
oContMaps(X,Y') is up-complete by Th8;
hence F is directed-sups-preserving map of XZ, XY by Th14;
id XY = id the carrier of XY by GRCAT_1:def 11;
then A2: dom id XY = the carrier of XY by RELAT_1:71;
A3: the carrier of sXY c= the carrier of uXZ by YELLOW_0:def 13;
then F|the carrier of XY is Function of the carrier of XY, the carrier of
XY
by FUNCT_2:38;
then A4: dom (F|the carrier of XY) = the carrier of XY by FUNCT_2:def 1;
now let x be set; assume
A5: x in the carrier of XY;
then reconsider a = x as Element of XZ by A3;
reconsider a as continuous map of X, Z by Th2;
x is Element of XY by A5;
then A6: rng f = the carrier of Y & x is map of X,Y by A1,Th2,YELLOW16:46;
then f is idempotent & rng a c= the carrier of Y & dom f = the carrier of
Z
by A1,FUNCT_2:def 1,RELSET_1:12,YELLOW16:47;
then f*a = a by A6,YELLOW16:4;
hence (id XY).x = f*a by A5,GRCAT_1:11
.= F.a by Def2
.= (F|the carrier of XY).x by A5,FUNCT_1:72;
end;
hence F|the carrier of XY = id XY by A2,A4,FUNCT_1:9;
oContMaps(X,Y) = ContMaps(X, Omega Y) by Def1;
then A7: oContMaps(X, Y') is directed-sups-inheriting full non empty
SubRelStr of (Omega Y)|^the carrier of X by Th7,WAYBEL24:def 3;
oContMaps(X,Z) = ContMaps(X, Omega Z) by Def1;
then A8: oContMaps(X, Z) is directed-sups-inheriting full non empty
SubRelStr of (Omega Z)|^the carrier of X by Th7,WAYBEL24:def 3;
Omega Y is directed-sups-inheriting full SubRelStr of Omega Z
by A1,Th18,WAYBEL25:17;
then (Omega Y)|^the carrier of X is directed-sups-inheriting full
SubRelStr of (Omega Z)|^the carrier of X by YELLOW16:41,44;
then oContMaps(X,Y) is directed-sups-inheriting full
SubRelStr of (Omega Z)|^the carrier of X by A7,YELLOW16:28,29;
hence oContMaps(X, Y) is directed-sups-inheriting full
SubRelStr of oContMaps(X, Z) by A8,Th17,YELLOW16:30;
end;
theorem Th20:
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
st Y is_a_retract_of Z
holds oContMaps(X, Y) is_a_retract_of oContMaps(X, Z)
proof let X be non empty TopSpace;
let Z be monotone-convergence T_0-TopSpace;
let Y be non empty SubSpace of Z;
given f being continuous map of Z,Y such that
A1: f is_a_retraction;
take oContMaps(X, f);
thus thesis by A1,Th19;
end;
theorem Th21:
for X,Y,Z being non empty TopSpace
for f being continuous map of Y,Z st f is_homeomorphism
holds oContMaps(X, f) is isomorphic
proof let X,Y,Z be non empty TopSpace;
let f be continuous map of Y,Z; assume
A1: f is_homeomorphism;
then reconsider g = f" as continuous map of Z,Y by TOPS_2:def 5;
A2: f is one-to-one & rng f = [#]Z & dom f = [#]Y by A1,TOPS_2:def 5;
set Xf = oContMaps(X,f), Xg = oContMaps(X,g);
set XY = oContMaps(X,Y), XZ = oContMaps(X,Z);
A3: Xf is monotone & Xg is monotone by Th9;
now let a be Element of XY;
reconsider h = a as continuous map of X,Y by Th2;
thus (Xg*Xf).a = Xg.(Xf.a) by FUNCT_2:21
.= Xg.(f*h) by Def2
.= g*(f*h) by Def2
.= g*f*h by RELAT_1:55
.= (id dom f)*h by A2,TOPS_2:65
.= (id the carrier of Y)*h by A2,PRE_TOPC:12
.= a by FUNCT_2:23
.= (id XY).a by GRCAT_1:11;
end;
then A4: Xg*Xf = id XY by YELLOW_2:9;
now let a be Element of XZ;
reconsider h = a as continuous map of X,Z by Th2;
thus (Xf*Xg).a = Xf.(Xg.a) by FUNCT_2:21
.= Xf.(g*h) by Def2
.= f*(g*h) by Def2
.= f*g*h by RELAT_1:55
.= (id rng f)*h by A2,TOPS_2:65
.= (id the carrier of Z)*h by A2,PRE_TOPC:12
.= a by FUNCT_2:23
.= (id XZ).a by GRCAT_1:11;
end;
then Xf*Xg = id XZ by YELLOW_2:9;
hence thesis by A3,A4,YELLOW16:17;
end;
theorem Th22:
for X,Y,Z being non empty TopSpace
st Y,Z are_homeomorphic
holds oContMaps(X, Y), oContMaps(X, Z) are_isomorphic
proof let X,Y,Z be non empty TopSpace;
given f being map of Y,Z such that
A1: f is_homeomorphism;
reconsider f as continuous map of Y,Z by A1,TOPS_2:def 5;
take oContMaps(X, f); thus thesis by A1,Th21;
end;
:: 4.3. LEMMA (ii)
theorem Th23:
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
st Y is_a_retract_of Z & oContMaps(X, Z) is complete continuous
holds oContMaps(X, Y) is complete continuous
proof let X be non empty TopSpace;
let Z be monotone-convergence T_0-TopSpace;
let Y be non empty SubSpace of Z;
assume Y is_a_retract_of Z;
then A1: oContMaps(X, Y) is_a_retract_of oContMaps(X,Z) by Th20;
assume oContMaps(X, Z) is complete continuous;
then oContMaps(X, Z) is complete continuous (non empty Poset);
hence oContMaps(X, Y) is complete continuous by A1,YELLOW16:23,24;
end;
theorem Th24:
for X being non empty TopSpace
for Y,Z being monotone-convergence T_0-TopSpace
st Y is_Retract_of Z & oContMaps(X, Z) is complete continuous
holds oContMaps(X, Y) is complete continuous
proof let X be non empty TopSpace;
let Y,Z be monotone-convergence T_0-TopSpace; assume
Y is_Retract_of Z;
then consider S being non empty SubSpace of Z such that
A1: S is_a_retract_of Z & S,Y are_homeomorphic by YELLOW16:59;
A2: oContMaps(X,S), oContMaps(X,Y) are_isomorphic by A1,Th22;
assume oContMaps(X, Z) is complete continuous;
then oContMaps(X,S) is complete continuous by A1,Th23;
hence thesis by A2,WAYBEL15:11,WAYBEL20:18;
end;
theorem Th25:
for Y being non trivial T_0-TopSpace
st not Y is_T1
holds Sierpinski_Space is_Retract_of Y
proof let Y be non trivial T_0-TopSpace;
given p,q being Point of Y such that
A1: p <> q and
A2: for W,V being Subset of Y st W is open & V is open &
p in W & not q in W & q in V holds p in V;
(ex V being Subset of Y st V is open & p in V & not q in V) or
(ex W being Subset of Y st W is open & not p in W & q in W)
by A1,TSP_1:def 3;
then consider V being Subset of Y such that
A3: V is open and
A4: p in V & not q in V or not p in V & q in V;
A5: the TopStruct of Omega Y = the TopStruct of Y by WAYBEL25:def 2;
then p is Element of Omega Y & q is Element of Omega Y;
then consider x,y being Element of Omega Y such that
A6: p in V & not q in V & x = q & y = p or
not p in V & q in V & x = p & y = q by A4;
reconsider V as open Subset of Omega Y by A3,A5,TOPS_3:76;
reconsider c = chi(V, the carrier of Y) as
continuous map of Y, Sierpinski_Space by A3,YELLOW16:48;
now let W be open Subset of Omega Y;
W is open Subset of Y by A5,TOPS_3:76;
hence x in W implies y in W by A2,A3,A6;
end;
then (0,1) --> (x,y) is continuous map of Sierpinski_Space, Omega Y
by YELLOW16:49;
then reconsider i = (0,1) --> (x,y) as continuous map of Sierpinski_Space, Y
by A5,YELLOW12:36;
c*i = id Sierpinski_Space by A5,A6,YELLOW16:50;
hence thesis by WAYBEL25:def 1;
end;
theorem Th26:
for X being non empty TopSpace
for Y being non trivial T_0-TopSpace
st oContMaps(X, Y) is with_suprema
holds not Y is_T1
proof let X be non empty TopSpace;
let Y be non trivial T_0-TopSpace;
consider a,b being Element of Y such that
A1: a <> b by REALSET1:def 20;
assume oContMaps(X, Y) is with_suprema;
then reconsider XY = oContMaps(X, Y) as sup-Semilattice;
reconsider f = X --> a, g = X --> b as continuous map of X, Y
by BORSUK_1:36;
reconsider ef = f, eg = g as Element of XY by Th2;
reconsider h = ef "\/" eg, f = ef, g = eg as
continuous map of X, Omega Y by Th1;
consider i being Element of X;
f = (the carrier of X) --> a & g = (the carrier of X) --> b
by BORSUK_1:def 3;
then A2: f.i = a & g.i = b by FUNCOP_1:13;
now assume not ex x,y being Element of Omega Y st x <= y & x <> y;
then A3: not (f.i <= h.i & f.i <> h.i) & not (g.i <= h.i & g.i <> h.i);
ef <= ef "\/" eg & eg <= ef "\/" eg by YELLOW_0:22;
then f <= h & g <= h by Th3;
then (ex x,y being Element of Omega Y st x = f.i & y = h.i & x <= y) &
(ex x,y being Element of Omega Y st x = g.i & y = h.i & x <= y)
by YELLOW_2:def 1;
hence contradiction by A1,A2,A3;
end;
then consider x,y being Element of Omega Y such that
A4: x <= y & x <> y;
A5: the TopStruct of Omega Y = the TopStruct of Y by WAYBEL25:def 2;
then reconsider p = x, q = y as Element of Y;
take p,q; thus p <> q by A4;
let W,V be Subset of Y; assume
W is open;
then reconsider W as open Subset of Omega Y by A5,TOPS_3:76;
W is upper;
hence thesis by A4,WAYBEL_0:def 20;
end;
definition
cluster Sierpinski_Space -> non trivial monotone-convergence;
coherence
proof
A1: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
0 in {0,1} & 1 in {0,1} & 0 <> 1 by TARSKI:def 2;
hence thesis by A1,REALSET1:def 20;
end;
end;
definition
cluster injective monotone-convergence non trivial T_0-TopSpace;
existence
proof take Sierpinski_Space; thus thesis;
end;
end;
:: 4.4. PROPOSITION
theorem Th27:
for X being non empty TopSpace
for Y being monotone-convergence non trivial T_0-TopSpace
st oContMaps(X, Y) is complete continuous
holds InclPoset the topology of X is continuous
proof let X be non empty TopSpace;
let Y be monotone-convergence non trivial T_0-TopSpace;
assume
A1: oContMaps(X, Y) is complete continuous;
then oContMaps(X, Y) is complete continuous (non empty Poset);
then not Y is_T1 by Th26;
then Sierpinski_Space is_Retract_of Y by Th25;
then A2: oContMaps(X, Sierpinski_Space) is complete continuous by A1,Th24;
InclPoset the topology of X, oContMaps(X, Sierpinski_Space)
are_isomorphic by Th6;
then oContMaps(X, Sierpinski_Space), InclPoset the topology of X
are_isomorphic by WAYBEL_1:7;
hence thesis by A2,WAYBEL15:11;
end;
theorem Th28:
for X being non empty TopSpace, x being Point of X
for Y being monotone-convergence T_0-TopSpace
ex F being directed-sups-preserving projection
map of oContMaps(X,Y), oContMaps(X,Y) st
(for f being continuous map of X,Y holds F.f = X --> (f.x)) &
ex h being continuous map of X,X st h = X --> x & F = oContMaps(h, Y)
proof let X be non empty TopSpace, x be Point of X;
let Y be monotone-convergence T_0-TopSpace;
set XY = oContMaps(X,Y);
reconsider f = X --> x as continuous map of X,X by BORSUK_1:36;
set F = oContMaps(f, Y);
A1: f = (the carrier of X) --> x by BORSUK_1:def 3;
dom f = the carrier of X by FUNCT_2:def 1;
then f*f = (the carrier of X) --> (f.x) by A1,FUNCOP_1:23
.= f by A1,FUNCOP_1:13;
then f is idempotent by QUANTAL1:def 9;
then F is directed-sups-preserving idempotent map of XY,XY by Th12,Th16;
then reconsider F as directed-sups-preserving projection map of XY,XY
by WAYBEL_1:def 13;
take F;
hereby let h be continuous map of X,Y;
A2: the carrier of X = dom h by FUNCT_2:def 1;
thus F.h = h*(X --> x) by Def3
.= h*((the carrier of X) --> x) by BORSUK_1:def 3
.= (the carrier of X) --> (h.x) by A2,FUNCOP_1:23
.= X --> (h.x) by BORSUK_1:def 3;
end;
thus thesis;
end;
:: 4.5. PROPOSITION
theorem Th29:
for X being non empty TopSpace, Y being monotone-convergence T_0-TopSpace
st oContMaps(X, Y) is complete continuous
holds Omega Y is complete continuous
proof let X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace
such that
A1: oContMaps(X, Y) is complete continuous;
consider b being Element of X;
consider F being directed-sups-preserving projection map of oContMaps(X,Y),
oContMaps(X,Y) such that
A2: for f being continuous map of X,Y holds F.f = X --> (f.b) and
ex h being continuous map of X,X st h = X --> b & F = oContMaps(h, Y)
by Th28;
oContMaps(X, Y) is complete continuous (non empty Poset) by A1;
then A3: Image F is complete continuous LATTICE by WAYBEL15:17,YELLOW_2:37;
oContMaps(X, Y) = ContMaps(X, Omega Y) by Def1;
then oContMaps(X, Y) is full SubRelStr of (Omega Y)|^the carrier of X
by WAYBEL24:def 3;
then reconsider imF = Image F as full non empty SubRelStr of
(Omega Y)|^the carrier of X by YELLOW16:28;
A4: the carrier of imF = rng F by YELLOW_2:11;
A5: dom F = the carrier of oContMaps(X,Y) by FUNCT_2:67;
A6: the TopStruct of Omega Y = the TopStruct of Y by WAYBEL25:def 2;
now let a be set;
hereby assume a is Element of imF;
then consider h being set such that
A7: h in dom F & a = F.h by A4,FUNCT_1:def 5;
h is Element of oContMaps(X,Y) by A7;
then reconsider h as continuous map of X,Y by Th2;
reconsider x = h.b as Element of Omega Y by A6;
a = X --> (h.b) by A2,A7
.= (the carrier of X) --> x by BORSUK_1:def 3;
hence ex x being Element of Omega Y st a = (the carrier of X) --> x;
end;
given x being Element of Omega Y such that
A8: a = (the carrier of X) --> x;
A9: a = X --> x by A8,BORSUK_1:def 3;
X --> x is continuous map of X, Omega Y by BORSUK_1:36;
then A10: a is Element of oContMaps(X,Y) by A9,Th1;
then reconsider h = a as continuous map of X,Y by Th2;
h.b = x & X --> (h.b) = (the carrier of X) --> (h.b)
by A8,BORSUK_1:def 3,FUNCOP_1:13;
then F.a = X --> x by A2,A8,A9;
then a in rng F by A5,A9,A10,FUNCT_1:def 5;
hence a is Element of imF by A4;
end;
then Omega Y, imF are_isomorphic by YELLOW16:52;
then imF, Omega Y are_isomorphic by WAYBEL_1:7;
hence thesis by A3,WAYBEL15:11,WAYBEL20:18;
end;
theorem Th30:
for X being non empty 1-sorted, I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for f being map of X, I-TOP_prod J
for i being Element of I
holds (commute f).i = proj(J,i)*f
proof let X be non empty 1-sorted, I be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let f be map of X, I-TOP_prod J;
A1: dom f = the carrier of X & rng f c= the carrier of I-TOP_prod J
by FUNCT_2:def 1;
A2: the carrier of I-TOP_prod J = product Carrier J by WAYBEL18:def 3;
A3: dom Carrier J = I by PBOOLE:def 3;
rng f c= Funcs(I, Union Carrier J)
proof let g be set; assume g in rng f;
then consider h being Function such that
A4: g = h & dom h = I &
for x being set st x in I holds h.x in (Carrier J).x
by A2,A3,CARD_3:def 5;
rng h c= Union Carrier J
proof let y be set; assume y in rng h;
then consider x being set such that
A5: x in dom h & y = h.x by FUNCT_1:def 5;
h.x in (Carrier J).x & dom Carrier J = I by A4,A5,PBOOLE:def 3;
hence thesis by A4,A5,CARD_5:10;
end;
hence thesis by A4,FUNCT_2:def 2;
end;
then A6: f in Funcs(the carrier of X, Funcs(I, Union Carrier J))
by A1,FUNCT_2:def 2;
then commute f in Funcs(I, Funcs(the carrier of X, Union Carrier J))
by PRALG_2:4;
then A7: ex g being Function st commute f = g & dom g = I &
rng g c= Funcs(the carrier of X, Union Carrier J) by FUNCT_2:def 2;
let i be Element of I;
(commute f).i in rng commute f by A7,FUNCT_1:def 5;
then consider g being Function such that
A8: (commute f).i = g and
A9: dom g = the carrier of X and
rng g c= Union Carrier J by A7,FUNCT_2:def 2;
A10: dom (proj(J, i)*f) = the carrier of X by FUNCT_2:def 1;
now let x be set; assume x in the carrier of X;
then reconsider a = x as Element of X;
consider h being Function such that
A11: f.a = h & dom h = I &
for x being set st x in I holds h.x in (Carrier J).x
by A2,A3,CARD_3:def 5;
A12: dom proj(Carrier J, i) = product Carrier J by PRALG_3:def 2;
(proj(J,i)*f).a = proj(J,i).(f.a) by FUNCT_2:21
.= (proj (Carrier J, i)).(f.a) by WAYBEL18:def 4
.= h.i by A2,A11,A12,PRALG_3:def 2;
hence g.x = (proj(J,i)*f).x by A6,A8,A11,PRALG_2:5;
end;
hence (commute f).i = proj(J,i)*f by A8,A9,A10,FUNCT_1:9;
end;
theorem Th31:
for S being 1-sorted, M being set holds
Carrier (M --> S) = M --> the carrier of S
proof let S be 1-sorted, M be set;
now let i be set; assume i in M;
then (M --> S).i = S & (M --> the carrier of S).i = the carrier of S &
ex R being 1-sorted st R = (M --> S).i &
(Carrier (M --> S)).i = the carrier of R
by FUNCOP_1:13,PRALG_1:def 13;
hence (Carrier (M --> S)).i = (M --> the carrier of S).i;
end;
hence thesis by PBOOLE:3;
end;
theorem Th32:
for X,Y being non empty TopSpace, M being non empty set
for f being continuous map of X, M-TOP_prod (M --> Y)
holds commute f is Function of M, the carrier of oContMaps(X, Y)
proof let X,Y be non empty TopSpace, M be non empty set;
let f be continuous map of X, M-TOP_prod (M --> Y);
A1: dom f = the carrier of X & rng f c= the carrier of M-TOP_prod (M --> Y)
by FUNCT_2:def 1;
rng f c= Funcs(M, the carrier of Y)
proof let g be set; assume
A2: g in rng f;
the carrier of M-TOP_prod (M --> Y)
= product Carrier (M --> Y) by WAYBEL18:def 3
.= product (M --> the carrier of Y) by Th31;
then g in product (M --> the carrier of Y) & dom (M --> the carrier of
Y) = M
by A2,FUNCOP_1:19;
then consider h being Function such that
A3: g = h & dom h = M &
for x being set st x in M holds h.x in (M --> the carrier of Y).x
by CARD_3:def 5;
rng h c= the carrier of Y
proof let y be set; assume y in rng h;
then consider x being set such that
A4: x in dom h & y = h.x by FUNCT_1:def 5;
(M --> the carrier of Y).x = the carrier of Y
by A3,A4,FUNCOP_1:13;
hence y in the carrier of Y by A3,A4;
end;
hence thesis by A3,FUNCT_2:def 2;
end;
then f in Funcs(the carrier of X, Funcs(M, the carrier of Y))
by A1,FUNCT_2:def 2;
then A5: commute f in Funcs(M, Funcs(the carrier of X, the carrier of Y))
by PRALG_2:4;
then A6: ex g being Function st commute f = g & dom g = M &
rng g c= Funcs(the carrier of X, the carrier of Y) by FUNCT_2:def 2;
rng commute f c= the carrier of oContMaps(X, Y)
proof let g be set; assume g in rng commute f;
then consider i being set such that
A7: i in dom commute f & g = (commute f).i by FUNCT_1:def 5;
ex h being Function st commute f = h & dom h = M &
rng h c= Funcs(the carrier of X, the carrier of Y)
by A5,FUNCT_2:def 2;
then reconsider i as Element of M by A7;
g = proj(M --> Y, i)*f & (M --> Y).i = Y by A7,Th30,FUNCOP_1:13;
then g is continuous map of X,Y by WAYBEL18:7;
then g is Element of oContMaps(X,Y) by Th2;
hence thesis;
end;
hence thesis by A6,FUNCT_2:4;
end;
theorem Th33:
for X,Y being non empty TopSpace holds
the carrier of oContMaps(X, Y) c= Funcs(the carrier of X, the carrier of Y)
proof let X,Y be non empty TopSpace;
oContMaps(X, Y) = ContMaps(X, Omega Y) by Def1;
then oContMaps(X, Y) is SubRelStr of (Omega Y)|^the carrier of X
by WAYBEL24:def 3;
then the carrier of oContMaps(X, Y) c=
the carrier of (Omega Y)|^the carrier of X by YELLOW_0:def 13;
then the carrier of oContMaps(X, Y) c=
Funcs(the carrier of X, the carrier of Omega Y) &
the TopStruct of Y = the TopStruct of Omega Y
by WAYBEL25:def 2,YELLOW_1:28;
hence thesis;
end;
theorem Th34:
for X,Y being non empty TopSpace, M being non empty set
for f being Function of M, the carrier of oContMaps(X, Y)
holds commute f is continuous map of X, M-TOP_prod (M --> Y)
proof let X,Y be non empty TopSpace, M be non empty set;
let f be Function of M, the carrier of oContMaps(X, Y);
A1: dom f = M & rng f c= the carrier of oContMaps(X, Y) by FUNCT_2:def 1;
the carrier of oContMaps(X, Y) c=
Funcs(the carrier of X, the carrier of Y) by Th33;
then rng f c= Funcs(the carrier of X, the carrier of Y) by XBOOLE_1:1;
then A2: f in Funcs(M, Funcs(the carrier of X, the carrier of Y))
by A1,FUNCT_2:def 2;
then commute f in Funcs(the carrier of X, Funcs(M, the carrier of Y))
by PRALG_2:4;
then A3: ex g being Function st commute f = g & dom g = the carrier of X &
rng g c= Funcs(M, the carrier of Y) by FUNCT_2:def 2;
A4: the carrier of M-TOP_prod (M --> Y)
= product Carrier (M --> Y) by WAYBEL18:def 3;
A5: Carrier (M --> Y) = M --> the carrier of Y by Th31;
then the carrier of M-TOP_prod (M --> Y) = Funcs(M, the carrier of Y)
by A4,CARD_3:20;
then commute f is Function of the carrier of X,
the carrier of M-TOP_prod (M --> Y) by A3,FUNCT_2:4;
then reconsider g = commute f as map of X, M-TOP_prod (M --> Y);
reconsider B = product_prebasis (M --> Y) as
prebasis of M-TOP_prod (M --> Y) by WAYBEL18:def 3;
now let P be Subset of M-TOP_prod (M --> Y); assume P in B;
then consider i being set, T being TopStruct, V being Subset of T such
that
A6: i in M & V is open & T = (M --> Y).i and
A7: P = product ((Carrier (M --> Y)) +* (i,V)) by WAYBEL18:def 2;
A8: T = Y by A6,FUNCOP_1:13;
reconsider i as Element of M by A6;
set FP = (Carrier (M --> Y)) +* (i,V);
A9: dom FP = dom Carrier (M --> Y) by FUNCT_7:32;
A10: dom Carrier (M --> Y) = M by A5,FUNCOP_1:19;
then A11: FP.i = V by FUNCT_7:33;
reconsider fi = f.i as continuous map of X, Y by Th2;
now let x be set;
hereby assume A12: x in g"P;
then x in the carrier of X & g.x in P by FUNCT_2:46;
then consider gx being Function such that
A13: g.x = gx & dom gx = dom FP &
for z being set st z in dom FP holds gx.z in FP.z
by A7,CARD_3:def 5;
reconsider Q = fi"V as Subset of X;
take Q;
thus Q is open by A6,A8,TOPS_2:55;
thus Q c= g"P
proof let a be set; assume A14: a in Q;
then A15: a in the carrier of X & fi.a in V by FUNCT_2:46;
g.a in rng g by A3,A14,FUNCT_1:def 5;
then consider ga being Function such that
A16: g.a = ga & dom ga = M & rng ga c= the carrier of Y
by A3,FUNCT_2:def 2;
now let z be set; assume
A17: z in M;
then z <> i & (M --> the carrier of Y).z = the carrier of Y or
z = i by FUNCOP_1:13;
then z <> i & ga.z in rng ga & FP.z = the carrier of Y or
z = i by A5,A16,A17,FUNCT_1:def 5,FUNCT_7:34;
hence ga.z in FP.z by A2,A11,A15,A16,PRALG_2:5;
end;
then ga in P by A7,A9,A10,A16,CARD_3:18;
hence thesis by A14,A16,FUNCT_2:46;
end;
A18: gx.i in V by A9,A10,A11,A13;
gx.i = fi.x by A2,A12,A13,PRALG_2:5;
hence x in Q by A12,A18,FUNCT_2:46;
end;
thus (ex Q being Subset of X st Q is open & Q c= g"P & x in Q)
implies x in g"P;
end;
hence g"P is open by TOPS_1:57;
end;
hence thesis by YELLOW_9:36;
end;
theorem Th35:
for X being non empty TopSpace, M being non empty set
ex F being map of oContMaps(X, M-TOP_prod (M --> Sierpinski_Space)),
M-POS_prod (M --> oContMaps(X, Sierpinski_Space))
st F is isomorphic &
for f being continuous map of X, M-TOP_prod (M --> Sierpinski_Space)
holds F.f = commute f
proof let X be non empty TopSpace, M be non empty set;
set S = Sierpinski_Space, S'M = M-TOP_prod (M --> S);
set X__S'M = oContMaps(X, S'M), X_S = oContMaps(X, S);
set X_S'_M = M-POS_prod (M --> X_S);
deffunc F(Element of X__S'M) = commute $1;
consider F being ManySortedSet of the carrier of X__S'M such that
A1: for f being Element of X__S'M holds
F.f = F(f) from LambdaDMS;
A2: dom F = the carrier of X__S'M by PBOOLE:def 3;
rng F c= the carrier of X_S'_M
proof let g be set; assume g in rng F;
then consider f being set such that
A3: f in dom F & g = F.f by FUNCT_1:def 5;
f is Element of X__S'M by A2,A3;
then reconsider f as continuous map of X, S'M by Th2;
g = commute f by A1,A2,A3;
then reconsider g as Function of M, the carrier of X_S by Th32;
dom g = M & rng g c= the carrier of X_S by FUNCT_2:def 1;
then g in Funcs(M, the carrier of X_S) by FUNCT_2:def 2;
then g in the carrier of X_S|^M by YELLOW_1:28;
hence thesis by YELLOW_1:def 5;
end;
then F is Function of the carrier of X__S'M, the carrier of X_S'_M
by A2,FUNCT_2:4;
then reconsider F as map of X__S'M, X_S'_M;
take F;
deffunc F(Element of X_S'_M) = commute $1;
consider G being ManySortedSet of the carrier of X_S'_M such that
A4: for f being Element of X_S'_M holds
G.f = F(f) from LambdaDMS;
A5: dom G = the carrier of X_S'_M by PBOOLE:def 3;
rng G c= the carrier of X__S'M
proof let g be set; assume g in rng G;
then consider f being set such that
A6: f in dom G & g = G.f by FUNCT_1:def 5;
f in the carrier of X_S|^M by A5,A6,YELLOW_1:def 5;
then f in Funcs(M, the carrier of X_S) by YELLOW_1:28;
then consider f' being Function such that
A7: f = f' & dom f' = M & rng f' c= the carrier of X_S by FUNCT_2:def 2;
f' is Function of M, the carrier of X_S &
g = commute f' by A4,A5,A6,A7,FUNCT_2:4;
then g is continuous map of X, S'M by Th34;
then g is Element of X__S'M by Th2;
hence thesis;
end;
then G is Function of the carrier of X_S'_M, the carrier of X__S'M
by A5,FUNCT_2:4;
then reconsider G as map of X_S'_M, X__S'M;
A8: the carrier of X__S'M c= Funcs(the carrier of X, the carrier of S'M)
by Th33;
A9: the carrier of S'M = product Carrier (M --> S) by WAYBEL18:def 3
.= product (M --> the carrier of S) by Th31
.= Funcs(M, the carrier of S) by CARD_3:20;
A10: the carrier of X_S'_M = the carrier of X_S|^M by YELLOW_1:def 5
.= Funcs(M, the carrier of X_S) by YELLOW_1:28;
the carrier of X_S c= Funcs(the carrier of X, the carrier of S)
by Th33;
then A11: the carrier of X_S'_M c=
Funcs(M, Funcs(the carrier of X, the carrier of S)) by A10,FUNCT_5:63;
A12: the RelStr of Omega S'M = M-POS_prod(M --> Omega S) by WAYBEL25:14;
A13: F is monotone
proof let a, b be Element of X__S'M such that
A14: a <= b;
reconsider f = a, g = b as continuous map of X, Omega S'M by Th1;
reconsider f' = a, g' = b as continuous map of X, S'M by Th2;
now let i be Element of M;
A15: (M --> X_S).i = X_S by FUNCOP_1:13;
then reconsider Fai = (F.a).i, Fbi = (F.b).i
as continuous map of X, Omega S by Th1;
now let j be set; assume j in the carrier of X;
then reconsider x = j as Element of X;
reconsider fx = f.x, gx = g.x
as Element of M-POS_prod(M --> Omega S) by A12;
a in the carrier of X__S'M & b in the carrier of X__S'M;
then F.a = commute f & F.b = commute g &
a in Funcs(the carrier of X, Funcs(M, the carrier of S)) &
b in Funcs(the carrier of X, Funcs(M, the carrier of S))
by A1,A8,A9;
then A16: Fai.x = (f'.x).i & Fbi.x = (g'.x).i by PRALG_2:5;
f <= g by A14,Th3;
then ex a, b being Element of Omega S'M st a = f.x & b = g.x & a <=
b
by YELLOW_2:def 1;
then fx <= gx by A12,YELLOW_0:1;
then fx.i <= gx.i & (M --> Omega S).i = Omega S
by FUNCOP_1:13,WAYBEL_3:28;
hence ex a, b being Element of Omega S
st a = Fai.j & b = Fbi.j & a <= b by A16;
end;
then Fai <= Fbi by YELLOW_2:def 1;
hence (F.a).i <= (F.b).i by A15,Th3;
end;
hence thesis by WAYBEL_3:28;
end;
A17: G is monotone
proof let a,b be Element of X_S'_M such that
A18: a <= b;
reconsider f = G.a, g = G.b as continuous map of X, Omega S'M by Th1;
now let i be set; assume i in the carrier of X;
then reconsider x = i as Element of X;
reconsider fx = f.x, gx = g.x as Element of M-POS_prod(M --> Omega S)
by A12;
now let j be Element of M;
A19: (M --> X_S).j = X_S by FUNCOP_1:13;
then reconsider aj = a.j, bj = b.j as
continuous map of X, Omega S by Th1;
a in the carrier of X_S'_M & b in the carrier of X_S'_M;
then G.a = commute a & G.b = commute b &
a in Funcs(M, Funcs(the carrier of X, the carrier of S)) &
b in Funcs(M, Funcs(the carrier of X, the carrier of S))
by A4,A11;
then A20: fx.j = aj.x & gx.j = bj.x by PRALG_2:5;
a.j <= b.j by A18,WAYBEL_3:28;
then aj <= bj by A19,Th3;
then (M --> Omega S).j = Omega S &
ex a, b being Element of Omega S
st a = aj.x & b = bj.x & a <= b by FUNCOP_1:13,YELLOW_2:def 1;
hence fx.j <= gx.j by A20;
end;
then fx <= gx by WAYBEL_3:28;
then f.x <= g.x by A12,YELLOW_0:1;
hence ex a,b being Element of Omega S'M st a = f.i & b = g.i & a <= b;
end;
then f <= g by YELLOW_2:def 1;
hence thesis by Th3;
end;
now let a be Element of X_S'_M;
A21: a in Funcs(M, the carrier of X_S) by A10;
the carrier of X_S c= Funcs(the carrier of X, the carrier of S)
by Th33;
then Funcs(M, the carrier of X_S) c=
Funcs(M, Funcs(the carrier of X, the carrier of S)) by FUNCT_5:63;
then A22: commute commute a = a by A21,PRALG_2:6;
thus (F*G).a = F.(G.a) by FUNCT_2:21 .= commute (G.a) by A1
.= a by A4,A22 .= (id X_S'_M).a by GRCAT_1:11;
end;
then A23: F*G = id X_S'_M by YELLOW_2:9;
now let a be Element of X__S'M;
a in the carrier of X__S'M;
then A24: commute commute a = a by A8,A9,PRALG_2:6;
thus (G*F).a = G.(F.a) by FUNCT_2:21 .= commute (F.a) by A4
.= a by A1,A24 .= (id X__S'M).a by GRCAT_1:11;
end;
then G*F = id X__S'M by YELLOW_2:9;
hence F is isomorphic by A13,A17,A23,YELLOW16:17;
let f be continuous map of X, M-TOP_prod (M --> Sierpinski_Space);
f is Element of X__S'M by Th2;
hence thesis by A1;
end;
theorem Th36:
for X being non empty TopSpace, M being non empty set
holds
oContMaps(X, M-TOP_prod (M --> Sierpinski_Space)),
M-POS_prod (M --> oContMaps(X, Sierpinski_Space)) are_isomorphic
proof let X be non empty TopSpace, M be non empty set;
consider F being map of oContMaps(X, M-TOP_prod (M --> Sierpinski_Space)),
M-POS_prod (M --> oContMaps(X, Sierpinski_Space)) such that
A1: F is isomorphic and
for f being continuous map of X, M-TOP_prod (M --> Sierpinski_Space)
holds F.f = commute f by Th35;
take F; thus thesis by A1;
end;
:: 4.6. PROPOSITION
theorem Th37:
for X being non empty TopSpace st InclPoset the topology of X is continuous
for Y being injective T_0-TopSpace
holds
oContMaps(X, Y) is complete continuous
proof let X be non empty TopSpace such that
A1: InclPoset the topology of X is continuous;
let Y be injective T_0-TopSpace;
consider M being non empty set such that
A2: Y is_Retract_of M-TOP_prod (M --> Sierpinski_Space) by WAYBEL18:20;
oContMaps(X, M-TOP_prod (M --> Sierpinski_Space)),
M-POS_prod (M --> oContMaps(X, Sierpinski_Space)) are_isomorphic
by Th36;
then A3: M-POS_prod (M --> oContMaps(X, Sierpinski_Space)),
oContMaps(X, M-TOP_prod (M --> Sierpinski_Space)) are_isomorphic
by WAYBEL_1:7;
InclPoset the topology of X, oContMaps(X, Sierpinski_Space)
are_isomorphic by Th6;
then reconsider XS = oContMaps(X, Sierpinski_Space) as
complete continuous (non empty Poset) by A1,WAYBEL15:11,WAYBEL20:18;
for i be Element of M holds
(M --> Sierpinski_Space).i is injective by FUNCOP_1:13;
then reconsider MS = M-TOP_prod (M --> Sierpinski_Space) as
injective T_0-TopSpace by WAYBEL18:8;
for i be Element of M holds
(M --> XS).i is complete continuous LATTICE by FUNCOP_1:13;
then M-POS_prod (M --> XS) is complete continuous
by WAYBEL20:34;
then oContMaps(X, MS) is complete continuous
by A3,WAYBEL15:11,WAYBEL20:18;
hence thesis by A2,Th24;
end;
definition
cluster non trivial complete Scott TopLattice;
existence
proof set L = BoolePoset 1;
A1: BoolePoset 1 = InclPoset bool 1 by YELLOW_1:4;
consider T being Scott TopAugmentation of L;
take T; the RelStr of T = the RelStr of L by YELLOW_9:def 4;
then 0 <> 1 & the carrier of T = bool 1 & 0 in {0,1} & 1 in {0,1}
by A1,TARSKI:def 2,YELLOW_1:1;
hence thesis by REALSET1:def 20,YELLOW14:1;
end;
end;
:: 4.7. THEOREM p.129.
theorem
for X being non empty TopSpace
for L being non trivial complete Scott TopLattice
holds
oContMaps(X, L) is complete continuous
iff
InclPoset the topology of X is continuous & L is continuous
proof let X be non empty TopSpace;
let L be non trivial complete Scott TopLattice;
A1: L is monotone-convergence by WAYBEL25:29;
Omega L = the TopRelStr of L by WAYBEL25:15;
then A2: the RelStr of Omega L = the RelStr of L;
A3: L is Scott TopAugmentation of L by YELLOW_9:44;
hereby assume
A4: oContMaps(X, L) is complete continuous;
hence InclPoset the topology of X is continuous by A1,Th27;
Omega L is continuous by A3,A4,Th29;
hence L is continuous by A2,YELLOW12:15;
end;
L is continuous implies L is injective by A3,WAYBEL25:12;
hence thesis by Th37;
end;
definition
let f be Function;
cluster Union disjoin f -> Relation-like;
coherence
proof
for x being set st x in Union disjoin f ex y,z being set st x = [y,z]
by CARD_3:32;
hence thesis by RELAT_1:def 1;
end;
end;
definition
let f be Function;
func *graph f -> Relation equals:
Def4: (Union disjoin f)~; :: card_3
correctness;
end;
reserve x,y for set, f for Function;
theorem Th39:
[x,y] in *graph f iff x in dom f & y in f.x
proof
A1: *graph f = (Union disjoin f)~ by Def4;
A2: [y,x]`1 = y & [y,x]`2 = x by MCART_1:7;
[x,y] in *graph f iff [y,x] in Union disjoin f by A1,RELAT_1:def 7;
hence thesis by A2,CARD_3:33;
end;
theorem Th40:
for X being finite set holds proj1 X is finite & proj2 X is finite
proof let X be finite set;
deffunc F(set) = $1`1;
consider f being Function such that
A1: dom f = X & for x being set st x in X holds f.x = F(x) from Lambda;
A2: proj1 X c= rng f
proof let x be set; assume x in proj1 X;
then consider y being set such that
A3: [x,y] in X by FUNCT_5:def 1;
[x,y]`1 = x by MCART_1:7;
then f.([x,y]) = x by A1,A3;
hence thesis by A1,A3,FUNCT_1:def 5;
end;
rng f is finite by A1,FINSET_1:26;
hence proj1 X is finite by A2,FINSET_1:13;
deffunc F(set) = $1`2;
consider f being Function such that
A4: dom f = X & for x being set st x in X holds f.x = F(x) from Lambda;
A5: proj2 X c= rng f
proof let x be set; assume x in proj2 X;
then consider y being set such that
A6: [y,x] in X by FUNCT_5:def 2;
[y,x]`2 = x by MCART_1:7;
then f.([y,x]) = x by A4,A6;
hence thesis by A4,A6,FUNCT_1:def 5;
end;
rng f is finite by A4,FINSET_1:26;
hence proj2 X is finite by A5,FINSET_1:13;
end;
:: 4.8. LEMMA p.130.
theorem Th41:
for X,Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for f being map of X, S
st *graph f is open Subset of [:X,Y:]
holds f is continuous
proof let X,Y be non empty TopSpace;
let S be Scott TopAugmentation of InclPoset the topology of Y;
let f be map of X, S; assume
*graph f is open Subset of [:X,Y:];
then consider AA being Subset-Family of [:X,Y:] such that
A1: *graph f = union AA and
A2: for e being set st e in AA
ex X1 being Subset of X, Y1 being Subset of Y st
e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:45;
A3: the carrier of InclPoset the topology of Y = the topology of Y
by YELLOW_1:1;
A4: the RelStr of S = the RelStr of InclPoset the topology of Y
by YELLOW_9:def 4;
A5: dom f = the carrier of X by FUNCT_2:def 1;
now let P be Subset of S; assume
A6: P is open;
now let x be set;
hereby assume A7: x in f"P; then
A8: x in the carrier of X & f.x in P by FUNCT_2:46;
reconsider y = x as Element of X by A7;
f.y in the topology of Y by A3,A4;
then reconsider W = f.y as open Subset of Y
by PRE_TOPC:def 5;
defpred P[set,set] means
x in $2`1 & $1 in $2`2 & [:$2`1,$2`2:] c= *graph f;
A9: now let e be set; assume e in f.x;
then [x,e] in *graph f by A5,A7,Th39;
then consider V being set such that
A10: [x,e] in V & V in AA by A1,TARSKI:def 4;
consider A being Subset of X, B being Subset of Y such that
A11: V = [:A,B:] & A is open & B is open by A2,A10;
reconsider u = [A,B] as set;
take u;
A in the topology of X & B in
the topology of Y by A11,PRE_TOPC:def 5;
hence u in [:the topology of X, the topology of Y:] by ZFMISC_1:106;
A = u`1 & B = u`2 by MCART_1:7;
hence P[e,u] by A1,A10,A11,ZFMISC_1:92,106;
end;
consider g being Function such that
A12: dom g = f.x & rng g c= [:the topology of X, the topology of Y:] and
A13: for a being set st a in f.x holds P[a,g.a]
from NonUniqBoundFuncEx(A9);
A14: proj1 rng g c= the topology of X by A12,FUNCT_5:13;
A15: proj2 rng g c= the topology of Y by A12,FUNCT_5:13;
A16: proj2 rng g c= bool (f.x)
proof let z be set; assume z in proj2 rng g;
then consider z1 being set such that
A17: [z1,z] in rng g by FUNCT_5:def 2;
consider a being set such that
A18: a in dom g & [z1,z] = g.a by A17,FUNCT_1:def 5;
[z1,z]`1 = z1 & [z1,z]`2 = z by MCART_1:7;
then A19: x in z1 & [:z1,z:] c= *graph f by A12,A13,A18;
z c= f.x
proof let a be set; assume a in z;
then [x,a] in [:z1,z:] by A19,ZFMISC_1:106;
hence thesis by A19,Th39;
end;
hence thesis;
end;
set J = {union A where A is Subset of proj2 rng g: A is finite};
consider A0 being empty Subset of proj2 rng g;
A20: A0 in J by ZFMISC_1:2;
J c= the topology of Y
proof let x be set; assume x in J;
then consider A being Subset of proj2 rng g such that
A21: x = union A & A is finite;
A22: A c= the topology of Y by A15,XBOOLE_1:1;
then A is Subset of bool the carrier of Y by XBOOLE_1:1;
then A is Subset-Family of Y by SETFAM_1:def 7;
hence thesis by A21,A22,PRE_TOPC:def 1;
end;
then reconsider J as non empty Subset of
InclPoset the topology of Y by A3,A20;
J is directed
proof let a,b be Element of InclPoset the topology of Y;
assume a in J;
then consider A being Subset of proj2 rng g such that
A23: a = union A & A is finite;
assume b in J;
then consider B being Subset of proj2 rng g such that
A24: b = union B & B is finite;
take ab = a"\/"b;
reconsider AB = A \/ B as finite Subset of proj2 rng g
by A23,A24,FINSET_1:14;
A25: union AB = a \/ b & a \/
b = ab by A23,A24,WAYBEL14:18,ZFMISC_1:96;
hence ab in J;
a c= ab & b c= ab by A25,XBOOLE_1:7;
hence thesis by YELLOW_1:3;
end;
then reconsider J' = J as non empty directed Subset of S
by A4,WAYBEL_0:3;
union J = f.y
proof
thus union J c= f.y
proof let a be set; assume a in union J;
then consider u being set such that
A26: a in u & u in J by TARSKI:def 4;
consider A being Subset of proj2 rng g such that
A27: u = union A & A is finite by A26;
A c= bool (f.y) by A16,XBOOLE_1:1;
then u c= union bool (f.y) by A27,ZFMISC_1:95;
then u c= f.y by ZFMISC_1:99;
hence thesis by A26;
end;
let a be set; assume a in f.y;
then A28: g.a in rng g & a in (g.a)`2 by A12,A13,FUNCT_1:def 5;
then g.a = [(g.a)`1, (g.a)`2] by A12,MCART_1:23;
then (g.a)`2 in proj2 rng g by A28,FUNCT_5:def 2;
then reconsider A = {(g.a)`2} as Subset of proj2 rng g by ZFMISC_1:
37;
union A = (g.a)`2 by ZFMISC_1:31;
then (g.a)`2 in J;
hence thesis by A28,TARSKI:def 4;
end;
then sup J = f.y & ex_sup_of J,S by YELLOW_0:17,YELLOW_1:22;
then sup J' = f.y & P is inaccessible
by A4,A6,WAYBEL11:def 4,YELLOW_0:26;
then J meets P by A8,WAYBEL11:def 1;
then consider a being set such that
A29: a in J & a in P by XBOOLE_0:3;
reconsider a as Element of S by A29;
consider A being Subset of proj2 rng g such that
A30: a = union A and
A31: A is finite by A29;
defpred P[set,set] means
ex c1 being set st [c1,$1] = g.$2 & x in c1 & $2 in $1 &
$2 in f.x & [:c1,$1:] c= *graph f;
A32: now let c be set; assume c in A;
then consider c1 being set such that
A33: [c1,c] in rng g by FUNCT_5:def 2;
consider a being set such that
A34: a in dom g & [c1,c] = g.a by A33,FUNCT_1:def 5;
take a; thus a in W by A12,A34;
[c1,c]`1 = c1 & [c1,c]`2 = c by MCART_1:7;
then x in c1 & a in c & [:c1,c:] c= *graph f by A12,A13,A34;
hence P[c,a] by A12,A34;
end;
consider hh being Function such that
A35: dom hh = A & rng hh c= W and
A36: for c being set st c in A holds P[c,hh.c]
from NonUniqBoundFuncEx(A32);
set B = proj1 (g.:rng hh);
g.:rng hh c= rng g by RELAT_1:144;
then B c= proj1 rng g by FUNCT_5:5;
then A37: B c= the topology of X by A14,XBOOLE_1:1;
then B c= bool the carrier of X by XBOOLE_1:1;
then reconsider B as Subset-Family of X by SETFAM_1:def
7;
reconsider B as Subset-Family of X;
reconsider Q = Intersect B as Subset of X;
take Q;
rng hh is finite by A31,A35,FINSET_1:26;
then g.:rng hh is finite by FINSET_1:17;
then B is finite by Th40;
then Q in FinMeetCl the topology of X by A37,CANTOR_1:def 4;
then Q in the topology of X by CANTOR_1:5;
hence Q is open by PRE_TOPC:def 5;
thus Q c= f"P
proof let z be set; assume
A38: z in Q;
then reconsider zz = z as Element of X;
reconsider fz = f.zz, aa = a as Element of
InclPoset the topology of Y by A4;
a c= f.zz
proof let p be set; assume p in a;
then consider q being set such that
A39: p in q & q in A by A30,TARSKI:def 4;
consider q1 being set such that
A40: [q1,q] = g.(hh.q) & x in q1 & hh.q in q & hh.q in f.x &
[:q1,q:] c= *graph f by A36,A39;
hh.q in rng hh by A35,A39,FUNCT_1:def 5;
then [q1,q] in g.:rng hh by A12,A40,FUNCT_1:def 12;
then q1 in B by FUNCT_5:def 1;
then zz in q1 by A38,CANTOR_1:10;
then [zz,p] in [:q1,q:] by A39,ZFMISC_1:106;
hence p in f.zz by A40,Th39;
end;
then aa <= fz by YELLOW_1:3;
then a <= f.zz & P is upper by A4,A6,WAYBEL11:def 4,YELLOW_0:1;
then f.zz in P by A29,WAYBEL_0:def 20;
hence thesis by FUNCT_2:46;
end;
now let c1 be set; assume c1 in B;
then consider c being set such that
A41: [c1,c] in g.:rng hh by FUNCT_5:def 1;
consider b being set such that
A42: b in dom g & b in rng hh & [c1,c] = g.b by A41,FUNCT_1:def 12;
consider c' being set such that
A43: c' in dom hh & b = hh.c' by A42,FUNCT_1:def 5;
consider c'1 being set such that
A44: [c'1,c'] = g.(hh.c') & x in c'1 & hh.c' in c' & hh.c' in f.x &
[:c'1,c':] c= *graph f by A35,A36,A43;
thus x in c1 by A42,A43,A44,ZFMISC_1:33;
end;
hence x in Q by A7,CANTOR_1:10;
end;
assume ex Q being Subset of X st Q is open & Q c= f"P & x in Q;
hence x in f"P;
end;
hence f"P is open by TOPS_1:57;
end;
hence thesis by TOPS_2:55;
end;
definition
let W be Relation, X be set;
func (W,X)*graph -> Function means:
Def5:
dom it = X & for x st x in X holds it.x = W.:{x};
existence
proof deffunc F(set) = W.:{$1};
thus ex f being Function st dom f = X & for x st x in X holds f.x = F(x)
from Lambda;
end;
correctness
proof let f,g be Function such that
A1: dom f = X and
A2: for x st x in X holds f.x = W.:{x} and
A3: dom g = X and
A4: for x st x in X holds g.x = W.:{x};
now let x; assume
A5: x in X;
hence f.x = W.:{x} by A2 .= g.x by A4,A5;
end;
hence thesis by A1,A3,FUNCT_1:9;
end;
end;
theorem Th42:
for W being Relation, X being set st dom W c= X
holds *graph((W,X)*graph) = W
proof let W be Relation, X be set such that
A1: dom W c= X;
A2: dom ((W,X)*graph) = X by Def5;
now let x,y be set;
hereby assume [x,y] in *graph((W,X)*graph);
then x in X & y in ((W,X)*graph).x by A2,Th39;
then y in W.:{x} by Def5;
then consider z being set such that
A3: [z,y] in W & z in {x} by RELAT_1:def 13;
thus [x,y] in W by A3,TARSKI:def 1;
end;
assume
A4: [x,y] in W;
then A5: x in {x} & x in dom W by RELAT_1:def 4,TARSKI:def 1;
then y in W.:{x} & x in X by A1,A4,RELAT_1:def 13;
then y in ((W,X)*graph).x by Def5;
hence [x,y] in *graph((W,X)*graph) by A1,A2,A5,Th39;
end;
hence thesis by RELAT_1:def 2;
end;
definition
let X, Y be TopSpace;
cluster -> Relation-like Subset of [:X,Y:];
coherence
proof let r be Subset of [:X,Y:];
r is Subset of [:the carrier of X, the carrier of Y:]
by BORSUK_1:def 5;
hence thesis;
end;
cluster -> Relation-like Element of the topology of [:X,Y:];
coherence
proof let r be Element of the topology of [:X,Y:];
r is Subset of [:the carrier of X, the carrier of Y:] by BORSUK_1:def 5;
hence thesis;
end;
end;
theorem Th43:
for X,Y being non empty TopSpace
for W being open Subset of [:X,Y:]
for x being Point of X
holds W.:{x} is open Subset of Y
proof let X,Y be non empty TopSpace, W be open Subset of [:X,Y:];
let x be Point of X;
the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:]
by BORSUK_1:def 5;
then reconsider W as Relation of the carrier of X, the carrier of Y
by RELSET_1:def 1;
reconsider A = W.:{x} as Subset of Y;
now let y;
hereby assume y in A;
then consider z being set such that
A1: [z,y] in W & z in {x} by RELAT_1:def 13;
consider AA being Subset-Family of [:X,Y:] such that
A2: W = union AA and
A3: for e being set st e in AA
ex X1 being Subset of X,
Y1 being Subset of Y st
e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:45;
z = x by A1,TARSKI:def 1;
then consider e being set such that
A4: [x,y] in e & e in AA by A1,A2,TARSKI:def 4;
consider X1 being Subset of X, Y1 being Subset of Y such that
A5: e = [:X1,Y1:] & X1 is open & Y1 is open by A3,A4;
A6: x in X1 by A4,A5,ZFMISC_1:106;
take Y1; thus Y1 is open by A5;
thus Y1 c= A
proof let z be set; assume z in Y1;
then [x,z] in e by A5,A6,ZFMISC_1:106;
then [x,z] in W & x in {x} by A2,A4,TARSKI:def 1,def 4;
hence thesis by RELAT_1:def 13;
end;
thus y in Y1 by A4,A5,ZFMISC_1:106;
end;
thus (ex Q being Subset of Y st Q is open & Q c= A & y in Q)
implies y in A;
end;
hence thesis by TOPS_1:57;
end;
:: 4.9. PROPOSITION a) p.130.
theorem Th44:
for X,Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for W being open Subset of [:X,Y:]
holds (W, the carrier of X)*graph is continuous map of X, S
proof let X,Y be non empty TopSpace;
let S be Scott TopAugmentation of InclPoset the topology of Y;
let W be open Subset of [:X,Y:];
set f = (W, the carrier of X)*graph;
the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:]
by BORSUK_1:def 5;
then reconsider W as Relation of the carrier of X, the carrier of Y
by RELSET_1:def 1;
A1: dom W c= the carrier of X;
A2: dom f = the carrier of X by Def5;
A3: the carrier of InclPoset the topology of Y = the topology of Y
by YELLOW_1:1;
A4: the RelStr of S = the RelStr of InclPoset the topology of Y
by YELLOW_9:def 4;
rng f c= the carrier of S
proof let y; assume y in rng f;
then consider x such that
A5: x in dom f & y = f.x by FUNCT_1:def 5;
reconsider x as Element of X by A2,A5;
y = W.:{x} by A5,Def5;
then y is open Subset of Y by Th43;
hence thesis by A3,A4,PRE_TOPC:def 5;
end;
then f is Function of the carrier of X, the carrier of S by A2,FUNCT_2:4;
then reconsider f as map of X,S;
*graph f = W by A1,Th42;
hence thesis by Th41;
end;
:: 4.9. PROPOSITION b) p.130.
theorem Th45:
for X,Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for W1, W2 being open Subset of [:X,Y:] st W1 c= W2
for f1, f2 being Element of oContMaps(X, S)
st f1 = (W1, the carrier of X)*graph & f2 = (W2, the carrier of X)*graph
holds f1 <= f2
proof let X,Y be non empty TopSpace;
let S be Scott TopAugmentation of InclPoset the topology of Y;
let W1,W2 be open Subset of [:X,Y:] such that
A1: W1 c= W2;
let f1,f2 be Element of oContMaps(X, S) such that
A2: f1 = (W1, the carrier of X)*graph & f2 = (W2, the carrier of X)*graph;
A3: the RelStr of S = the RelStr of InclPoset the topology of Y
by YELLOW_9:def 4;
S is TopAugmentation of S by YELLOW_9:44;
then A4: the RelStr of S = the RelStr of Omega S by WAYBEL25:16;
reconsider g1 = f1, g2 = f2 as continuous map of X, Omega S by Th1;
now let j be set; assume j in the carrier of X;
then reconsider x = j as Element of X;
take a = g1.x, b = g2.x;
thus a = g1.j & b = g2.j;
reconsider g1x = g1.x, g2x = g2.x as
Element of InclPoset the topology of Y by A3,A4;
g1.x = W1.:{x} & g2.x = W2.:{x} by A2,Def5;
then g1.x c= g2.x by A1,RELAT_1:157;
then g1x <= g2x by YELLOW_1:3;
hence a <= b by A3,A4,YELLOW_0:1;
end;
then g1 <= g2 by YELLOW_2:def 1;
hence thesis by Th3;
end;
:: 4.9. PROPOSITION p.130.
theorem
for X,Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
ex F being map of InclPoset the topology of [:X, Y:], oContMaps(X, S) st
F is monotone &
for W being open Subset of [:X,Y:] holds F.W = (W, the carrier of X)*graph
proof let X, Y be non empty TopSpace;
let S be Scott TopAugmentation of InclPoset the topology of Y;
deffunc F(Element of the topology of [:X,Y:])
= ($1, the carrier of X)*graph;
consider F being ManySortedSet of the topology of [:X,Y:] such that
A1: for R being Element of the topology of [:X,Y:]
holds F.R = F(R) from LambdaDMS;
A2: the carrier of InclPoset the topology of [:X,Y:] = the topology of [:X,Y:]
by YELLOW_1:1;
A3: dom F = the topology of [:X,Y:] by PBOOLE:def 3;
rng F c= the carrier of oContMaps(X, S)
proof let y be set; assume y in rng F;
then consider x such that
A4: x in dom F & y = F.x by FUNCT_1:def 5;
reconsider x as Element of the topology of [:X,Y:] by A4,PBOOLE:def 3;
y = (x, the carrier of X)*graph & x is open Subset of [:X,Y:]
by A1,A4,PRE_TOPC:def 5;
then y is continuous map of X,S by Th44;
then y is Element of oContMaps(X, S) by Th2;
hence thesis;
end;
then F is Function of the topology of [:X,Y:], the carrier of oContMaps(X,
S)
by A3,FUNCT_2:4;
then reconsider F as map of InclPoset the topology of [:X, Y:], oContMaps(X,
S)
by A2;
take F;
thus F is monotone
proof let x,y be Element of InclPoset the topology of [:X,Y:];
x in the topology of [:X,Y:] & y in the topology of [:X,Y:] by A2;
then reconsider W1 = x, W2 = y as open Subset of [:X,Y:]
by PRE_TOPC:def 5;
assume x <= y;
then W1 c= W2 & F.x = (W1, the carrier of X)*graph &
F.y = (W2, the carrier of X)*graph by A1,A2,YELLOW_1:3;
hence thesis by Th45;
end;
let W be open Subset of [:X,Y:];
W in the topology of [:X,Y:] by PRE_TOPC:def 5;
hence F.W = (W, the carrier of X)*graph by A1;
end;