:: Continuous Lattices between T$_0$ Spaces
:: by Grzegorz Bancerek
::
:: Received September 24, 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 YELLOW_1, PBOOLE, CARD_3, WAYBEL18, WAYBEL_3, XBOOLE_0, PRE_TOPC,
STRUCT_0, ORDERS_2, WAYBEL24, WAYBEL25, RELAT_2, MONOID_0, SUBSET_1,
ORDINAL2, FUNCT_1, XXREAL_0, CAT_1, YELLOW_0, NEWTON, TARSKI, YELLOW_9,
WAYBEL11, ZFMISC_1, CARD_1, RCOMP_1, FUNCT_3, RELAT_1, WELLORD1,
VALUED_1, T_0TOPSP, WAYBEL_0, SEQM_3, BINOP_1, FUNCOP_1, BORSUK_1,
GROUP_6, YELLOW16, TOPS_2, REWRITE1, LATTICE3, EQREL_1, FUNCTOR0,
WAYBEL_1, FUNCT_6, RLVECT_2, FUNCT_2, CANTOR_1, FUNCT_4, WAYBEL_9,
MCART_1, FINSET_1, SETFAM_1, WAYBEL26;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1,
MCART_1, FINSET_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, TOPS_2,
FUNCT_3, FUNCT_4, ORDINAL1, NUMBERS, SETFAM_1, FUNCT_2, FUNCOP_1,
STRUCT_0, CARD_3, FUNCT_6, MONOID_0, PRALG_1, FUNCT_7, WELLORD1,
ORDERS_2, LATTICE3, PRE_TOPC, CANTOR_1, 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 TOLER_1, FUNCT_7, TOPS_2, BORSUK_1, T_0TOPSP, CANTOR_1, MONOID_0,
QUANTAL1, ORDERS_3, PRALG_3, WAYBEL_1, WAYBEL11, YELLOW_9, WAYBEL18,
WAYBEL24, WAYBEL25, YELLOW16, XTUPLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, STRUCT_0,
PRE_TOPC, BORSUK_1, LATTICE3, YELLOW_0, TSP_1, MONOID_0, WAYBEL_0,
YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3, YELLOW_6, WAYBEL10,
WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL24, YELLOW14, WAYBEL25, YELLOW16,
FUNCT_1, XTUPLE_0;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, RELAT_1, YELLOW_0, BORSUK_1, WAYBEL_0, WAYBEL_1, T_0TOPSP,
YELLOW16, URYSOHN1, XBOOLE_0;
equalities RELAT_1, YELLOW_2, STRUCT_0;
expansions TARSKI, RELAT_1, BORSUK_1, WAYBEL_0, YELLOW_2, STRUCT_0;
theorems YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, PRE_TOPC, BORSUK_1,
ORDERS_2, 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,
QUANTAL1, CANTOR_1, FUNCT_7, YELLOW_9, WAYBEL18, WAYBEL20, MCART_1,
YELLOW14, WAYBEL11, FINSET_1, WAYBEL15, PRALG_1, YELLOW16, WAYBEL14,
FUNCT_5, CARD_5, SETFAM_1, XBOOLE_0, XBOOLE_1, FUNCT_6, STRUCT_0,
PARTFUN1, XTUPLE_0;
schemes FUNCT_1, PBOOLE;
begin
notation
let I be set;
let J be RelStr-yielding ManySortedSet of I;
synonym I-POS_prod J for product J;
end;
notation
let I be set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
synonym I-TOP_prod J for product J;
end;
:: 4.1. DEFINITION (a)
definition
let X,Y be non empty TopSpace;
func oContMaps(X, Y) -> non empty strict RelStr equals
ContMaps(X, Omega Y);
coherence;
end;
registration
let X,Y be non empty TopSpace;
cluster oContMaps(X, Y) -> reflexive transitive constituted-Functions;
coherence;
end;
registration
let X be non empty TopSpace;
let Y be non empty T_0 TopSpace;
cluster oContMaps(X, Y) -> antisymmetric;
coherence;
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 Function of X, Omega Y
proof
let X,Y be non empty TopSpace;
let a be set;
hereby
assume a is Element of oContMaps(X,Y);
then ex f being Function of X, Omega Y st a = f & f is continuous by
WAYBEL24:def 3;
hence a is continuous Function of X, Omega Y;
end;
assume a is continuous Function of X, Omega Y;
hence thesis by WAYBEL24:def 3;
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 Function 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 & the TopStruct of X = the
TopStruct of X by WAYBEL25:def 2;
hereby
assume a is Element of oContMaps(X,Y);
then a is continuous Function of X, Omega Y by Th1;
hence a is continuous Function of X, Y by A1,YELLOW12:36;
end;
assume a is continuous Function of X, Y;
then a is continuous Function of X, Omega Y by A1,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 Function 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);
A1: 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:58;
A2: a <= b iff x <= y by A1,YELLOW_0:59,60;
let f,g be Function of X, Omega Y;
assume a = f & b = g;
hence thesis by A2,WAYBEL10:11;
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; :: redefines pi (CARD_3, definition)
coherence
proof
set XY = oContMaps(X, Y);
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 reconsider A as Subset of (Omega Y)|^the carrier of X by XBOOLE_1:1;
pi(A,x) is Subset of Omega Y;
hence thesis;
end;
end;
registration
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 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 reconsider A as non empty Subset of (Omega Y)|^the carrier of X by
XBOOLE_1:1;
pi(A,x) <> {};
hence thesis;
end;
end;
theorem Th4:
Omega Sierpinski_Space is TopAugmentation of BoolePoset{0}
proof
set S = the strict Scott TopAugmentation of BoolePoset{0};
A1: the RelStr of S = BoolePoset{0} by YELLOW_9:def 4;
BoolePoset{0} = InclPoset bool {0} by YELLOW_1:4;
then
A2: the carrier of BoolePoset{0} = {0,1} by YELLOW14:1,YELLOW_1:1;
the carrier of Sierpinski_Space = {0,1} & the topology of S = the
topology of Sierpinski_Space by WAYBEL18:12,def 9;
then Omega Sierpinski_Space = Omega S by A2,A1,WAYBEL25:13
.= S by WAYBEL25:15;
hence thesis;
end;
theorem Th5:
for X being non empty TopSpace ex f being Function 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
FUNCT_1:sch 5;
A3: rng f c= the carrier of oContMaps(X, Sierpinski_Space)
proof
let x be object;
assume x in rng f;
then consider a being object such that
A4: a in dom f and
A5: x = f.a by FUNCT_1:def 3;
reconsider a as Subset of X by A1,A4;
a is open by A1,A4,PRE_TOPC:def 2;
then
chi(a, the carrier of X) is continuous Function of X, Sierpinski_Space
by YELLOW16:46;
then x is continuous Function of X, Sierpinski_Space by A1,A2,A4,A5;
then x is Element of oContMaps(X, Sierpinski_Space) by Th2;
hence thesis;
end;
set S = InclPoset the topology of X;
A6: the carrier of InclPoset the topology of X = the topology of X by
YELLOW_1:1;
then reconsider f as Function of InclPoset the topology of X, oContMaps(X,
Sierpinski_Space) by A1,A3,FUNCT_2:2;
A7: now
let x,y be Element of S;
x in the topology of X & y in the topology of X by A6;
then reconsider V = x, W = y as open Subset of X by PRE_TOPC:def 2;
set cx = chi(V, the carrier of X), cy = chi(W, the carrier of X);
A8: f.x = cx & f.y = cy by A2,A6;
cx is continuous Function of X, Sierpinski_Space by YELLOW16:46;
then
A9: cx is Element of oContMaps(X,Sierpinski_Space) by Th2;
cy is continuous Function of X, Sierpinski_Space by YELLOW16:46;
then cy is Element of oContMaps(X,Sierpinski_Space) by Th2;
then reconsider
cx, cy as continuous Function of X, Omega Sierpinski_Space by A9,Th1;
x <= y iff V c= W by YELLOW_1:3;
then x <= y iff cx <= cy by Th4,YELLOW16:49;
hence x <= y iff f.x <= f.y by A8,Th3;
end;
set T = oContMaps(X, Sierpinski_Space);
A10: rng f = the carrier of T
proof
the topology of Sierpinski_Space = {{}, {1}, {0,1}} by WAYBEL18:def 9;
then {1} in the topology of Sierpinski_Space by ENUMSET1:def 1;
then reconsider V = {1} as open Subset of Sierpinski_Space by
PRE_TOPC:def 2;
thus rng f c= the carrier of T;
let t be object;
assume t in the carrier of T;
then reconsider g = t as continuous Function of X, Sierpinski_Space by Th2;
[#]Sierpinski_Space <> {};
then
A11: g"V is open by TOPS_2:43;
then reconsider c = chi(g"V, the carrier of X) as Function of X,
Sierpinski_Space by YELLOW16:46;
now
let x be Element of X;
x in g"V or not x in g"V;
then
A12: g.x in V & c.x = 1 or not g.x in V & c.x = 0 by FUNCT_2:38,FUNCT_3:def 3;
the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
then g.x = 0 or g.x = 1 by TARSKI:def 2;
hence g.x = c.x by A12,TARSKI:def 1;
end;
then
A13: g = c by FUNCT_2:63;
A14: g"V in the topology of X by A11,PRE_TOPC:def 2;
then f.(g"V) = chi(g"V, the carrier of X) by A2;
hence thesis by A1,A14,A13,FUNCT_1:def 3;
end;
take f;
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 A6;
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,A6;
hence thesis by FUNCT_3:38;
end;
hence f is isomorphic by A10,A7,WAYBEL_0:66;
let V be open Subset of X;
V in the topology of X by PRE_TOPC:def 2;
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 Function 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 Function of Y,Z;
func oContMaps(X, f) -> Function of oContMaps(X, Y), oContMaps(X, Z) means
:
Def2: for g being continuous Function of X,Y holds it.g = f*g;
uniqueness
proof
let G1,G2 be Function of oContMaps(X, Y), oContMaps(X, Z) such that
A1: for g being continuous Function of X,Y holds G1.g = f*g and
A2: for g being continuous Function 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 Function of X, Y by Th2;
thus G1.x = f*g by A1
.= G2.x by A2;
end;
hence thesis by FUNCT_2:63;
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 FUNCT_1:sch 5;
rng F c= the carrier of oContMaps(X, Z)
proof
let y be object;
assume y in rng F;
then consider x being object such that
A5: x in dom F and
A6: y = F.x by FUNCT_1:def 3;
reconsider g = x as continuous Function of X,Y by A3,A5,Th2;
y = g(#)f by A3,A4,A5,A6
.= f*g;
then y is Element of oContMaps(X,Z) by Th2;
hence thesis;
end;
then reconsider F as Function of oContMaps(X, Y), oContMaps(X, Z) by A3,
FUNCT_2:2;
take F;
let g be continuous Function of X,Y;
g is Element of oContMaps(X,Y) by Th2;
hence F.g = g(#)f by A4
.= f*g;
end;
func oContMaps(f, X) -> Function of oContMaps(Z, X), oContMaps(Y, X) means
:
Def3: for g being continuous Function of Z, X holds it.g = g*f;
uniqueness
proof
let G1,G2 be Function of oContMaps(Z, X), oContMaps(Y, X) such that
A7: for g being continuous Function of Z,X holds G1.g = g*f and
A8: for g being continuous Function 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 Function of Z, X by Th2;
thus G1.x = g*f by A7
.= G2.x by A8;
end;
hence thesis by FUNCT_2:63;
end;
existence
proof
deffunc F(set) = f(#)$1;
consider F being Function such that
A9: dom F = the carrier of oContMaps(Z, X) and
A10: for x being set st x in the carrier of oContMaps(Z, X) holds F.x
= F(x) from FUNCT_1:sch 5;
rng F c= the carrier of oContMaps(Y, X)
proof
let y be object;
assume y in rng F;
then consider x being object such that
A11: x in dom F and
A12: y = F.x by FUNCT_1:def 3;
reconsider g = x as continuous Function of Z,X by A9,A11,Th2;
y = f(#)g by A9,A10,A11,A12
.= g*f;
then y is Element of oContMaps(Y,X) by Th2;
hence thesis;
end;
then reconsider F as Function of oContMaps(Z, X), oContMaps(Y, X) by A9,
FUNCT_2:2;
take F;
let g be continuous Function of Z,X;
g is Element of oContMaps(Z,X) by Th2;
hence F.g = f(#)g by A10
.= g*f;
end;
end;
theorem Th7:
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;
ContMaps(X, Omega Y) is directed-sups-inheriting full SubRelStr of (
Omega Y) |^ the carrier of X by WAYBEL24:def 3,WAYBEL25:43;
hence thesis by YELLOW16:5;
end;
theorem Th8:
for X,Y,Z being non empty TopSpace for f being continuous
Function of Y,Z holds oContMaps(X, f) is monotone
proof
let X,Y,Z be non empty TopSpace;
let f be continuous Function of Y,Z;
let a,b be Element of oContMaps(X, Y);
the TopStruct of Y = the TopStruct of Omega Y & the TopStruct of Z = the
TopStruct of Omega Z by WAYBEL25:def 2;
then reconsider f9 = f as continuous Function of Omega Y, Omega Z by
YELLOW12:36;
reconsider g1 = a, g2 = b as continuous Function of X, Omega Y by Th1;
set Xf = oContMaps(X, f);
reconsider fg1 = f9*g1, fg2 = f9*g2 as Function of X, Omega Z;
g2 is continuous Function of X,Y by Th2;
then
A1: Xf.b = f9*g2 by Def2;
assume a <= b;
then
A2: g1 <= g2 by Th3;
now
let x be set;
assume x in the carrier of X;
then reconsider x9 = x as Element of X;
A3: (f9*g2).x9 = f9.(g2.x9) by FUNCT_2:15;
( ex a, b being Element of Omega Y st a = g1.x9 & b = g2.x9 & a <= b)
& (f9*g1) .x9 = f9.(g1.x9) by A2,FUNCT_2:15;
then (f9*g1).x9 <= (f9*g2).x9 by A3,WAYBEL_1:def 2;
hence ex a,b being Element of Omega Z st a = (f9*g1).x & b = (f9*g2).x & a
<= b;
end;
then
A4: fg1 <= fg2;
g1 is continuous Function of X,Y by Th2;
then Xf.a = f9*g1 by Def2;
hence Xf.a <= Xf.b by A1,A4,Th3;
end;
theorem
for X,Y being non empty TopSpace for f being continuous Function 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 Function 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 Function of X,Y by Th2;
thus (Xf*Xf).g = Xf.(Xf.g) by FUNCT_2:15
.= Xf.(f*h) by Def2
.= f*(f*h) by Def2
.= (f*f)*h by RELAT_1:36
.= f*h by A1,QUANTAL1:def 9
.= Xf.g by Def2;
end;
then Xf*Xf = Xf by FUNCT_2:63;
hence thesis by QUANTAL1:def 9;
end;
theorem Th10:
for X,Y,Z being non empty TopSpace for f being continuous
Function of Y,Z holds oContMaps(f, X) is monotone
proof
let X,Y,Z be non empty TopSpace;
let f be continuous Function of Y,Z;
let a,b be Element of oContMaps(Z, X);
reconsider g1 = a, g2 = b as continuous Function of Z, Omega X by Th1;
set Xf = oContMaps(f, X);
the TopStruct of Y = the TopStruct of Omega Y & the TopStruct of Z = the
TopStruct of Omega Z by WAYBEL25:def 2;
then reconsider f9 = f as continuous Function of Omega Y, Omega Z by
YELLOW12:36;
g2 is continuous Function of Z,X by Th2;
then
A1: Xf.b = g2 qua Function*f9 by Def3;
g1 is continuous Function of Z,X by Th2;
then
A2: Xf.a = g1 qua Function*f9 by Def3;
then reconsider
fg1 = g1 qua Function*f9, fg2 = g2 qua Function*f9 as Function of
Y, Omega X by A1,Th1;
assume a <= b;
then
A3: g1 <= g2 by Th3;
now
let x be set;
assume x in the carrier of Y;
then reconsider x9 = x as Element of Y;
(g1*f).x9 = g1.(f.x9) & (g2*f).x9 = g2.(f.x9) by FUNCT_2:15;
hence ex a, b being Element of Omega X st a = (g1*f).x & b = (g2*f).x & a
<= b by A3;
end;
then fg1 <= fg2;
hence Xf.a <= Xf.b by A2,A1,Th3;
end;
theorem Th11:
for X,Y being non empty TopSpace for f being continuous Function
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 Function 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 Function of Y,X by Th2;
thus (fX*fX).g = fX.(fX.g) by FUNCT_2:15
.= fX.(h*f) by Def3
.= h*f*f by Def3
.= h*(f*f) by RELAT_1:36
.= h*f by A1,QUANTAL1:def 9
.= fX.g by Def3;
end;
then fX*fX = fX by FUNCT_2:63;
hence thesis by QUANTAL1:def 9;
end;
theorem Th12:
for X,Y,Z being non empty TopSpace for f being continuous
Function 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 Function 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 object;
assume a in pi(Xf.:A,x);
then consider h being Function such that
A1: h in Xf.:A and
A2: a = h.x by CARD_3:def 6;
consider g being object such that
A3: g in the carrier of oContMaps(X,Y) and
A4: g in A and
A5: h = Xf.g by A1,FUNCT_2:64;
reconsider g as continuous Function of X,Y by A3,Th2;
h = f*g by A5,Def2;
then
A6: a = f.(g.x) by A2,FUNCT_2:15;
g.x in pi(A,x) by A4,CARD_3:def 6;
hence thesis by A6,FUNCT_2:35;
end;
let a be object;
assume a in f.:pi(A,x);
then consider b being object such that
b in the carrier of Y and
A7: b in pi(A,x) and
A8: a = f.b by FUNCT_2:64;
consider g being Function such that
A9: g in A and
A10: b = g.x by A7,CARD_3:def 6;
reconsider g as continuous Function of X,Y by A9,Th2;
f*g = Xf.g by Def2;
then
A11: f*g in Xf.:A by A9,FUNCT_2:35;
a = (f*g).x by A8,A10,FUNCT_2:15;
hence thesis by A11,CARD_3:def 6;
end;
:: 4.2. LEMMA (ii)
theorem Th13:
for X being non empty TopSpace for Y,Z being
monotone-convergence T_0-TopSpace for f being continuous Function 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;
let f be continuous Function of Y,Z;
let A be Subset of oContMaps(X, Y);
reconsider sA = sup A as continuous Function of X,Y by Th2;
set Xf = oContMaps(X, f);
reconsider sfA = sup (Xf.:A), XfsA = Xf.sup A as Function of X, Omega Z by
Th1;
reconsider XZ = oContMaps(X, Z) as directed-sups-inheriting non empty full
SubRelStr of (Omega Z) |^ the carrier of X by WAYBEL24:def 3,WAYBEL25:43;
assume A is non empty directed;
then reconsider A9 = A as non empty directed Subset of oContMaps(X, Y);
reconsider fA9 = Xf.:A9 as non empty directed Subset of oContMaps(X, Z) by
Th8,YELLOW_2:15;
reconsider XY = oContMaps(X, Y) as directed-sups-inheriting non empty full
SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3,WAYBEL25:43;
reconsider B = A9 as non empty directed Subset of XY;
reconsider B9 = B as non empty directed Subset of (Omega Y) |^ the carrier
of X by YELLOW_2:7;
reconsider fB = fA9 as non empty directed Subset of XZ;
reconsider fB9 = fB as non empty directed Subset of (Omega Z) |^ the carrier
of X by YELLOW_2:7;
assume ex_sup_of A, oContMaps(X, Y);
set I = the carrier of X;
set J1 = I --> Omega Y;
set J2 = I --> Omega 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 f9 = f as continuous Function of Omega Y, Omega Z by
YELLOW12:36;
ex_sup_of fB9, (Omega Z) |^ the carrier of X by WAYBEL_0:75;
then
A1: sup fB9 = sup (oContMaps(X, f).:A) by WAYBEL_0:7;
oContMaps(X, Z) is up-complete & fA9 is directed by Th7;
hence ex_sup_of oContMaps(X, f).:A, oContMaps(X, Z) by WAYBEL_0:75;
A2: (Omega Z) |^ I = I-POS_prod J2 by YELLOW_1:def 5;
then reconsider fB99 = fB9 as non empty directed Subset of I-POS_prod J2;
now
let x be Element of X;
J2.x = Omega Z & pi(fB99,x) is directed by FUNCOP_1:7,YELLOW16:35;
hence ex_sup_of pi(fB99,x), J2.x by WAYBEL_0:75;
end;
then
A3: ex_sup_of fB99, I-POS_prod J2 by YELLOW16:31;
A4: (Omega Y) |^ the carrier of X = I-POS_prod J1 by YELLOW_1:def 5;
then reconsider B99 = B9 as non empty directed Subset of I-POS_prod J1;
A5: ex_sup_of B9, (Omega Y) |^ the carrier of X by WAYBEL_0:75;
then
A6: sup B9 = sup A by WAYBEL_0:7;
now
let x be Element of X;
A7: J1.x = Omega Y by FUNCOP_1:7;
then reconsider Bx = pi(B99,x) as directed non empty Subset of Omega Y by
YELLOW16:35;
A8: J2.x = Omega Z & ex_sup_of Bx, Omega Y by FUNCOP_1:7,WAYBEL_0:75;
A9: (sup B99).x = sup pi(B99,x) by A5,A4,YELLOW16:33;
A10: f9 preserves_sup_of Bx & pi(fB99,x) = f9.:Bx by Th12,WAYBEL_0:def 37;
thus sfA.x = sup pi(fB99,x) by A1,A2,A3,YELLOW16:33
.= f.sup Bx by A8,A10
.= (f*sA).x by A6,A4,A9,A7,FUNCT_2:15
.= XfsA.x by Def2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th14:
for X,Y,Z being non empty TopSpace for f being continuous
Function 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 Function 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 object;
assume a in pi(fX.:A,x);
then consider h being Function such that
A1: h in fX.:A and
A2: a = h.x by CARD_3:def 6;
consider g being object such that
A3: g in the carrier of oContMaps(Z,X) and
A4: g in A and
A5: h = fX.g by A1,FUNCT_2:64;
reconsider g as continuous Function of Z,X by A3,Th2;
h = g*f by A5,Def3;
then a = g.(f.x) by A2,FUNCT_2:15;
hence thesis by A4,CARD_3:def 6;
end;
let a be object;
assume a in pi(A,f.x);
then consider g being Function such that
A6: g in A and
A7: a = g.(f.x) by CARD_3:def 6;
reconsider g as continuous Function of Z,X by A6,Th2;
g*f = fX.g by Def3;
then
A8: g*f in fX.:A by A6,FUNCT_2:35;
a = (g*f).x by A7,FUNCT_2:15;
hence thesis by A8,CARD_3:def 6;
end;
theorem Th15:
for Y,Z being non empty TopSpace for X being
monotone-convergence T_0-TopSpace for f being continuous Function 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;
let f be continuous Function of Y,Z;
let A be Subset of oContMaps(Z, X);
reconsider sA = sup A as continuous Function of Z,X by Th2;
set fX = oContMaps(f, X);
reconsider sfA = sup (fX.:A), XfsA = fX.sup A as Function of Y, Omega X by
Th1;
reconsider YX = oContMaps(Y, X) as directed-sups-inheriting non empty full
SubRelStr of (Omega X) |^ the carrier of Y by WAYBEL24:def 3,WAYBEL25:43;
assume A is non empty directed;
then reconsider A9 = A as non empty directed Subset of oContMaps(Z, X);
reconsider fA9 = fX.:A9 as non empty directed Subset of oContMaps(Y, X) by
Th10,YELLOW_2:15;
reconsider ZX = oContMaps(Z, X) as directed-sups-inheriting non empty full
SubRelStr of (Omega X) |^ the carrier of Z by WAYBEL24:def 3,WAYBEL25:43;
reconsider B = A9 as non empty directed Subset of ZX;
reconsider B9 = B as non empty directed Subset of (Omega X) |^ the carrier
of Z by YELLOW_2:7;
reconsider fB = fA9 as non empty directed Subset of YX;
reconsider fB9 = fB as non empty directed Subset of (Omega X) |^ the carrier
of Y by YELLOW_2:7;
assume ex_sup_of A, oContMaps(Z, X);
set I1 = the carrier of Z, I2 = the carrier of Y;
set J1 = I1 --> Omega X;
set J2 = I2 --> Omega X;
ex_sup_of fB9, (Omega X) |^ the carrier of Y by WAYBEL_0:75;
then
A1: sup fB9 = sup (oContMaps(f, X).:A) by WAYBEL_0:7;
oContMaps(Y, X) is up-complete & fA9 is directed by Th7;
hence ex_sup_of oContMaps(f, X).:A, oContMaps(Y, X) by WAYBEL_0:75;
A2: (Omega X) |^ I2 = I2-POS_prod J2 by YELLOW_1:def 5;
then reconsider fB99 = fB9 as non empty directed Subset of I2-POS_prod J2;
now
let x be Element of Y;
J2.x = Omega X & pi(fB99,x) is directed by FUNCOP_1:7,YELLOW16:35;
hence ex_sup_of pi(fB99,x), J2.x by WAYBEL_0:75;
end;
then
A3: ex_sup_of fB99, I2-POS_prod J2 by YELLOW16:31;
A4: (Omega X) |^ I1 = I1-POS_prod J1 by YELLOW_1:def 5;
then reconsider B99 = B9 as non empty directed Subset of I1-POS_prod J1;
A5: ex_sup_of B9, (Omega X) |^ the carrier of Z by WAYBEL_0:75;
then
A6: sup B9 = sup A by WAYBEL_0:7;
now
let x be Element of Y;
A7: J1.(f.x) = Omega X & J2.x = Omega X by FUNCOP_1:7;
A8: pi(fB99,x) = pi(B99,f.x) by Th14;
thus sfA.x = sup pi(fB99,x) by A1,A2,A3,YELLOW16:33
.= (sup B99).(f.x) by A5,A4,A7,A8,YELLOW16:33
.= (sA*f).x by A6,A4,FUNCT_2:15
.= XfsA.x by Def3;
end;
hence thesis by FUNCT_2:63;
end;
:: 4.3. LEMMA (i) genralized
theorem Th16:
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: Omega Y is full SubRelStr of Omega Z by WAYBEL25:17;
A2: [#]Y c= [#]Z by PRE_TOPC:def 4;
XY is SubRelStr of XZ
proof
thus
A3: the carrier of XY c= the carrier of XZ
proof
let x be object;
assume x in the carrier of XY;
then reconsider f = x as continuous Function of X, Y by Th2;
dom f = the carrier of X & rng f c= the carrier of Z by A2,FUNCT_2:def 1;
then x is continuous Function of X,Z by FUNCT_2:2,PRE_TOPC:26;
then x is Element of XZ by Th2;
hence thesis;
end;
let x,y be object;
assume
A4: [x,y] in the InternalRel of XY;
reconsider x, y as Element of XY by A4,ZFMISC_1:87;
reconsider a = x, b = y as Element of XZ by A3;
reconsider f = x, g = y as continuous Function of X, Omega Y by Th1;
reconsider f9 = a, g9 = b as continuous Function of X, Omega Z by Th1;
x <= y by A4,ORDERS_2:def 5;
then f <= g by Th3;
then f9 <= g9 by A1,YELLOW16:2;
then a <= b by Th3;
hence thesis by ORDERS_2:def 5;
end;
then reconsider XY as non empty SubRelStr of XZ;
A5: (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 A5,XBOOLE_1:19;
let x,y be object;
assume
A6: [x,y] in (the InternalRel of XZ)|_2 the carrier of XY;
then
A7: [x,y] in [:the carrier of XY, the carrier of XY:] by A5,XBOOLE_0:def 4;
reconsider x,y as Element of XY by A7,ZFMISC_1:87;
the carrier of XY c= the carrier of XZ by YELLOW_0:def 13;
then reconsider a = x, b = y as Element of XZ;
reconsider f9 = a, g9 = b as continuous Function of X, Omega Z by Th1;
reconsider f = x, g = y as continuous Function of X, Omega Y by Th1;
[a,b] in the InternalRel of XZ by A5,A6,XBOOLE_0:def 4;
then a <= b by ORDERS_2:def 5;
then f9 <= g9 by Th3;
then f <= g by A1,YELLOW16:3;
then x <= y by Th3;
hence thesis by ORDERS_2:def 5;
end;
hence thesis by YELLOW_0:def 14;
end;
theorem Th17:
for Z being monotone-convergence T_0-TopSpace for Y being non
empty SubSpace of Z for f being continuous Function of Z,Y st f is
being_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 Function of Z,Y;
A1: the RelStr of OZ = the RelStr of Omega Z;
[#]Y c= [#]Z by PRE_TOPC:def 4;
then dom f = the carrier of Z & rng f c= the carrier of Z by FUNCT_2:def 1;
then
A2: f is continuous Function of Z,Z by PRE_TOPC:26,RELSET_1:4;
the TopStruct of Omega Z = the TopStruct of Z by WAYBEL25:def 2;
then reconsider f9 = f as continuous Function of Omega Z, Omega Z by A2,
YELLOW12:36;
reconsider g = f9 as Function of OZ, OZ;
assume
A3: f is being_a_retraction;
then g is idempotent directed-sups-preserving by YELLOW16:45;
then
A4: Image g is directed-sups-inheriting by YELLOW16:6;
the TopStruct of Omega Y = the TopStruct of Y & rng g = the carrier of
subrelstr rng g by WAYBEL25:def 2,YELLOW_0:def 15;
then OY is directed-sups-inheriting by A3,A4,A1,WAYBEL21:22,YELLOW16:44;
hence thesis;
end;
Lm1: for Z being monotone-convergence T_0-TopSpace for Y being non empty
SubSpace of Z for f being continuous Function of Z,Y st f is being_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 Function of Z,Y;
assume f is being_a_retraction;
then Y is_a_retract_of Z;
hence thesis by WAYBEL25:36,YELLOW16:56;
end;
theorem Th18:
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
Function of Z,Y st f is being_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 Th7;
let f be continuous Function of Z,Y;
set F = oContMaps(X, f);
reconsider sXY = XY as full non empty SubRelStr of uXZ by Th16;
assume
A1: f is being_a_retraction;
then reconsider Y9 = Y as monotone-convergence T_0-TopSpace by Lm1;
oContMaps(X,Y9) is up-complete by Th7;
hence F is directed-sups-preserving Function of XZ, XY by Th13;
A2: the carrier of sXY c= the carrier of uXZ by YELLOW_0:def 13;
A3: now
let x be object;
A4: dom f = the carrier of Z by FUNCT_2:def 1;
A5: rng f = the carrier of Y & f is idempotent by A1,YELLOW16:44,45;
assume
A6: x in the carrier of XY;
then reconsider a = x as Element of XZ by A2;
reconsider a as continuous Function of X, Z by Th2;
x is Function of X,Y by A6,Th2;
then rng a c= the carrier of Y by RELAT_1:def 19;
then f*a = a by A5,A4,YELLOW16:4;
hence (id XY).x = f*a by A6,FUNCT_1:18
.= F.a by Def2
.= (F|the carrier of XY).x by A6,FUNCT_1:49;
end;
F|the carrier of XY is Function of the carrier of XY, the carrier of XY
by A2,FUNCT_2:32;
then
dom id XY = the carrier of XY & dom (F|the carrier of XY) = the carrier
of XY by FUNCT_2:def 1;
hence F|the carrier of XY = id XY by A3,FUNCT_1:2;
Omega Y is directed-sups-inheriting full SubRelStr of Omega Z by A1,Th17,
WAYBEL25:17;
then oContMaps(X, Y9) is directed-sups-inheriting full non empty SubRelStr
of ( Omega Y)|^the carrier of X & (Omega Y)|^the carrier of X is
directed-sups-inheriting full SubRelStr of (Omega Z)|^the carrier of X by
WAYBEL24:def 3,WAYBEL25:43,YELLOW16:39,42;
then
oContMaps(X, Z) is directed-sups-inheriting full non empty SubRelStr of
( Omega Z)|^the carrier of X & oContMaps(X,Y) is directed-sups-inheriting full
SubRelStr of (Omega Z)|^the carrier of X by WAYBEL24:def 3,WAYBEL25:43
,YELLOW16:26,27;
hence thesis by Th16,YELLOW16:28;
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 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 Function of Z,Y such that
A1: f is being_a_retraction;
take oContMaps(X, f);
thus thesis by A1,Th18;
end;
theorem Th20:
for X,Y,Z being non empty TopSpace for f being continuous
Function of Y,Z st f is being_homeomorphism holds oContMaps(X, f) is isomorphic
proof
let X,Y,Z be non empty TopSpace;
let f be continuous Function of Y,Z;
set XY = oContMaps(X,Y), XZ = oContMaps(X,Z);
assume
A1: f is being_homeomorphism;
then reconsider g = f" as continuous Function of Z,Y by TOPS_2:def 5;
set Xf = oContMaps(X,f), Xg = oContMaps(X,g);
A2: f is one-to-one & rng f = [#]Z by A1,TOPS_2:def 5;
now
let a be Element of XZ;
reconsider h = a as continuous Function of X,Z by Th2;
thus (Xf*Xg).a = Xf.(Xg.a) by FUNCT_2:15
.= Xf.(g*h) by Def2
.= f*(g*h) by Def2
.= f*g*h by RELAT_1:36
.= (id the carrier of Z)*h by A2,TOPS_2:52
.= a by FUNCT_2:17
.= (id XZ).a;
end;
then
A3: Xf*Xg = id XZ by FUNCT_2:63;
A4: dom f = [#]Y by A1,TOPS_2:def 5;
now
let a be Element of XY;
reconsider h = a as continuous Function of X,Y by Th2;
thus (Xg*Xf).a = Xg.(Xf.a) by FUNCT_2:15
.= Xg.(f*h) by Def2
.= g*(f*h) by Def2
.= g*f*h by RELAT_1:36
.= (id the carrier of Y)*h by A2,A4,TOPS_2:52
.= a by FUNCT_2:17
.= (id XY).a;
end;
then
A5: Xg*Xf = id XY by FUNCT_2:63;
Xf is monotone & Xg is monotone by Th8;
hence thesis by A5,A3,YELLOW16:15;
end;
theorem Th21:
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 Function of Y,Z such that
A1: f is being_homeomorphism;
reconsider f as continuous Function of Y,Z by A1,TOPS_2:def 5;
take oContMaps(X, f);
thus thesis by A1,Th20;
end;
:: 4.3. LEMMA (ii)
theorem Th22:
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
by Th19,YELLOW16:21,YELLOW16:22;
theorem Th23:
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 and
A2: S,Y are_homeomorphic by YELLOW16:57;
assume oContMaps(X, Z) is complete continuous;
then
A3: oContMaps(X,S) is complete continuous by A1,Th22;
oContMaps(X,S), oContMaps(X,Y) are_isomorphic by A2,Th21;
hence thesis by A3,WAYBEL15:9,WAYBEL20:18;
end;
theorem Th24:
for Y being non trivial T_0-TopSpace st not Y is T_1 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 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;
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 Function of Sierpinski_Space, Omega Y by
YELLOW16:47;
then reconsider
i = (0,1) --> (x,y) as continuous Function of Sierpinski_Space, Y
by A5,YELLOW12:36;
reconsider V as open Subset of Omega Y by A3,A5,TOPS_3:76;
reconsider c = chi(V, the carrier of Y) as continuous Function of Y,
Sierpinski_Space by A3,YELLOW16:46;
c*i = id Sierpinski_Space by A5,A6,YELLOW16:48;
hence thesis by WAYBEL25:def 1;
end;
theorem Th25:
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 T_1
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 STRUCT_0:def 10;
set i = the Element of X;
reconsider f = X --> a, g = X --> b as continuous Function of X, Y;
assume oContMaps(X, Y) is with_suprema;
then reconsider XY = oContMaps(X, Y) as sup-Semilattice;
reconsider ef = f, eg = g as Element of XY by Th2;
reconsider h = ef "\/" eg, f = ef, g = eg as continuous Function of X, Omega
Y by Th1;
A2: f.i = a & g.i = b by FUNCOP_1:7;
now
eg <= ef "\/" eg by YELLOW_0:22;
then g <= h by Th3;
then
A3: ex x,y being Element of Omega Y st x = g.i & y = h.i & x <= y;
ef <= ef "\/" eg by YELLOW_0:22;
then f <= h by Th3;
then
A4: ex x,y being Element of Omega Y st x = f.i & y = h.i & x <= y;
assume
A5: not ex x,y being Element of Omega Y st x <= y & x <> y;
then not (f.i <= h.i & f.i <> h.i);
hence contradiction by A1,A2,A5,A4,A3;
end;
then consider x,y being Element of Omega Y such that
A6: x <= y and
A7: x <> y;
A8: 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 A7;
let W,V be Subset of Y;
assume W is open;
then reconsider W as open Subset of Omega Y by A8,TOPS_3:76;
W is upper;
hence thesis by A6;
end;
registration
cluster Sierpinski_Space -> non trivial monotone-convergence;
coherence
proof
A1: 1 in {0,1} by TARSKI:def 2;
the carrier of Sierpinski_Space = {0,1} & 0 in {0,1} by TARSKI:def 2
,WAYBEL18:def 9;
hence thesis by A1;
end;
end;
registration
cluster injective monotone-convergence non trivial for T_0-TopSpace;
existence
proof
take Sierpinski_Space;
thus thesis;
end;
end;
:: 4.4. PROPOSITION
theorem Th26:
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 Sierpinski_Space is_Retract_of Y by Th24,Th25;
then
A2: oContMaps(X, Sierpinski_Space) is complete continuous by A1,Th23;
InclPoset the topology of X, oContMaps(X, Sierpinski_Space)
are_isomorphic by Th6;
hence thesis by A2,WAYBEL15:9,WAYBEL_1:6;
end;
theorem Th27:
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 Function of oContMaps(X,Y), oContMaps(X,Y) st (for f being
continuous Function of X,Y holds F.f = X --> (f.x)) & ex h being continuous
Function 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 Function of X,X;
set F = oContMaps(f, Y);
dom f = the carrier of X by FUNCT_2:def 1;
then f*f = (the carrier of X) --> (f.x) by FUNCOP_1:17
.= f by FUNCOP_1:7;
then f is idempotent by QUANTAL1:def 9;
then F is directed-sups-preserving idempotent Function of XY,XY by Th11,Th15;
then reconsider
F as directed-sups-preserving projection Function of XY,XY by WAYBEL_1:def 13
;
take F;
hereby
let h be continuous Function of X,Y;
A1: the carrier of X = dom h by FUNCT_2:def 1;
thus F.h = h*((the carrier of X) --> x) by Def3
.= X --> (h.x) by A1,FUNCOP_1:17;
end;
thus thesis;
end;
:: 4.5. PROPOSITION
theorem Th28:
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;
set b = the Element of X;
A2: the TopStruct of Omega Y = the TopStruct of Y by WAYBEL25:def 2;
consider F being directed-sups-preserving projection Function of oContMaps(X
,Y), oContMaps(X,Y) such that
A3: for f being continuous Function of X,Y holds F.f = X --> (f.b) and
ex h being continuous Function of X,X st h = X --> b & F = oContMaps(h,
Y) by Th27;
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:26;
A4: the carrier of imF = rng F by YELLOW_0:def 15;
A5: dom F = the carrier of oContMaps(X,Y) by FUNCT_2:52;
now
let a be set;
hereby
assume a is Element of imF;
then consider h being object such that
A6: h in dom F and
A7: a = F.h by A4,FUNCT_1:def 3;
reconsider h as continuous Function of X,Y by A6,Th2;
reconsider x = h.b as Element of Omega Y by A2;
a = X --> (h.b) by A3,A7
.= (the carrier of X) --> x;
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;
a = X --> x by A8;
then
A9: a is Element of oContMaps(X,Y) by Th1;
then reconsider h = a as continuous Function of X,Y by Th2;
A10: X --> (h.b) = (the carrier of X) --> (h.b);
h.b = x by A8,FUNCOP_1:7;
then F.a = X --> x by A3,A10;
hence a is Element of imF by A4,A5,A8,A9,FUNCT_1:def 3;
end;
then Omega Y, imF are_isomorphic by YELLOW16:50;
then
A11: imF, Omega Y are_isomorphic by WAYBEL_1:6;
Image F is complete continuous LATTICE by A1,WAYBEL15:15,YELLOW_2:35;
hence thesis by A11,WAYBEL15:9,WAYBEL20:18;
end;
theorem Th29:
for X being non empty 1-sorted, I being non empty set for J
being TopStruct-yielding non-Empty ManySortedSet of I
for f being Function 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 TopStruct-yielding non-Empty ManySortedSet of I;
let f be Function of X, I-TOP_prod J;
A1: the carrier of I-TOP_prod J = product Carrier J by WAYBEL18:def 3;
let i be Element of I;
A2: dom Carrier J = I by PARTFUN1:def 2;
A3: rng f c= Funcs(I, Union Carrier J)
proof
let g be object;
assume g in rng f;
then consider h being Function such that
A4: g = h and
A5: dom h = I and
A6: for x being object st x in I holds h.x in (Carrier J).x
by A1,A2,CARD_3:def 5;
rng h c= Union Carrier J
proof
let y be object;
A7: dom Carrier J = I by PARTFUN1:def 2;
assume y in rng h;
then consider x being object such that
A8: x in dom h and
A9: y = h.x by FUNCT_1:def 3;
h.x in (Carrier J).x by A5,A6,A8;
hence thesis by A5,A8,A9,A7,CARD_5:2;
end;
hence thesis by A4,A5,FUNCT_2:def 2;
end;
dom f = the carrier of X by FUNCT_2:def 1;
then
A10: f in Funcs(the carrier of X, Funcs(I, Union Carrier J)) by A3,
FUNCT_2:def 2;
then commute f in Funcs(I, Funcs(the carrier of X, Union Carrier J)) by
FUNCT_6:55;
then
A11: 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;
then (commute f).i in rng commute f by FUNCT_1:def 3;
then consider g being Function such that
A12: (commute f).i = g and
A13: dom g = the carrier of X and
rng g c= Union Carrier J by A11,FUNCT_2:def 2;
A14: now
let x be object;
A15: dom proj(Carrier J, i) = product Carrier J by CARD_3:def 16;
assume x in the carrier of X;
then reconsider a = x as Element of X;
consider h being Function such that
A16: f.a = h and
dom h = I and
for x being object st x in I holds h.x in (Carrier J).x
by A1,A2,CARD_3:def 5;
(proj(J,i)*f).a = proj(J,i).(f.a) by FUNCT_2:15
.= (proj (Carrier J, i)).(f.a) by WAYBEL18:def 4
.= h.i by A1,A16,A15,CARD_3:def 16;
hence g.x = (proj(J,i)*f).x by A10,A12,A16,FUNCT_6:56;
end;
dom (proj(J, i)*f) = the carrier of X by FUNCT_2:def 1;
hence thesis by A12,A13,A14,FUNCT_1:2;
end;
theorem Th30:
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 object;
assume
A1: i in M;
then
(M --> S).i = S & ex R being 1-sorted st R = (M --> S).i & (Carrier (M
--> S )).i = the carrier of R by FUNCOP_1:7,PRALG_1:def 15;
hence (Carrier (M --> S)).i = (M --> the carrier of S).i by A1,FUNCOP_1:7;
end;
hence thesis by PBOOLE:3;
end;
theorem Th31:
for X,Y being non empty TopSpace, M being non empty set for f
being continuous Function 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 Function of X, M-TOP_prod (M --> Y);
A1: rng f c= Funcs(M, the carrier of Y)
proof
let g be object;
assume
A2: g in rng f;
A3: dom (M --> the carrier of Y) = M by FUNCOP_1:13;
the carrier of M-TOP_prod (M --> Y) = product Carrier (M --> Y) by
WAYBEL18:def 3
.= product (M --> the carrier of Y) by Th30;
then consider h being Function such that
A4: g = h and
A5: dom h = M and
A6: for x being object st x in M holds h.x in (M --> the carrier of Y).x
by A2,A3,CARD_3:def 5;
rng h c= the carrier of Y
proof
let y be object;
assume y in rng h;
then consider x being object such that
A7: x in dom h and
A8: y = h.x by FUNCT_1:def 3;
(M --> the carrier of Y).x = the carrier of Y by A5,A7,FUNCOP_1:7;
hence thesis by A5,A6,A7,A8;
end;
hence thesis by A4,A5,FUNCT_2:def 2;
end;
dom f = the carrier of X by FUNCT_2:def 1;
then f in Funcs(the carrier of X, Funcs(M, the carrier of Y)) by A1,
FUNCT_2:def 2;
then
A9: commute f in Funcs(M, Funcs(the carrier of X, the carrier of Y)) by
FUNCT_6:55;
A10: rng commute f c= the carrier of oContMaps(X, Y)
proof
let g be object;
assume g in rng commute f;
then consider i being object such that
A11: i in dom commute f and
A12: g = (commute f).i by FUNCT_1:def 3;
ex h being Function st commute f = h & dom h = M & rng h c= Funcs(the
carrier of X, the carrier of Y) by A9,FUNCT_2:def 2;
then reconsider i as Element of M by A11;
A13: (M --> Y).i = Y by FUNCOP_1:7;
g = proj(M --> Y, i)*f by A12,Th29;
then g is continuous Function of X,Y by A13,WAYBEL18:6;
then g is Element of oContMaps(X,Y) by Th2;
hence thesis;
end;
ex g being Function st commute f = g & dom g = M & rng g c= Funcs(the
carrier of X, the carrier of Y) by A9,FUNCT_2:def 2;
hence thesis by A10,FUNCT_2:2;
end;
theorem Th32:
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) is SubRelStr of (Omega Y)|^the carrier of X by WAYBEL24:def 3
;
then
A1: the carrier of oContMaps(X, Y) c= the carrier of (Omega Y)|^the carrier
of X by YELLOW_0:def 13;
the TopStruct of Y = the TopStruct of Omega Y by WAYBEL25:def 2;
hence thesis by A1,YELLOW_1:28;
end;
theorem Th33:
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 Function 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);
reconsider B = product_prebasis (M --> Y) as prebasis of M-TOP_prod (M --> Y
) by WAYBEL18:def 3;
A1: Carrier (M --> Y) = M --> the carrier of Y by Th30;
the carrier of oContMaps(X, Y) c= Funcs(the carrier of X, the carrier of
Y) by Th32;
then dom f = M & rng f c= Funcs(the carrier of X, the carrier of Y) by
FUNCT_2:def 1;
then
A2: f in Funcs(M, Funcs(the carrier of X, the carrier of Y)) by FUNCT_2:def 2;
then commute f in Funcs(the carrier of X, Funcs(M, the carrier of Y)) by
FUNCT_6:55;
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;
the carrier of M-TOP_prod (M --> Y) = product Carrier (M --> Y) by
WAYBEL18:def 3;
then the carrier of M-TOP_prod (M --> Y) = Funcs(M, the carrier of Y) by A1,
CARD_3:11;
then reconsider g = commute f as Function of X, M-TOP_prod (M --> Y) by A3,
FUNCT_2:2;
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
A4: i in M and
A5: V is open and
A6: T = (M --> Y).i and
A7: P = product ((Carrier (M --> Y)) +* (i,V)) by WAYBEL18:def 2;
reconsider i as Element of M by A4;
set FP = (Carrier (M --> Y)) +* (i,V);
A8: dom FP = dom Carrier (M --> Y) by FUNCT_7:30;
reconsider fi = f.i as continuous Function of X, Y by Th2;
A9: dom Carrier (M --> Y) = M by A1,FUNCOP_1:13;
then
A10: FP.i = V by FUNCT_7:31;
A11: T = Y by A4,A6,FUNCOP_1:7;
now
let x be set;
hereby
reconsider Q = fi"V as Subset of X;
assume
A12: x in g"P;
then g.x in P by FUNCT_2:38;
then consider gx being Function such that
A13: g.x = gx and
dom gx = dom FP and
A14: for z being object st z in dom FP holds gx.z in FP.z
by A7,CARD_3:def 5;
A15: gx.i = fi.x by A2,A12,A13,FUNCT_6:56;
take Q;
[#]Y <> {};
hence Q is open by A5,A11,TOPS_2:43;
thus Q c= g"P
proof
let a be object;
assume
A16: a in Q;
then g.a in rng g by A3,FUNCT_1:def 3;
then consider ga being Function such that
A17: g.a = ga and
A18: dom ga = M and
A19: rng ga c= the carrier of Y by A3,FUNCT_2:def 2;
A20: fi.a in V by A16,FUNCT_2:38;
now
let z be object;
assume
A21: z in M;
then
z <> i & (M --> the carrier of Y).z = the carrier of Y or z =
i by FUNCOP_1:7;
then
z <> i & ga.z in rng ga & FP.z = the carrier of Y or z = i by A1
,A18,A21,FUNCT_1:def 3,FUNCT_7:32;
hence ga.z in FP.z by A2,A10,A16,A20,A17,A19,FUNCT_6:56;
end;
then ga in P by A7,A8,A9,A18,CARD_3:9;
hence thesis by A16,A17,FUNCT_2:38;
end;
gx.i in V by A8,A9,A10,A14;
hence x in Q by A12,A15,FUNCT_2:38;
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:25;
end;
hence thesis by YELLOW_9:36;
end;
theorem Th34:
for X being non empty TopSpace, M being non empty set ex F being
Function 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
Function 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, S9M = M-TOP_prod (M --> S);
set XxxS9M = oContMaps(X, S9M), XxS = oContMaps(X, S);
set XxS9xM = M-POS_prod (M --> XxS);
deffunc F(Element of XxxS9M) = commute $1;
consider F being ManySortedSet of the carrier of XxxS9M such that
A1: for f being Element of XxxS9M holds F.f = F(f) from PBOOLE:sch 5;
A2: dom F = the carrier of XxxS9M by PARTFUN1:def 2;
rng F c= the carrier of XxS9xM
proof
let g be object;
assume g in rng F;
then consider f being object such that
A3: f in dom F and
A4: g = F.f by FUNCT_1:def 3;
reconsider f as continuous Function of X, S9M by A3,Th2;
g = commute f by A1,A3,A4;
then reconsider g as Function of M, the carrier of XxS by Th31;
dom g = M & rng g c= the carrier of XxS by FUNCT_2:def 1;
then g in Funcs(M, the carrier of XxS) by FUNCT_2:def 2;
then g in the carrier of XxS|^M by YELLOW_1:28;
hence thesis by YELLOW_1:def 5;
end;
then reconsider F as Function of XxxS9M, XxS9xM by A2,FUNCT_2:2;
deffunc F(Element of XxS9xM) = commute $1;
consider G being ManySortedSet of the carrier of XxS9xM such that
A5: for f being Element of XxS9xM holds G.f = F(f) from PBOOLE:sch 5;
A6: dom G = the carrier of XxS9xM by PARTFUN1:def 2;
A7: rng G c= the carrier of XxxS9M
proof
let g be object;
assume g in rng G;
then consider f being object such that
A8: f in dom G and
A9: g = G.f by FUNCT_1:def 3;
f in the carrier of XxS|^M by A6,A8,YELLOW_1:def 5;
then f in Funcs(M, the carrier of XxS) by YELLOW_1:28;
then consider f9 being Function such that
A10: f = f9 and
A11: dom f9 = M & rng f9 c= the carrier of XxS by FUNCT_2:def 2;
A12: f9 is Function of M, the carrier of XxS by A11,FUNCT_2:2;
g = commute f9 by A5,A8,A9,A10;
then g is continuous Function of X, S9M by A12,Th33;
then g is Element of XxxS9M by Th2;
hence thesis;
end;
take F;
A13: the carrier of S9M = product Carrier (M --> S) by WAYBEL18:def 3
.= product (M --> the carrier of S) by Th30
.= Funcs(M, the carrier of S) by CARD_3:11;
reconsider G as Function of XxS9xM, XxxS9M by A6,A7,FUNCT_2:2;
A14: the carrier of XxxS9M c= Funcs(the carrier of X, the carrier of S9M) by
Th32;
now
let a be Element of XxxS9M;
A15: commute commute a = a by A14,A13,FUNCT_6:57;
thus (G*F).a = G.(F.a) by FUNCT_2:15
.= commute (F.a) by A5
.= a by A1,A15
.= (id XxxS9M).a;
end;
then
A16: G*F = id XxxS9M by FUNCT_2:63;
A17: the RelStr of Omega S9M = M-POS_prod(M --> Omega S) by WAYBEL25:14;
A18: F is monotone
proof
let a, b be Element of XxxS9M such that
A19: a <= b;
reconsider f9 = a, g9 = b as continuous Function of X, S9M by Th2;
reconsider f = a, g = b as continuous Function of X, Omega S9M by Th1;
now
let i be Element of M;
A20: (M --> XxS).i = XxS by FUNCOP_1:7;
then reconsider
Fai = (F.a).i, Fbi = (F.b).i as continuous Function 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;
b in the carrier of XxxS9M & F.b = commute g by A1;
then
A21: Fbi.x = (g9.x).i by A14,A13,FUNCT_6:56;
reconsider fx = f.x, gx = g.x as Element of M-POS_prod(M --> Omega S)
by A17;
a in the carrier of XxxS9M & F.a = commute f by A1;
then
A22: Fai.x = (f9.x).i by A14,A13,FUNCT_6:56;
f <= g by A19,Th3;
then ex a, b being Element of Omega S9M st a = f.x & b = g.x & a <= b;
then fx <= gx by A17,YELLOW_0:1;
then
A23: fx.i <= gx.i by WAYBEL_3:28;
(M --> Omega S).i = Omega S by FUNCOP_1:7;
hence ex a, b being Element of Omega S st a = Fai.j & b = Fbi.j & a <=
b by A22,A21,A23;
end;
then Fai <= Fbi;
hence (F.a).i <= (F.b).i by A20,Th3;
end;
hence thesis by WAYBEL_3:28;
end;
A24: the carrier of XxS9xM = the carrier of XxS|^M by YELLOW_1:def 5
.= Funcs(M, the carrier of XxS) by YELLOW_1:28;
then
A25: the carrier of XxS9xM c= Funcs(M, Funcs(the carrier of X, the carrier
of S)) by Th32,FUNCT_5:56;
A26: G is monotone
proof
let a,b be Element of XxS9xM such that
A27: a <= b;
reconsider f = G.a, g = G.b as continuous Function of X, Omega S9M 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
A17;
now
let j be Element of M;
A28: (M --> XxS).j = XxS by FUNCOP_1:7;
then reconsider
aj = a.j, bj = b.j as continuous Function of X, Omega S by Th1;
a.j <= b.j by A27,WAYBEL_3:28;
then aj <= bj by A28,Th3;
then
A29: ex a, b being Element of Omega S st a = aj.x & b = bj.x & a <= b;
b in the carrier of XxS9xM & G.b = commute b by A5;
then
A30: gx.j = bj.x by A25,FUNCT_6:56;
a in the carrier of XxS9xM & G.a = commute a by A5;
then fx.j = aj.x by A25,FUNCT_6:56;
hence fx.j <= gx.j by A30,A29,FUNCOP_1:7;
end;
then fx <= gx by WAYBEL_3:28;
hence ex a,b being Element of Omega S9M st a = f.i & b = g.i & a <= b by
A17,YELLOW_0:1;
end;
then f <= g;
hence thesis by Th3;
end;
now
let a be Element of XxS9xM;
a in Funcs(M, the carrier of XxS) & Funcs(M, the carrier of XxS) c=
Funcs(M, Funcs(the carrier of X, the carrier of S)) by A24,Th32,FUNCT_5:56;
then
A31: commute commute a = a by FUNCT_6:57;
thus (F*G).a = F.(G.a) by FUNCT_2:15
.= commute (G.a) by A1
.= a by A5,A31
.= (id XxS9xM).a;
end;
then F*G = id XxS9xM by FUNCT_2:63;
hence F is isomorphic by A18,A26,A16,YELLOW16:15;
let f be continuous Function of X, M-TOP_prod (M --> Sierpinski_Space);
f is Element of XxxS9M by Th2;
hence thesis by A1;
end;
theorem Th35:
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 Function 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 Function of X, M-TOP_prod (M --> Sierpinski_Space
) holds F.f = commute f by Th34;
take F;
thus thesis by A1;
end;
:: 4.6. PROPOSITION
theorem Th36:
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;
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:9,WAYBEL20:18;
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:19;
for i be Element of M holds (M --> Sierpinski_Space).i is injective by
FUNCOP_1:7;
then reconsider MS = M-TOP_prod (M --> Sierpinski_Space) as injective
T_0-TopSpace by WAYBEL18:7;
for i be Element of M holds (M --> XS).i is complete continuous LATTICE
by FUNCOP_1:7;
then
A3: M-POS_prod (M --> XS) is complete continuous by WAYBEL20:33;
M-POS_prod (M --> oContMaps(X, Sierpinski_Space)), oContMaps(X, M
-TOP_prod (M --> Sierpinski_Space)) are_isomorphic by Th35,WAYBEL_1:6;
then oContMaps(X, MS) is complete continuous by A3,WAYBEL15:9,WAYBEL20:18;
hence thesis by A2,Th23;
end;
registration
cluster non trivial complete Scott for TopLattice;
existence
proof
set L = BoolePoset{0};
set T = the Scott TopAugmentation of L;
take T;
BoolePoset{0} = InclPoset bool {0} & the RelStr of T = the RelStr of L by
YELLOW_1:4,YELLOW_9:def 4;
then
A1: the carrier of T = bool {0} by YELLOW_1:1;
0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
hence thesis by A1,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 Scott TopAugmentation of L by YELLOW_9:44;
Omega L = the TopRelStr of L by WAYBEL25:15;
then
A2: the RelStr of Omega L = the RelStr of L;
A3: L is monotone-convergence by WAYBEL25:29;
hereby
assume
A4: oContMaps(X, L) is complete continuous;
hence InclPoset the topology of X is continuous by A3,Th26;
Omega L is continuous by A1,A4,Th28;
hence L is continuous by A2,YELLOW12:15;
end;
thus thesis by A1,Th36;
end;
registration
let f be Function;
cluster Union disjoin f -> Relation-like;
coherence
by CARD_3:21;
end;
definition
let f be Function;
func *graph f -> Relation equals
(Union disjoin f)~;
correctness;
end;
reserve x,y for object,
f for Function;
theorem Th38:
[x,y] in *graph f iff x in dom f & y in f.x
proof
A1: [x,y] in *graph f iff [y,x] in Union disjoin f by RELAT_1:def 7;
[y,x]`1 = y & [y,x]`2 = x;
hence thesis by A1,CARD_3:22;
end;
theorem Th39:
for X being finite set holds proj1 X is finite & proj2 X is finite
proof
deffunc F(object) = $1`1;
let X be finite set;
consider f being Function such that
A1: dom f = X & for x being object st x in X holds f.x = F(x) from FUNCT_1:
sch 3;
A2: proj1 X c= rng f
proof
let x be object;
assume x in proj1 X;
then consider y being object such that
A3: [x,y] in X by XTUPLE_0:def 12;
[x,y]`1 = x;
then f.([x,y]) = x by A1,A3;
hence thesis by A1,A3,FUNCT_1:def 3;
end;
rng f is finite by A1,FINSET_1:8;
hence proj1 X is finite by A2;
deffunc F(object) = $1`2;
consider f being Function such that
A4: dom f = X & for x being object st x in X holds f.x = F(x) from FUNCT_1:
sch 3;
A5: proj2 X c= rng f
proof
let x be object;
assume x in proj2 X;
then consider y being object such that
A6: [y,x] in X by XTUPLE_0:def 13;
[y,x]`2 = x;
then f.([y,x]) = x by A4,A6;
hence thesis by A4,A6,FUNCT_1:def 3;
end;
rng f is finite by A4,FINSET_1:8;
hence thesis by A5;
end;
:: 4.8. LEMMA p.130.
theorem Th40:
for X,Y being non empty TopSpace for S being Scott
TopAugmentation of InclPoset the topology of Y for f being Function 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 Function of X, S;
A1: the RelStr of S = the RelStr of InclPoset the topology of Y by
YELLOW_9:def 4;
A2: dom f = the carrier of X by FUNCT_2:def 1;
assume *graph f is open Subset of [:X,Y:];
then consider AA being Subset-Family of [:X,Y:] such that
A3: *graph f = union AA and
A4: 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:5;
A5: the carrier of InclPoset the topology of Y = the topology of Y by
YELLOW_1:1;
A6: now
let P be Subset of S;
assume
A7: P is open;
now
let x be set;
hereby
defpred P[object,object] means
x in $2`1 & $1 in $2`2 & [:$2`1,$2`2:] c= *graph f;
assume
A8: x in f"P;
then reconsider y = x as Element of X;
A9: now
let e be object;
assume e in f.x;
then [x,e] in *graph f by A2,A8,Th38;
then consider V being set such that
A10: [x,e] in V and
A11: V in AA by A3,TARSKI:def 4;
consider A being Subset of X, B being Subset of Y such that
A12: V = [:A,B:] and
A13: A is open & B is open by A4,A11;
reconsider u = [A,B] as object;
take u;
A in the topology of X & B in the topology of Y by A13,PRE_TOPC:def 2
;
hence u in [:the topology of X, the topology of Y:] by ZFMISC_1:87;
thus P[e,u] by A3,A10,A11,A12,ZFMISC_1:74,87;
end;
consider g being Function such that
A14: dom g = f.x & rng g c= [:the topology of X, the topology of Y :] and
A15: for a being object st a in f.x holds P[a,g.a] from FUNCT_1:sch 6(A9);
set J = {union A where A is Subset of proj2 rng g: A is finite};
A16: proj2 rng g c= the topology of Y by A14,FUNCT_5:11;
A17: J c= the topology of Y
proof
let x be object;
assume x in J;
then consider A being Subset of proj2 rng g such that
A18: x = union A and
A is finite;
A19: A c= the topology of Y by A16;
then A is Subset-Family of Y by XBOOLE_1:1;
hence thesis by A18,A19,PRE_TOPC:def 1;
end;
{}proj2 rng g in J by ZFMISC_1:2;
then reconsider
J as non empty Subset of InclPoset the topology of Y by A17,YELLOW_1:1;
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
A20: a = union A and
A21: A is finite;
assume b in J;
then consider B being Subset of proj2 rng g such that
A22: b = union B and
A23: B is finite;
reconsider AB = A \/ B as finite Subset of proj2 rng g by A21,A23;
take ab = a"\/"b;
A24: a \/ b = ab by WAYBEL14:18;
union AB = a \/ b by A20,A22,ZFMISC_1:78;
hence ab in J by A24;
a c= ab & b c= ab by A24,XBOOLE_1:7;
hence thesis by YELLOW_1:3;
end;
then reconsider J9 = J as non empty directed Subset of S by A1,
WAYBEL_0:3;
A25: proj2 rng g c= bool (f.x)
proof
let z be object;
reconsider zz=z as set by TARSKI:1;
assume z in proj2 rng g;
then consider z1 being object such that
A26: [z1,z] in rng g by XTUPLE_0:def 13;
A27: [z1,z]`1 = z1;
reconsider zz1=z1 as set by TARSKI:1;
A28: ex a being object st a in dom g & [z1,z] = g.a by A26,FUNCT_1:def 3;
then
A29: x in zz1 by A14,A15,A27;
[z1,z]`2 = z;
then
A30: [:zz1,zz:] c= *graph f by A14,A15,A28,A27;
zz c= f.x
proof
let a be object;
assume a in zz;
then [x,a] in [:zz1,zz:] by A29,ZFMISC_1:87;
hence thesis by A30,Th38;
end;
hence thesis;
end;
union J = f.y
proof
thus union J c= f.y
proof
let a be object;
assume a in union J;
then consider u being set such that
A31: a in u and
A32: u in J by TARSKI:def 4;
consider A being Subset of proj2 rng g such that
A33: u = union A and
A is finite by A32;
A c= bool (f.y) by A25;
then u c= union bool (f.y) by A33,ZFMISC_1:77;
then u c= f.y by ZFMISC_1:81;
hence thesis by A31;
end;
let a be object;
assume
A34: a in f.y;
then
A35: g.a in rng g by A14,FUNCT_1:def 3;
then g.a = [(g.a)`1, (g.a)`2] by A14,MCART_1:21;
then (g.a)`2 in proj2 rng g by A35,XTUPLE_0:def 13;
then reconsider A = {(g.a)`2} as Subset of proj2 rng g by ZFMISC_1:31
;
union A = (g.a)`2 by ZFMISC_1:25;
then
A36: (g.a)`2 in J;
a in (g.a)`2 by A15,A34;
hence thesis by A36,TARSKI:def 4;
end;
then sup J = f.y by YELLOW_1:22;
then
A37: sup J9 = f.y by A1,YELLOW_0:17,26;
f.y in the topology of Y by A5,A1;
then reconsider W = f.y as open Subset of Y by PRE_TOPC:def 2;
A38: proj1 rng g c= the topology of X by A14,FUNCT_5:11;
defpred P[object,object] means
ex c1,d being set st d = $1 & [c1,$1] = g.$2 & x in c1 &
$2 in d & $2 in f.x & [:c1,d:] c= *graph f;
f.x in P by A8,FUNCT_2:38;
then J meets P by A7,A37,WAYBEL11:def 1;
then consider a being object such that
A39: a in J and
A40: a in P by XBOOLE_0:3;
reconsider a as Element of S by A40;
consider A being Subset of proj2 rng g such that
A41: a = union A and
A42: A is finite by A39;
A43: now
let c be object;
assume c in A;
then consider c1 being object such that
A44: [c1,c] in rng g by XTUPLE_0:def 13;
reconsider cc1=c1 as set by TARSKI:1;
consider a being object such that
A45: a in dom g and
A46: [c1,c] = g.a by A44,FUNCT_1:def 3;
reconsider cc = c as set by TARSKI:1;
reconsider a as object;
take a;
thus a in W by A14,A45;
A47: [c1,c]`1 = c1;
then
A48: x in cc1 by A14,A15,A45,A46;
A49: [c1,c]`2 = c;
then [:cc1,cc:] c= *graph f by A14,A15,A45,A46,A47;
hence P[c,a] by A14,A15,A45,A46,A49,A48;
end;
consider hh being Function such that
A50: dom hh = A & rng hh c= W and
A51: for c being object st c in A holds P[c,hh.c] from FUNCT_1:sch 6(A43);
set B = proj1 (g.:rng hh);
g.:rng hh c= rng g by RELAT_1:111;
then B c= proj1 rng g by XTUPLE_0:8;
then
A52: B c= the topology of X by A38;
then reconsider B as Subset-Family of X by XBOOLE_1:1;
reconsider B as Subset-Family of X;
reconsider Q = Intersect B as Subset of X;
take Q;
g.:rng hh is finite by A42,A50,FINSET_1:5,8;
then B is finite by Th39;
then Q in FinMeetCl the topology of X by A52,CANTOR_1:def 3;
then Q in the topology of X by CANTOR_1:5;
hence Q is open by PRE_TOPC:def 2;
thus Q c= f"P
proof
let z be object;
assume
A53: 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 A1;
a c= f.zz
proof
let p be object;
assume p in a;
then consider q being set such that
A54: p in q and
A55: q in A by A41,TARSKI:def 4;
P[q,hh.q] by A51,A55;
then consider q1,d being set such that
A56: d = q and
A57: [q1,q] = g.(hh.q) and
A58: hh.q in f.x and
A59: [:q1,d:] c= *graph f;
hh.q in rng hh by A50,A55,FUNCT_1:def 3;
then [q1,q] in g.:rng hh by A14,A57,A58,FUNCT_1:def 6;
then q1 in B by XTUPLE_0:def 12;
then zz in q1 by A53,SETFAM_1:43;
then [zz,p] in [:q1,q:] by A54,ZFMISC_1:87;
hence thesis by A59,Th38,A56;
end;
then aa <= fz by YELLOW_1:3;
then a <= f.zz by A1,YELLOW_0:1;
then f.zz in P by A7,A40,WAYBEL_0:def 20;
hence thesis by FUNCT_2:38;
end;
now
let c1 be set;
assume c1 in B;
then consider c being object such that
A60: [c1,c] in g.:rng hh by XTUPLE_0:def 12;
consider b being object such that
b in dom g and
A61: b in rng hh and
A62: [c1,c] = g.b by A60,FUNCT_1:def 6;
consider c9 being object such that
A63: c9 in dom hh and
A64: b = hh.c9 by A61,FUNCT_1:def 3;
ex c91,d being set
st d =c9 & [c91,c9] = g.(hh.c9) & x in c91 & hh.c9 in
d & hh.c9 in f.x & [:c91,d:] c= *graph f by A50,A51,A63;
hence x in c1 by A62,A64,XTUPLE_0:1;
end;
hence x in Q by A8,SETFAM_1:43;
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:25;
end;
[#]S <> {};
hence thesis by A6,TOPS_2:43;
end;
definition
let W be Relation, X be set;
func (W,X)*graph -> Function means
: Def5:
dom it = X & for x being object st x in X holds it.x = Im(W,x);
existence
proof
deffunc F(object) = Im(W,$1);
thus ex f being Function st dom f = X &
for x being object st x in X holds f.x = F(x)
from FUNCT_1:sch 3;
end;
correctness
proof
let f,g be Function such that
A1: dom f = X and
A2: for x being object st x in X holds f.x = Im(W,x) and
A3: dom g = X and
A4: for x being object st x in X holds g.x = Im(W,x);
now
let x be object;
assume
A5: x in X;
hence f.x = Im(W,x) by A2
.= g.x by A4,A5;
end;
hence thesis by A1,A3,FUNCT_1:2;
end;
end;
theorem Th41:
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 object;
hereby
assume [x,y] in *graph((W,X)*graph);
then x in X & y in ((W,X)*graph).x by A2,Th38;
then y in Im(W,x) by Def5;
then ex z being object st [z,y] in W & z in {x} by RELAT_1:def 13;
hence [x,y] in W by TARSKI:def 1;
end;
assume
A3: [x,y] in W;
then
A4: x in dom W by XTUPLE_0:def 12;
x in {x} by TARSKI:def 1;
then y in Im(W,x) by A3,RELAT_1:def 13;
then y in ((W,X)*graph).x by A1,A4,Def5;
hence [x,y] in *graph((W,X)*graph) by A1,A2,A4,Th38;
end;
hence thesis;
end;
registration
let X, Y be TopSpace;
cluster -> Relation-like for 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 2;
hence thesis;
end;
cluster -> Relation-like for Element of the topology of [:X,Y:];
coherence;
end;
theorem Th42:
for X,Y being non empty TopSpace for W being open Subset of [:X,
Y:] for x being Point of X holds Im(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;
reconsider W as Relation of the carrier of X, the carrier of Y by
BORSUK_1:def 2;
reconsider A = W.:{x} as Subset of Y;
now
let y be set;
hereby
assume y in A;
then consider z being object such that
A1: [z,y] in W and
A2: z in {x} by RELAT_1:def 13;
consider AA being Subset-Family of [:X,Y:] such that
A3: W = union AA and
A4: 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:5;
z = x by A2,TARSKI:def 1;
then consider e being set such that
A5: [x,y] in e and
A6: e in AA by A1,A3,TARSKI:def 4;
consider X1 being Subset of X, Y1 being Subset of Y such that
A7: e = [:X1,Y1:] and
X1 is open and
A8: Y1 is open by A4,A6;
take Y1;
thus Y1 is open by A8;
A9: x in X1 by A5,A7,ZFMISC_1:87;
thus Y1 c= A
proof
let z be object;
assume z in Y1;
then [x,z] in e by A7,A9,ZFMISC_1:87;
then
A10: [x,z] in W by A3,A6,TARSKI:def 4;
x in {x} by TARSKI:def 1;
hence thesis by A10,RELAT_1:def 13;
end;
thus y in Y1 by A5,A7,ZFMISC_1:87;
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:25;
end;
:: 4.9. PROPOSITION a) p.130.
theorem Th43:
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 Function 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;
reconsider W as Relation of the carrier of X, the carrier of Y by
BORSUK_1:def 2;
A1: dom f = the carrier of X by Def5;
A2: the carrier of InclPoset the topology of Y = the topology of Y & the
RelStr of S = the RelStr of InclPoset the topology of Y by YELLOW_1:1
,YELLOW_9:def 4;
rng f c= the carrier of S
proof
let y be object;
assume y in rng f;
then consider x being object such that
A3: x in dom f and
A4: y = f.x by FUNCT_1:def 3;
reconsider x as Element of X by A3,Def5;
y = Im(W,x) by A4,Def5;
then y is open Subset of Y by Th42;
hence thesis by A2,PRE_TOPC:def 2;
end;
then reconsider f as Function of X,S by A1,FUNCT_2:2;
dom W c= the carrier of X;
then *graph f = W by Th41;
hence thesis by Th40;
end;
:: 4.9. PROPOSITION b) p.130.
theorem Th44:
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;
reconsider g1 = f1, g2 = f2 as continuous Function of X, Omega S by Th1;
S is TopAugmentation of S by YELLOW_9:44;
then
A3: the RelStr of S = the RelStr of Omega S by WAYBEL25:16;
A4: the RelStr of S = the RelStr of InclPoset the topology of Y by
YELLOW_9:def 4;
now
let j be set;
assume j in the carrier of X;
then reconsider x = j as Element of X;
reconsider g1x = g1.x, g2x = g2.x as Element of InclPoset the topology of
Y by A3,YELLOW_9:def 4;
take a = g1.x, b = g2.x;
thus a = g1.j & b = g2.j;
g1.x = Im(W1,x) & g2.x = Im(W2,x) by A2,Def5;
then g1.x c= g2.x by A1,RELAT_1:124;
then g1x <= g2x by YELLOW_1:3;
hence a <= b by A4,A3,YELLOW_0:1;
end;
then g1 <= g2;
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 Function 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
PBOOLE:sch 5;
A2: rng F c= the carrier of oContMaps(X, S)
proof
let y be object;
assume y in rng F;
then consider x being object such that
A3: x in dom F and
A4: y = F.x by FUNCT_1:def 3;
reconsider x as Element of the topology of [:X,Y:] by A3;
A5: x is open Subset of [:X,Y:] by PRE_TOPC:def 2;
y = (x, the carrier of X)*graph by A1,A4;
then y is continuous Function of X,S by A5,Th43;
then y is Element of oContMaps(X, S) by Th2;
hence thesis;
end;
A6: dom F = the topology of [:X,Y:] by PARTFUN1:def 2;
A7: the carrier of InclPoset the topology of [:X,Y:] = the topology of [:X,Y
:] by YELLOW_1:1;
then reconsider
F as Function of InclPoset the topology of [:X, Y:], oContMaps(X,
S) by A6,A2,FUNCT_2:2;
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 A7;
then reconsider W1 = x, W2 = y as open Subset of [:X,Y:] by PRE_TOPC:def 2;
assume x <= y;
then
A8: W1 c= W2 by YELLOW_1:3;
F.x = (W1, the carrier of X)*graph & F.y = (W2, the carrier of X)
*graph by A1,A7;
hence thesis by A8,Th44;
end;
let W be open Subset of [:X,Y:];
W in the topology of [:X,Y:] by PRE_TOPC:def 2;
hence thesis by A1;
end;