Copyright (c) 1999 Association of Mizar Users
environ
vocabulary RELAT_1, SEQ_1, ORDERS_1, YELLOW_0, FUNCT_1, CAT_1, RELAT_2,
WAYBEL_0, SEQM_3, PRE_TOPC, FUNCOP_1, QUANTAL1, ORDINAL2, BINOP_1, BOOLE,
GROUP_6, LATTICES, FUNCT_3, BORSUK_1, WAYBEL_1, WELLORD1, BHSP_3,
YELLOW_1, WAYBEL_3, GROUP_1, CARD_3, PBOOLE, LATTICE3, FUNCT_4, RLVECT_2,
SUBSET_1, WAYBEL18, YELLOW_9, T_0TOPSP, TOPS_2, YELLOW16;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, FUNCT_3, FUNCT_7, STRUCT_0, CARD_3, ZF_FUND1, PBOOLE,
PRALG_1, PRE_CIRC, FUNCT_4, WELLORD1, ORDERS_1, LATTICE3, GRCAT_1,
PRE_TOPC, TOPS_2, T_0TOPSP, BORSUK_1, QUANTAL1, YELLOW_0, WAYBEL_0,
YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_9, WAYBEL_3, WAYBEL18;
constructors PRE_CIRC, FUNCT_7, ENUMSET1, ORDERS_3, WAYBEL_1, T_0TOPSP,
ZF_FUND1, QUANTAL1, GRCAT_1, TOPS_2, YELLOW_9, NATTRA_1, TOLER_1,
WAYBEL18, BORSUK_1;
clusters STRUCT_0, WAYBEL_0, WAYBEL_3, RELSET_1, YELLOW_1, LATTICE3, BORSUK_2,
WAYBEL10, WAYBEL17, YELLOW_0, FUNCT_1, SUBSET_1, PRE_TOPC, TOPS_1,
YELLOW_2, WAYBEL18, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, RELAT_1, LATTICE3, YELLOW_0, BORSUK_1, WAYBEL_0, YELLOW_1,
YELLOW_2, WAYBEL_1, WAYBEL_3, T_0TOPSP, WAYBEL25, XBOOLE_0;
theorems STRUCT_0, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, PRE_TOPC,
BORSUK_1, TOPMETR, ORDERS_1, YELLOW12, ZF_FUND1, RELAT_1, FUNCT_2,
FUNCT_1, ENUMSET1, WAYBEL_3, PBOOLE, FUNCOP_1, LATTICE3, CARD_3, TARSKI,
ZFMISC_1, WELLORD1, GRCAT_1, QUANTAL1, FUNCT_4, YELLOW_9, WAYBEL20,
FUNCT_7, TOPS_2, FUNCT_3, WAYBEL10, T_0TOPSP, WAYBEL15, YELLOW_6,
PRALG_1, WAYBEL18, WAYBEL13, WAYBEL21, XBOOLE_0, XBOOLE_1, AMI_1;
schemes PRALG_2;
begin :: Poset retracts
theorem
for a,b being Relation holds a*b = a(#)b
proof let a,b be Relation;
thus a*b c= a(#)b
proof let x be set; assume
A1: x in a*b;
then consider x1,x2 being set such that
A2: x = [x1,x2] by RELAT_1:def 1;
ex y being set st [x1,y] in a & [y,x2] in b by A1,A2,RELAT_1:def 8;
hence thesis by A2,ZF_FUND1:def 1;
end;
let x be set; assume x in a(#)b;
then ex u,v,w being set st x = [u,w] & [u,v] in a & [v,w] in
b by ZF_FUND1:def 1;
hence thesis by RELAT_1:def 8;
end;
theorem
for X being set, L being non empty RelStr, S being non empty SubRelStr of L
for f,g being Function of X, the carrier of S
for f',g' being Function of X, the carrier of L
st f' = f & g' = g & f <= g
holds f' <= g'
proof let X be set, L be non empty RelStr, S be non empty SubRelStr of L;
let f,g be Function of X, the carrier of S;
let f',g' be Function of X, the carrier of L such that
A1: f' = f & g' = g & f <= g;
let x be set; assume
A2: x in X;
then f.x in the carrier of S & g.x in the carrier of S by FUNCT_2:7;
then reconsider a = f.x, b = g.x as Element of S;
reconsider a' = a, b' = b as Element of L by YELLOW_0:59;
take a', b'; thus a' = f'.x & b' = g'.x by A1;
ex a,b being Element of S st a = f.x & b = g.x & a <= b
by A1,A2,YELLOW_2:def 1;
hence thesis by YELLOW_0:60;
end;
theorem
for X being set, L being non empty RelStr
for S being full non empty SubRelStr of L
for f,g being Function of X, the carrier of S
for f',g' being Function of X, the carrier of L
st f' = f & g' = g & f' <= g'
holds f <= g
proof let X be set, L be non empty RelStr;
let S be full non empty SubRelStr of L;
let f,g be Function of X, the carrier of S;
let f',g' be Function of X, the carrier of L such that
A1: f' = f & g' = g & f' <= g';
let x be set; assume
A2: x in X;
then f.x in the carrier of S & g.x in the carrier of S by FUNCT_2:7;
then reconsider a = f.x, b = g.x as Element of S;
take a, b; thus a = f.x & b = g.x;
ex a',b' being Element of L st a' = a & b' = b & a' <= b'
by A1,A2,YELLOW_2:def 1;
hence thesis by YELLOW_0:61;
end;
definition
let S be non empty RelStr;
let T be non empty reflexive antisymmetric RelStr;
cluster directed-sups-preserving monotone map of S,T;
existence
proof consider x being Element of T;
take f = S --> x;
A1: f = (the carrier of S) --> x by BORSUK_1:def 3;
thus f is directed-sups-preserving
proof let X be Subset of S; assume
A2: X is non empty directed;
A3: f.:X = {x}
proof thus f.:X c= {x} by A1,BORSUK_1:6;
consider a being Element of X;
A4: a in X by A2;
then f.a = x & dom f = the carrier of S by A1,FUNCOP_1:13,19;
then x in f.:X by A4,FUNCT_1:def 12;
hence thesis by ZFMISC_1:37;
end;
assume ex_sup_of X,S;
thus ex_sup_of f.:X, T by A3,YELLOW_0:38;
thus sup (f.:X) = x by A3,YELLOW_0:39 .= f.sup X by A1,FUNCOP_1:13;
end;
let a,b be Element of S;
f.a = x & f.b = x & x <= x by A1,FUNCOP_1:13;
hence thesis;
end;
end;
theorem
for f,g being Function st f is idempotent & rng g c= rng f & rng g c= dom f
holds f*g = g
proof let f,g be Function; assume f is idempotent;
then A1: f*f = f by QUANTAL1:def 9;
assume
A2: rng g c= rng f;
assume
rng g c= dom f;
then A3: dom (f*g) = dom g by RELAT_1:46;
now let x be set; assume x in dom g;
then A4: (f*g).x = f.(g.x) & g.x in rng g by FUNCT_1:23,def 5;
then consider a being set such that
A5: a in dom f & g.x = f.a by A2,FUNCT_1:def 5;
thus (f*g).x = g.x by A1,A4,A5,FUNCT_1:23;
end;
hence f*g = g by A3,FUNCT_1:9;
end;
definition
let S be 1-sorted;
cluster idempotent map of S,S;
existence
proof take f = id S;
A1: the carrier of S = {} implies the carrier of S = {};
f = id the carrier of S by GRCAT_1:def 11;
then f*f = f by A1,FUNCT_2:23;
hence thesis by QUANTAL1:def 9;
end;
end;
theorem Th5:
for L being up-complete (non empty Poset)
for S being directed-sups-inheriting full (non empty SubRelStr of L)
holds S is up-complete
proof let L be up-complete (non empty Poset);
let S be directed-sups-inheriting full (non empty SubRelStr of L);
now let X be non empty directed Subset of S;
reconsider Y = X as non empty directed Subset of L by YELLOW_2:7;
ex_sup_of Y,L by WAYBEL_0:75;
hence ex_sup_of X,S by WAYBEL_0:7;
end;
hence S is up-complete by WAYBEL_0:75;
end;
theorem Th6:
for L being up-complete (non empty Poset)
for f being map of L, L st f is idempotent directed-sups-preserving
holds Image f is directed-sups-inheriting
proof let L be up-complete (non empty Poset);
let f be map of L, L;
assume
A1: f is idempotent directed-sups-preserving;
set S = subrelstr(rng f);
consider a being Element of L;
dom f = the carrier of L by FUNCT_2:def 1;
then f.a in rng f by FUNCT_1:def 5;
then the carrier of S is non empty by YELLOW_0:def 15;
then reconsider S' = S as non empty full SubRelStr of L by STRUCT_0:def 1;
S is directed-sups-inheriting
proof
let X be directed Subset of S;
assume X <> {};
then X is non empty directed Subset of S';
then reconsider X'= X as non empty directed Subset of L by YELLOW_2:7;
A2: f preserves_sup_of X' by A1,WAYBEL_0:def 37;
assume ex_sup_of X,L;
then A3: ex_sup_of f.:X',L & sup(f.:X') = f.sup X' by A2,WAYBEL_0:def 31;
X c= the carrier of S;
then X c= rng f by YELLOW_0:def 15;
then sup X' = f.sup X' & the carrier of L <> {} by A1,A3,YELLOW_2:22;
then "\/"(X, L) in rng f by FUNCT_2:6;
hence "\/"(X, L) in the carrier of S by YELLOW_0:def 15;
end;
hence Image f is directed-sups-inheriting by YELLOW_2:def 2;
end;
canceled;
theorem Th8:
for S, T being non empty RelStr, f being map of T,S, g being map of S,T holds
f*g = id S implies rng f = the carrier of S
proof let S,T be non empty RelStr;
let f be map of T,S, g be map of S,T such that
A1: f*g = id S;
id S = id the carrier of S & the carrier of T <> {} by GRCAT_1:def 11;
hence rng f = the carrier of S by A1,FUNCT_2:29;
end;
theorem Th9:
for T being non empty RelStr, S being non empty SubRelStr of T
for f being map of T,S holds
f*incl(S,T) = id S implies f is idempotent map of T, T
proof let T be non empty RelStr, S be non empty SubRelStr of T;
let f be map of T,S; assume
A1: f*incl(S, T) = id S;
then A2: rng f = the carrier of S by Th8;
A3: the carrier of S c= the carrier of T by YELLOW_0:def 13;
then incl(S, T) = id the carrier of S by YELLOW_9:def 1;
then incl(S, T)*f = f by FUNCT_2:23;
then A4: f*f = (id S)*f by A1,RELAT_1:55
.= (id the carrier of S)*f by GRCAT_1:def 11
.= f by FUNCT_2:23;
dom f = the carrier of T by FUNCT_2:def 1;
then f is Function of the carrier of T, the carrier of T by A2,A3,FUNCT_2:4
;
hence thesis by A4,QUANTAL1:def 9;
end;
definition
let S,T be non empty Poset;
let f be Function;
pred f is_a_retraction_of T,S means:Def1:
f is directed-sups-preserving map of T,S & f|the carrier of S = id S &
S is directed-sups-inheriting full SubRelStr of T;
pred f is_an_UPS_retraction_of T,S means:Def2:
f is directed-sups-preserving map of T,S &
ex g being directed-sups-preserving map of S,T st f*g = id S;
end;
definition
let S,T be non empty Poset;
pred S is_a_retract_of T means:Def3:
ex f being map of T,S st f is_a_retraction_of T,S;
pred S is_an_UPS_retract_of T means:Def4:
ex f being map of T,S st f is_an_UPS_retraction_of T,S;
end;
theorem Th10:
for S,T being non empty Poset, f being Function
st f is_a_retraction_of T,S
holds f*incl(S,T) = id S
proof let S,T be non empty Poset, f be Function such that
f is directed-sups-preserving map of T,S and
A1: f|the carrier of S = id S and
A2: S is directed-sups-inheriting full SubRelStr of T;
the carrier of S c= the carrier of T by A2,YELLOW_0:def 13;
hence f*incl(S, T) = f*id the carrier of S by YELLOW_9:def 1
.= id S by A1,RELAT_1:94;
end;
theorem Th11:
for S being non empty Poset, T being up-complete (non empty Poset)
for f being Function
st f is_a_retraction_of T,S
holds f is_an_UPS_retraction_of T,S
proof let S be non empty Poset;
let T be up-complete (non empty Poset), f be Function; assume
A1: f is_a_retraction_of T,S;
hence f is directed-sups-preserving map of T,S by Def1;
S is directed-sups-inheriting full SubRelStr of T by A1,Def1;
then reconsider g = incl(S,T) as directed-sups-preserving map of S,T
by WAYBEL21:10;
take g; thus f*g = id S by A1,Th10;
end;
theorem Th12:
for S,T being non empty Poset, f being Function
st f is_a_retraction_of T,S
holds rng f = the carrier of S
proof let S,T be non empty Poset, f be Function; assume
f is_a_retraction_of T,S;
then f*incl(S,T) = id S & f is map of T,S by Def1,Th10;
hence thesis by Th8;
end;
theorem Th13:
for S,T being non empty Poset, f being Function
st f is_an_UPS_retraction_of T,S
holds rng f = the carrier of S
proof let S,T be non empty Poset, f be Function; assume
f is directed-sups-preserving map of T,S &
ex g being directed-sups-preserving map of S,T st f*g = id S;
hence thesis by Th8;
end;
theorem Th14:
for S,T being non empty Poset, f being Function
st f is_a_retraction_of T,S
holds f is idempotent map of T,T
proof let S,T be non empty Poset, f be Function; assume
f is_a_retraction_of T,S;
then f*incl(S,T) = id S & f is map of T,S & S is SubRelStr of T by Def1,
Th10;
hence thesis by Th9;
end;
theorem Th15:
for T,S being non empty Poset, f being map of T,T
st f is_a_retraction_of T,S
holds Image f = the RelStr of S
proof let T,S be non empty Poset, f be map of T,T; assume
f is_a_retraction_of T,S;
then A1: rng f = the carrier of S & S is full SubRelStr of T by Def1,Th12;
Image f = subrelstr rng f by YELLOW_2:def 2;
then the carrier of Image f = rng f by YELLOW_0:def 15;
hence thesis by A1,YELLOW_0:58;
end;
theorem Th16:
for T being up-complete (non empty Poset)
for S being non empty Poset, f being map of T,T
st f is_a_retraction_of T,S
holds f is directed-sups-preserving projection
proof let T be up-complete (non empty Poset);
let S be non empty Poset, f be map of T,T; assume
A1: f is_a_retraction_of T,S;
then reconsider g = f as directed-sups-preserving map of T,S by Def1;
A2: f is_an_UPS_retraction_of T,S by A1,Th11;
f is idempotent by A1,Th14;
then A3: f = f*f by QUANTAL1:def 9 .= (f|rng f)*f by FUNCT_4:2
.= (f|the carrier of S)*f by A2,Th13 .= (id S)*f by A1,Def1
.= (id the carrier of S)*g by GRCAT_1:def 11;
A4: S is full directed-sups-inheriting non empty SubRelStr of T
by A1,Def1;
then A5: incl(S,T) is directed-sups-preserving by WAYBEL21:10;
the carrier of S c= the carrier of T by A4,YELLOW_0:def 13;
then A6: incl(S,T) = id the carrier of S by YELLOW_9:def 1;
hence f is directed-sups-preserving by A3,A5,WAYBEL20:29;
f is directed-sups-preserving idempotent map of T,T by A1,A3,A5,A6,Th14,
WAYBEL20:29;
hence thesis by WAYBEL_1:def 13;
end;
theorem Th17:
for S,T being non empty reflexive transitive RelStr
for f being map of S,T holds
f is isomorphic iff f is monotone &
ex g being monotone map of T,S st f*g = id T & g*f = id S
proof let S,T be non empty reflexive transitive RelStr, f be map of S,T;
A1: id S = id the carrier of S & id T = id the carrier of T by GRCAT_1:def 11;
hereby assume
A2: f is isomorphic;
hence f is monotone by WAYBEL_0:def 38;
consider g being map of T,S such that
A3: g = f qua Function" & g is monotone by A2,WAYBEL_0:def 38;
reconsider g as monotone map of T,S by A3;
take g;
f is one-to-one & rng f = the carrier of T
by A2,WAYBEL_0:66;
hence f*g = id T & g*f = id S by A1,A3,FUNCT_2:35;
end;
assume
A4: f is monotone;
given g being monotone map of T,S such that
A5: f*g = id T & g*f = id S;
A6: f is one-to-one & rng f = the carrier of T by A1,A5,FUNCT_2:29;
then g = f qua Function" by A1,A5,FUNCT_2:36;
hence f is isomorphic by A4,A6,WAYBEL_0:def 38;
end;
theorem Th18:
for S,T being non empty Poset holds
S,T are_isomorphic iff
ex f being monotone map of S,T, g being monotone map of T,S
st f*g = id T & g*f = id S
proof let S,T be non empty Poset;
A1: id S = id the carrier of S & id T = id the carrier of T by GRCAT_1:def 11;
hereby assume S,T are_isomorphic;
then consider f being map of S,T such that
A2: f is isomorphic by WAYBEL_1:def 8;
reconsider f as monotone map of S,T by A2,WAYBEL_0:def 38;
take f;
consider g being map of T,S such that
A3: g = f qua Function" & g is monotone by A2,WAYBEL_0:def 38;
reconsider g as monotone map of T,S by A3;
take g;
f is one-to-one & rng f = the carrier of T
by A2,WAYBEL_0:66;
hence f*g = id T & g*f = id S by A1,A3,FUNCT_2:35;
end;
given f being monotone map of S,T, g being monotone map of T,S such that
A4: f*g = id T & g*f = id S;
take f;
A5: f is one-to-one & rng f = the carrier of T by A1,A4,FUNCT_2:29;
then g = f qua Function" by A1,A4,FUNCT_2:36;
hence f is isomorphic by A5,WAYBEL_0:def 38;
end;
theorem
for S,T being up-complete (non empty Poset)
st S,T are_isomorphic
holds S is_an_UPS_retract_of T & T is_an_UPS_retract_of S
proof let S,T be up-complete (non empty Poset);
assume S,T are_isomorphic;
then consider f be monotone map of S,T, g be monotone map of T,S such that
A1: f*g = id T & g*f = id S by Th18;
f is isomorphic & g is isomorphic by A1,Th17;
then f is sups-preserving & g is sups-preserving by WAYBEL13:20;
then (for X being Subset of S st X is non empty directed
holds f preserves_sup_of X) &
for X being Subset of T st X is non empty directed
holds g preserves_sup_of X by WAYBEL_0:def 33;
then f is directed-sups-preserving & g is directed-sups-preserving
by WAYBEL_0:def 37;
then g is_an_UPS_retraction_of T,S &
f is_an_UPS_retraction_of S,T by A1,Def2;
hence thesis by Def4;
end;
theorem Th20:
for T,S being non empty Poset
for f being monotone map of T,S, g being monotone map of S,T
st f*g = id S
ex h being projection map of T,T
st h = g*f &
h|the carrier of Image h = id Image h &
S, Image h are_isomorphic
proof let T,S be non empty Poset;
let f be monotone map of T,S, g be monotone map of S,T such that
A1: f*g = id S;
set h = g*f;
A2: id S = id the carrier of S by GRCAT_1:def 11;
h*h = h*g*f by RELAT_1:55 .= g*(id S)*f by A1,RELAT_1:55
.= h by A2,FUNCT_2:23;
then h is idempotent monotone map of T,T by QUANTAL1:def 9,YELLOW_2:14;
then reconsider h as projection map of T,T by WAYBEL_1:def 13;
take h; thus h = g*f;
id the carrier of Image h = id Image h by GRCAT_1:def 11;
hence h|the carrier of Image h = h*id Image h by RELAT_1:94
.= h*(inclusion h) by WAYBEL_1:def 17
.= (corestr h)*(inclusion h) by WAYBEL_1:32
.= id Image h by WAYBEL_1:36;
rng f = the carrier of S & dom g = the carrier of S
by A1,Th8,FUNCT_2:def 1;
then A4: rng h = rng g by RELAT_1:47;
A5: Image h = subrelstr rng h & Image g = subrelstr rng g
by YELLOW_2:def 2;
then reconsider gg = corestr g as map of S, Image h by A4;
take gg;
A6: gg = g by WAYBEL_1:32;
then A7: gg is one-to-one by A1,A2,FUNCT_2:29;
A8: rng gg = the carrier of Image h by A4,A5,A6,YELLOW_0:def 15;
now let x,y be Element of S;
x <= y implies g.x <= g.y & gg.x in the carrier of Image h
by WAYBEL_1:def 2;
hence x <= y implies gg.x <= gg.y by A6,YELLOW_0:61;
assume gg.x <= gg.y;
then A9: g.x <= g.y by A6,YELLOW_0:60;
(id S).x = x & (id S).y = y by GRCAT_1:11;
then x = f.(g.x) & y = f.(g.y) by A1,FUNCT_2:21;
hence x <= y by A9,WAYBEL_1:def 2;
end;
hence gg is isomorphic by A7,A8,WAYBEL_0:66;
end;
theorem Th21:
for T being up-complete (non empty Poset), S being non empty Poset
for f being Function st f is_an_UPS_retraction_of T,S
ex h being directed-sups-preserving projection map of T,T
st h is_a_retraction_of T, Image h & S, Image h are_isomorphic
proof let T be up-complete (non empty Poset);
let S be non empty Poset, f be Function such that
A1: f is directed-sups-preserving map of T,S;
given g being directed-sups-preserving map of S,T such that
A2: f*g = id S;
reconsider f as directed-sups-preserving map of T,S by A1;
consider h being projection map of T,T such that
A3: h = g*f and
A4: h|the carrier of Image h = id Image h and
A5: S, Image h are_isomorphic by A2,Th20;
reconsider h as directed-sups-preserving projection map of T,T
by A3,WAYBEL20:29;
take h;
reconsider R = Image h as non empty Poset;
h = corestr h by WAYBEL_1:32;
then A6: h is directed-sups-preserving map of T, R by WAYBEL20:22;
R is directed-sups-inheriting full SubRelStr of T by Th6;
hence h is_a_retraction_of T, Image h by A4,A6,Def1;
thus thesis by A5;
end;
theorem Th22:
for L being up-complete (non empty Poset)
for S being non empty Poset st S is_a_retract_of L
holds S is up-complete
proof let L be up-complete (non empty Poset);
let S be non empty Poset;
given f being map of L,S such that
A1: f is_a_retraction_of L,S;
S is full directed-sups-inheriting (non empty SubRelStr of L) by A1,Def1;
hence thesis by Th5;
end;
theorem Th23:
for L being complete (non empty Poset)
for S being non empty Poset st S is_a_retract_of L
holds S is complete
proof let L be complete (non empty Poset);
let S be non empty Poset;
given f being map of L, S such that
A1: f is_a_retraction_of L,S;
reconsider f as directed-sups-preserving projection map of L,L
by A1,Th14,Th16;
the RelStr of S = Image f & Image f is complete by A1,Th15,YELLOW_2:37;
hence thesis by YELLOW_0:3;
end;
theorem Th24:
for L being continuous complete LATTICE
for S being non empty Poset st S is_a_retract_of L
holds S is continuous
proof let L be continuous complete LATTICE;
let S be non empty Poset; given f being map of L,S such that
A1: f is_a_retraction_of L,S;
reconsider g = f as directed-sups-preserving projection map of L,L
by A1,Th14,Th16;
A2: Image g is continuous LATTICE by WAYBEL15:17;
Image g = the RelStr of S by A1,Th15;
hence S is continuous by A2,YELLOW12:15;
end;
theorem
for L being up-complete (non empty Poset)
for S being non empty Poset st S is_an_UPS_retract_of L
holds S is up-complete
proof let L be up-complete (non empty Poset);
let S be non empty Poset;
given f being map of L,S such that
A1: f is_an_UPS_retraction_of L,S;
consider h being directed-sups-preserving projection map of L,L such that
A2: h is_a_retraction_of L, Image h & S, Image h are_isomorphic by A1,Th21;
h = corestr h by WAYBEL_1:32;
then Image h is_a_retract_of L by A2,Def3;
then Image h is up-complete & Image h, S are_isomorphic by A2,Th22,WAYBEL_1
:7;
hence thesis by WAYBEL13:30;
end;
theorem
for L being complete (non empty Poset)
for S being non empty Poset st S is_an_UPS_retract_of L
holds S is complete
proof let L be complete (non empty Poset), S be non empty Poset;
given f being map of L, S such that
A1: f is_an_UPS_retraction_of L,S;
consider h being directed-sups-preserving projection map of L,L such that
A2: h is_a_retraction_of L, Image h & S, Image h are_isomorphic by A1,Th21;
h = corestr h by WAYBEL_1:32;
then Image h is_a_retract_of L by A2,Def3;
then Image h is complete & Image h, S are_isomorphic by A2,Th23,WAYBEL_1:7
;
hence thesis by WAYBEL20:18;
end;
theorem
for L being continuous complete LATTICE
for S being non empty Poset st S is_an_UPS_retract_of L
holds S is continuous
proof let L be continuous complete LATTICE;
let S be non empty Poset; given f being map of L,S such that
A1: f is_an_UPS_retraction_of L,S;
consider h being directed-sups-preserving projection map of L,L such that
A2: h is_a_retraction_of L, Image h & S, Image h are_isomorphic by A1,Th21;
h = corestr h by WAYBEL_1:32;
then Image h is_a_retract_of L by A2,Def3;
then Image h is continuous & Image h, S are_isomorphic by A2,Th24,WAYBEL_1:
7;
hence thesis by WAYBEL15:11;
end;
theorem Th28:
for L being RelStr
for S being full SubRelStr of L
for R being SubRelStr of S
holds R is full iff R is full SubRelStr of L
proof let L be RelStr, S be full SubRelStr of L, R be SubRelStr of S;
reconsider R' = R as SubRelStr of L by YELLOW_6:16;
A1: the carrier of R c= the carrier of S by YELLOW_0:def 13;
hereby assume R is full;
then the InternalRel of R = (the InternalRel of S)|_2 the carrier of R
by YELLOW_0:def 14
.= ((the InternalRel of L)|_2 the carrier of S)|_2 the carrier of R
by YELLOW_0:def 14
.= (the InternalRel of L)|_2 the carrier of R' by A1,WELLORD1:29;
hence R is full SubRelStr of L by YELLOW_0:def 14;
end;
assume
A2: R is full SubRelStr of L;
((the InternalRel of L)|_2 the carrier of S)|_2 the carrier of R
= (the InternalRel of L)|_2 the carrier of R by A1,WELLORD1:29
.= the InternalRel of R by A2,YELLOW_0:def 14;
hence the InternalRel of R = (the InternalRel of S)|_2 the carrier of R
by YELLOW_0:def 14;
end;
theorem
for L being non empty transitive RelStr
for S being directed-sups-inheriting non empty full SubRelStr of L
for R being directed-sups-inheriting non empty SubRelStr of S
holds R is directed-sups-inheriting SubRelStr of L
proof let L be non empty transitive RelStr;
let S be directed-sups-inheriting non empty full SubRelStr of L;
let R be directed-sups-inheriting non empty SubRelStr of S;
reconsider T = R as SubRelStr of L by YELLOW_6:16;
T is directed-sups-inheriting
proof let X be directed Subset of T;
reconsider Y = X as directed Subset of S by YELLOW_2:7;
assume
A1: X <> {};
assume ex_sup_of X,L;
then sup Y = "\/"(X,L) & ex_sup_of Y, S by A1,WAYBEL_0:7;
hence "\/"(X,L) in the carrier of T by A1,WAYBEL_0:def 4;
end;
hence thesis;
end;
theorem
for L being up-complete (non empty Poset)
for S1,S2 being directed-sups-inheriting full non empty SubRelStr of L
st S1 is SubRelStr of S2
holds S1 is directed-sups-inheriting full SubRelStr of S2
proof let L be up-complete (non empty Poset);
let S1,S2 be directed-sups-inheriting full non empty SubRelStr of L;
assume S1 is SubRelStr of S2;
then reconsider S = S1 as SubRelStr of S2;
S is directed-sups-inheriting
proof let X be directed Subset of S; assume X <> {};
then reconsider Y1 = X as non empty directed Subset of S1;
reconsider Y = Y1 as non empty directed Subset of L by YELLOW_2:7;
reconsider Y2 = Y1 as non empty directed Subset of S2 by YELLOW_2:7;
ex_sup_of Y, L by WAYBEL_0:75;
then sup Y2 = sup Y & sup Y = sup Y1 by WAYBEL_0:7;
then sup Y2 in the carrier of S1;
hence thesis;
end;
hence thesis by Th28;
end;
begin :: Products
definition
let R be Relation;
attr R is Poset-yielding means:Def5:
for x being set st x in rng R holds x is Poset;
end;
definition
cluster Poset-yielding -> RelStr-yielding reflexive-yielding Relation;
coherence
proof let R be Relation; assume
A1: for x being set st x in rng R holds x is Poset;
hence for x being set st x in rng R holds x is RelStr;
thus for S being RelStr st S in rng R holds S is reflexive by A1;
end;
end;
definition
let X be non empty set;
let L be non empty RelStr;
let i be Element of X;
let Y be Subset of L|^X;
redefine func pi(Y,i) -> Subset of L;
coherence
proof
reconsider Y' = Y as Subset of product (X --> L) by YELLOW_1:def 5;
pi(Y',i) is Subset of (X --> L).i;
hence thesis by FUNCOP_1:13;
end;
end;
definition
let X be set;
let S be Poset;
cluster X --> S -> Poset-yielding;
coherence
proof
A1: rng (X --> S) c= {S} by FUNCOP_1:19;
let x be set; assume x in rng (X --> S);
hence thesis by A1,TARSKI:def 1;
end;
end;
definition
let I be set;
cluster Poset-yielding non-Empty ManySortedSet of I;
existence
proof consider P being non empty Poset;
take I --> P; thus thesis;
end;
end;
definition
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
cluster product J -> transitive antisymmetric;
coherence
proof
A1: now let i be Element of I;
dom J = I by PBOOLE:def 3;
then J.i in rng J by FUNCT_1:def 5;
hence J.i is Poset by Def5;
end;
then for i being Element of I holds J.i is transitive;
hence product J is transitive by WAYBEL_3:29;
for i being Element of I holds J.i is antisymmetric by A1;
hence thesis by WAYBEL_3:30;
end;
end;
definition
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let i be Element of I;
redefine func J.i -> non empty Poset;
coherence
proof dom J = I by PBOOLE:def 3;
then J.i in rng J by FUNCT_1:def 5;
hence thesis by Def5;
end;
end;
Lm1:
now let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J;
deffunc F(Element of I) = sup pi(X,$1);
consider f being ManySortedSet of I such that
A1: for i being Element of I holds f.i = F(i) from LambdaDMS;
A2: dom f = I by PBOOLE:def 3;
now let i be Element of I;
f.i = sup pi(X,i) by A1;
hence f.i is Element of J.i;
end;
then reconsider f as Element of product J by A2,WAYBEL_3:27;
assume
A3: for i being Element of I holds ex_sup_of pi(X,i), J.i;
take f;
thus for i being Element of I holds f.i = sup pi(X,i) by A1;
thus f is_>=_than X
proof let x be Element of product J such that
A4: x in X;
now let i be Element of I;
ex_sup_of pi(X,i), J.i & f.i = sup pi(X,i) by A1,A3;
then f.i is_>=_than pi(X,i) & x.i in pi(X,i)
by A4,CARD_3:def 6,YELLOW_0:30;
hence x.i <= f.i by LATTICE3:def 9;
end;
hence thesis by WAYBEL_3:28;
end;
let g be Element of product J; assume
A5: X is_<=_than g;
now let i be Element of I;
A6: f.i = sup pi(X,i) & ex_sup_of pi(X,i), J.i by A1,A3;
g.i is_>=_than pi(X,i)
proof let a be Element of J.i; assume
a in pi(X,i);
then consider h being Function such that
A7: h in X & a = h.i by CARD_3:def 6;
reconsider h as Element of product J by A7;
h <= g by A5,A7,LATTICE3:def 9;
hence a <= g.i by A7,WAYBEL_3:28;
end;
hence f.i <= g.i by A6,YELLOW_0:30;
end;
hence f <= g by WAYBEL_3:28;
end;
Lm2:
now let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J;
deffunc F(Element of I) = inf pi(X,$1);
consider f being ManySortedSet of I such that
A1: for i being Element of I holds f.i = F(i) from LambdaDMS;
A2: dom f = I by PBOOLE:def 3;
now let i be Element of I;
f.i = inf pi(X,i) by A1;
hence f.i is Element of J.i;
end;
then reconsider f as Element of product J by A2,WAYBEL_3:27;
assume
A3: for i being Element of I holds ex_inf_of pi(X,i), J.i;
take f;
thus for i being Element of I holds f.i = inf pi(X,i) by A1;
thus f is_<=_than X
proof let x be Element of product J such that
A4: x in X;
now let i be Element of I;
ex_inf_of pi(X,i), J.i & f.i = inf pi(X,i) by A1,A3;
then f.i is_<=_than pi(X,i) & x.i in pi(X,i)
by A4,CARD_3:def 6,YELLOW_0:31;
hence x.i >= f.i by LATTICE3:def 8;
end;
hence thesis by WAYBEL_3:28;
end;
let g be Element of product J; assume
A5: X is_>=_than g;
now let i be Element of I;
A6: f.i = inf pi(X,i) & ex_inf_of pi(X,i), J.i by A1,A3;
g.i is_<=_than pi(X,i)
proof let a be Element of J.i; assume
a in pi(X,i);
then consider h being Function such that
A7: h in X & a = h.i by CARD_3:def 6;
reconsider h as Element of product J by A7;
h >= g by A5,A7,LATTICE3:def 8;
hence a >= g.i by A7,WAYBEL_3:28;
end;
hence f.i >= g.i by A6,YELLOW_0:31;
end;
hence f >= g by WAYBEL_3:28;
end;
theorem Th31:
for I being non empty set
for J being Poset-yielding non-Empty ManySortedSet of I
for f being Element of product J, X being Subset of product J
holds
f is_>=_than X
iff for i being Element of I holds f.i is_>=_than pi(X,i)
proof let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let f be Element of product J, X be Subset of product J;
hereby assume
A1: f is_>=_than X;
let i be Element of I;
thus f.i is_>=_than pi(X, i)
proof let x be Element of J.i; assume
x in pi(X, i);
then consider g being Function such that
A2: g in X & x = g.i by CARD_3:def 6;
reconsider g as Element of product J by A2;
g <= f by A1,A2,LATTICE3:def 9;
hence thesis by A2,WAYBEL_3:28;
end;
end;
assume
A3: for i being Element of I holds f.i is_>=_than pi(X,i);
let g be Element of product J; assume
A4: g in X;
now let i be Element of I;
g.i in pi(X,i) & f.i is_>=_than pi(X,i) by A3,A4,CARD_3:def 6;
hence g.i <= f.i by LATTICE3:def 9;
end;
hence thesis by WAYBEL_3:28;
end;
theorem Th32:
for I being non empty set
for J being Poset-yielding non-Empty ManySortedSet of I
for f being Element of product J, X being Subset of product J
holds
f is_<=_than X
iff for i being Element of I holds f.i is_<=_than pi(X,i)
proof let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let f be Element of product J, X be Subset of product J;
hereby assume
A1: f is_<=_than X;
let i be Element of I;
thus f.i is_<=_than pi(X, i)
proof let x be Element of J.i; assume
x in pi(X, i);
then consider g being Function such that
A2: g in X & x = g.i by CARD_3:def 6;
reconsider g as Element of product J by A2;
g >= f by A1,A2,LATTICE3:def 8;
hence thesis by A2,WAYBEL_3:28;
end;
end;
assume
A3: for i being Element of I holds f.i is_<=_than pi(X,i);
let g be Element of product J; assume
A4: g in X;
now let i be Element of I;
g.i in pi(X,i) & f.i is_<=_than pi(X,i) by A3,A4,CARD_3:def 6;
hence g.i >= f.i by LATTICE3:def 8;
end;
hence thesis by WAYBEL_3:28;
end;
theorem Th33:
for I being non empty set
for J being Poset-yielding non-Empty ManySortedSet of I
for X being Subset of product J
holds
ex_sup_of X, product J
iff for i being Element of I holds ex_sup_of pi(X,i), J.i
proof let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J;
hereby assume
A1: ex_sup_of X, product J;
let i be Element of I; set f = sup X;
f is_>=_than X by A1,YELLOW_0:30;
then A2: f.i is_>=_than pi(X, i) by Th31;
now let x be Element of J.i; assume
A3: pi(X,i) is_<=_than x;
set g = f+*(i,x);
A4: dom g = dom f & dom f = I by FUNCT_7:32,WAYBEL_3:27;
then A5: g.i = x by FUNCT_7:33;
now let j be Element of I;
g.j = f.j or g.j = x & j = i by A5,FUNCT_7:34;
hence g.j is Element of J.j;
end;
then reconsider g as Element of product J by A4,WAYBEL_3:27;
A6: X is_<=_than f by A1,YELLOW_0:30;
X is_<=_than g
proof let h be Element of product J; assume h in X;
then A7: h <= f & h.i in pi(X, i) by A6,CARD_3:def 6,LATTICE3:def 9;
now let j be Element of I;
g.j = f.j or g.j = x & j = i by A5,FUNCT_7:34;
hence h.j <= g.j by A3,A7,LATTICE3:def 9,WAYBEL_3:28;
end;
hence h <= g by WAYBEL_3:28;
end;
then f <= g by A1,YELLOW_0:30;
hence f.i <= x by A5,WAYBEL_3:28;
end;
hence ex_sup_of pi(X, i), J.i by A2,YELLOW_0:30;
end;
assume for i being Element of I holds ex_sup_of pi(X,i), J.i;
then consider f being Element of product J such that
for i being Element of I holds f.i = sup pi(X,i) and
A8: f is_>=_than X and
A9: for g being Element of product J st X is_<=_than g holds f <= g by Lm1;
thus ex_sup_of X, product J by A8,A9,YELLOW_0:30;
end;
theorem Th34:
for I being non empty set
for J being Poset-yielding non-Empty ManySortedSet of I
for X being Subset of product J
holds
ex_inf_of X, product J
iff for i being Element of I holds ex_inf_of pi(X,i), J.i
proof let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J;
hereby assume
A1: ex_inf_of X, product J;
let i be Element of I; set f = inf X;
A2: f is_<=_than X by A1,YELLOW_0:31;
then A3: f.i is_<=_than pi(X, i) by Th32;
now let x be Element of J.i; assume
A4: pi(X,i) is_>=_than x;
set g = f+*(i,x);
A5: dom g = dom f & dom f = I by FUNCT_7:32,WAYBEL_3:27;
then A6: g.i = x by FUNCT_7:33;
now let j be Element of I;
g.j = f.j or g.j = x & j = i by A6,FUNCT_7:34;
hence g.j is Element of J.j;
end;
then reconsider g as Element of product J by A5,WAYBEL_3:27;
X is_>=_than g
proof let h be Element of product J; assume h in X;
then A7: h >= f & h.i in pi(X, i) by A2,CARD_3:def 6,LATTICE3:def 8;
now let j be Element of I;
g.j = f.j or g.j = x & j = i by A6,FUNCT_7:34;
hence h.j >= g.j by A4,A7,LATTICE3:def 8,WAYBEL_3:28;
end;
hence h >= g by WAYBEL_3:28;
end;
then f >= g by A1,YELLOW_0:31;
hence f.i >= x by A6,WAYBEL_3:28;
end;
hence ex_inf_of pi(X, i), J.i by A3,YELLOW_0:31;
end;
assume for i being Element of I holds ex_inf_of pi(X,i), J.i;
then consider f being Element of product J such that
for i being Element of I holds f.i = inf pi(X,i) and
A8: f is_<=_than X and
A9: for g being Element of product J st X is_>=_than g holds f >= g by Lm2;
thus ex_inf_of X, product J by A8,A9,YELLOW_0:31;
end;
theorem Th35:
for I being non empty set
for J being Poset-yielding non-Empty ManySortedSet of I
for X being Subset of product J
st ex_sup_of X, product J
for i being Element of I holds (sup X).i = sup pi(X,i)
proof let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J; assume ex_sup_of X, product J;
then for i being Element of I holds ex_sup_of pi(X,i), J.i by Th33;
then consider f being Element of product J such that
A1: for i being Element of I holds f.i = sup pi(X,i) and
A2: f is_>=_than X and
A3: for g being Element of product J st X is_<=_than g holds f <= g by Lm1;
sup X = f by A2,A3,YELLOW_0:30;
hence thesis by A1;
end;
theorem Th36:
for I being non empty set
for J being Poset-yielding non-Empty ManySortedSet of I
for X being Subset of product J
st ex_inf_of X, product J
for i being Element of I holds (inf X).i = inf pi(X,i)
proof let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J; assume ex_inf_of X, product J;
then for i being Element of I holds ex_inf_of pi(X,i), J.i by Th34;
then consider f being Element of product J such that
A1: for i being Element of I holds f.i = inf pi(X,i) and
A2: f is_<=_than X and
A3: for g being Element of product J st X is_>=_than g holds f >= g by Lm2;
inf X = f by A2,A3,YELLOW_0:31;
hence thesis by A1;
end;
theorem Th37:
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
for X being directed Subset of product J
for i being Element of I holds pi(X,i) is directed
proof let I be non empty set;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
let X be directed Subset of product J;
let i be Element of I; let x,y be Element of J.i;
assume x in pi(X,i);
then consider f being Function such that
A1: f in X & x = f.i by CARD_3:def 6;
assume y in pi(X,i);
then consider g being Function such that
A2: g in X & y = g.i by CARD_3:def 6;
reconsider f,g as Element of product J by A1,A2;
consider h being Element of product J such that
A3: h in X & f <= h & g <= h by A1,A2,WAYBEL_0:def 1;
take h.i;
thus h.i in pi(X,i) by A3,CARD_3:def 6;
thus thesis by A1,A2,A3,WAYBEL_3:28;
end;
theorem Th38:
for I being non empty set
for J,K being RelStr-yielding non-Empty ManySortedSet of I
st for i being Element of I holds K.i is SubRelStr of J.i
holds product K is SubRelStr of product J
proof let I be non empty set;
let J,K be RelStr-yielding non-Empty ManySortedSet of I such that
A1: for i being Element of I holds K.i is SubRelStr of J.i;
A2: the carrier of product K = product Carrier K by YELLOW_1:def 4;
A3: the carrier of product J = product Carrier J by YELLOW_1:def 4;
A4: dom Carrier J = I & dom Carrier K = I by PBOOLE:def 3;
now let i be set; assume i in I; then reconsider j = i as Element of I;
A5: (ex R being 1-sorted st R = J.j & (Carrier J).j = the carrier of R) &
(ex R being 1-sorted st R = K.j & (Carrier K).j = the carrier of R)
by PRALG_1:def 13;
K.j is SubRelStr of J.j by A1;
hence (Carrier K).i c= (Carrier J).i by A5,YELLOW_0:def 13;
end;
hence
A6: the carrier of product K c= the carrier of product J
by A2,A3,A4,CARD_3:38;
let x,y be set; assume
A7: [x,y] in the InternalRel of product K;
then A8: x in the carrier of product K & y in the carrier of product K
by ZFMISC_1:106;
then reconsider x,y as Element of product K;
reconsider f = x, g = y as Element of product J by A6,A8;
A9: x <= y by A7,ORDERS_1:def 9;
now let i be Element of I;
K.i is SubRelStr of J.i & x.i <= y.i by A1,A9,WAYBEL_3:28;
hence f.i <= g.i by YELLOW_0:60;
end;
then f <= g by WAYBEL_3:28;
hence thesis by ORDERS_1:def 9;
end;
theorem Th39:
for I being non empty set
for J,K being RelStr-yielding non-Empty ManySortedSet of I
st for i being Element of I holds K.i is full SubRelStr of J.i
holds product K is full SubRelStr of product J
proof let I be non empty set;
let J,K be RelStr-yielding non-Empty ManySortedSet of I; assume
A1: for i being Element of I holds K.i is full SubRelStr of J.i;
then for i being Element of I holds K.i is SubRelStr of J.i;
then reconsider S = product K as non empty SubRelStr of product J by Th38;
A2: (the InternalRel of product J)|_2 the carrier of S =
(the InternalRel of product J)/\[:the carrier of S,the carrier of S:]
by WELLORD1:def 6;
S is full
proof
the InternalRel of S c= the InternalRel of product J
by YELLOW_0:def 13;
hence the InternalRel of S c= (the InternalRel of product J)|_2
the carrier of S by A2,XBOOLE_1:19;
let x,y be set; assume
[x,y] in (the InternalRel of product J)|_2 the carrier of S;
then A3: [x,y] in the InternalRel of product J &
[x,y] in [:the carrier of S, the carrier of S:] by A2,XBOOLE_0:def 3
;
then x in the carrier of S & y in the carrier of S by ZFMISC_1:106;
then reconsider x, y as Element of S;
reconsider a = x, b = y as Element of product J by YELLOW_0:59;
reconsider x, y as Element of product K;
A4: a <= b by A3,ORDERS_1:def 9;
now let i be Element of I;
a.i <= b.i & K.i is full SubRelStr of J.i & x.i in the carrier of K.
i
by A1,A4,WAYBEL_3:28;
hence x.i <= y.i by YELLOW_0:61;
end;
then x <= y by WAYBEL_3:28;
hence thesis by ORDERS_1:def 9;
end;
hence thesis;
end;
theorem
for L being non empty RelStr, S being non empty SubRelStr of L, X being set
holds S|^X is SubRelStr of L|^X
proof let L be non empty RelStr, S be non empty SubRelStr of L, X be set;
A1: S|^X = product (X --> S) & L|^X = product (X --> L) by YELLOW_1:def 5;
per cases; suppose X = {};
then S|^X = RelStr (#{{}}, id {{}}#) & L|^X = RelStr (#{{}},
id {
{}}#)
by YELLOW_1:27;
hence thesis by YELLOW_6:15;
suppose X <> {};
then reconsider X as non empty set;
now let i be Element of X;
(X --> L).i = L & (X --> S).i = S by FUNCOP_1:13;
hence (X --> S).i is SubRelStr of (X --> L).i;
end;
hence thesis by A1,Th38;
end;
theorem Th41:
for L being non empty RelStr, S be full non empty SubRelStr of L, X be set
holds S|^X is full SubRelStr of L|^X
proof let L be non empty RelStr, S be full non empty SubRelStr of L,
X be set;
A1: S|^X = product (X --> S) & L|^X = product (X --> L) by YELLOW_1:def 5;
per cases; suppose X = {};
then S|^X = RelStr (#{{}}, id {{}}#) & L|^X = RelStr (#{{}},id {{}}#)
by YELLOW_1:27;
hence thesis by YELLOW_6:15;
suppose X <> {};
then reconsider X as non empty set;
now let i be Element of X;
(X --> L).i = L & (X --> S).i = S by FUNCOP_1:13;
hence (X --> S).i is full SubRelStr of (X --> L).i;
end;
hence thesis by A1,Th39;
end;
begin :: Inheritance
definition
let S,T be non empty RelStr, X be set;
pred S inherits_sup_of X,T means:Def6:
ex_sup_of X,T implies "\/"(X, T) in the carrier of S;
pred S inherits_inf_of X,T means:Def7:
ex_inf_of X,T implies "/\"(X, T) in the carrier of S;
end;
theorem Th42:
for T being non empty transitive RelStr
for S being full non empty SubRelStr of T
for X being Subset of S
holds S inherits_sup_of X,T iff
(ex_sup_of X,T implies ex_sup_of X, S & sup X = "\/"(X, T))
proof let T be non empty transitive RelStr;
let S be full non empty SubRelStr of T;
let X be Subset of S;
hereby assume that
A1: S inherits_sup_of X,T and
A2: ex_sup_of X,T;
"\/"(X, T) in the carrier of S by A1,A2,Def6;
hence ex_sup_of X, S & sup X = "\/"(X, T) by A2,YELLOW_0:65;
end;
assume
A3: ex_sup_of X,T implies ex_sup_of X, S & sup X = "\/"(X, T);
assume ex_sup_of X,T; hence thesis by A3;
end;
theorem
for T being non empty transitive RelStr
for S being full non empty SubRelStr of T
for X being Subset of S
holds S inherits_inf_of X,T iff
(ex_inf_of X,T implies ex_inf_of X, S & inf X = "/\"(X, T))
proof let T be non empty transitive RelStr;
let S be full non empty SubRelStr of T;
let X be Subset of S;
hereby assume that
A1: S inherits_inf_of X,T and
A2: ex_inf_of X,T;
"/\"(X, T) in the carrier of S by A1,A2,Def7;
hence ex_inf_of X, S & inf X = "/\"(X, T) by A2,YELLOW_0:64;
end;
assume
A3: ex_inf_of X,T implies ex_inf_of X, S & inf X = "/\"(X, T);
assume ex_inf_of X,T; hence thesis by A3;
end;
scheme ProductSupsInheriting
{ I() -> non empty set,
J,K() -> Poset-yielding non-Empty ManySortedSet of I(),
P[set, set] }:
for X being Subset of product K() st P[X, product K()]
holds product K() inherits_sup_of X, product J()
provided
A1: for X being Subset of product K() st P[X, product K()]
for i being Element of I() holds P[pi(X, i), K().i]
and
A2: for i being Element of I() holds K().i is full SubRelStr of J().i
and
A3: for i being Element of I(), X being Subset of K().i st P[X, K().i]
holds K().i inherits_sup_of X, J().i
proof let X be Subset of product K() such that
A4: P[X, product K()] and
A5: ex_sup_of X, product J();
set f = "\/"(X, product J());
product K() is SubRelStr of product J() by A2,Th39;
then the carrier of product K() c= the carrier of product J()
by YELLOW_0:def 13;
then X c= the carrier of product J() by XBOOLE_1:1;
then reconsider Y = X as Subset of product J();
A6: dom f = I() by WAYBEL_3:27;
now let i be Element of I();
P[pi(X, i), K().i] by A1,A4;
then A7: K().i inherits_sup_of pi(X, i), J().i by A3;
ex_sup_of pi(Y,i), J().i by A5,Th33;
then sup pi(Y,i) in the carrier of K().i by A7,Def6;
then f.i in the carrier of K().i by A5,Th35;
hence f.i is Element of K().i;
end;
then "\/"(X, product J()) is Element of product K() by A6,WAYBEL_3:27;
hence thesis;
end;
scheme PowerSupsInheriting
{ I() -> non empty set,
L() -> non empty Poset,
S() -> non empty full SubRelStr of L(),
P[set, set] }:
for X being Subset of S()|^I() st P[X, S()|^I()]
holds S()|^I() inherits_sup_of X, L()|^I()
provided
A1: for X being Subset of S()|^I() st P[X, S()|^I()]
for i being Element of I() holds P[pi(X, i), S()]
and
A2: for X being Subset of S() st P[X, S()] holds S() inherits_sup_of X, L()
proof
defpred p[set,set] means P[$1,$2];
reconsider K = I() --> S(), J = I() --> L() as
Poset-yielding non-Empty ManySortedSet of I();
A3: S()|^I() = product K & L()|^I() = product J by YELLOW_1:def 5;
A4: now let X be Subset of product K such that
A5: p[X, product K];
let i be Element of I();
K.i = S() by FUNCOP_1:13;
hence p[pi(X, i), K.i] by A1,A3,A5;
end;
A6: now let i be Element of I();
K.i = S() & J.i = L() by FUNCOP_1:13;
hence K.i is full SubRelStr of J.i;
end;
A7: now let i be Element of I(), X be Subset of K.i such that
A8: p[X, K.i];
K.i = S() & J.i = L() by FUNCOP_1:13;
hence K.i inherits_sup_of X, J.i by A2,A8;
end;
for X being Subset of product K st p[X, product K]
holds product K inherits_sup_of X, product J
from ProductSupsInheriting(A4,A6,A7);
hence thesis by A3;
end;
scheme ProductInfsInheriting
{ I() -> non empty set,
J,K() -> Poset-yielding non-Empty ManySortedSet of I(),
P[set, set] }:
for X being Subset of product K() st P[X, product K()]
holds product K() inherits_inf_of X, product J()
provided
A1: for X being Subset of product K() st P[X, product K()]
for i being Element of I() holds P[pi(X, i), K().i]
and
A2: for i being Element of I() holds K().i is full SubRelStr of J().i
and
A3: for i being Element of I(), X being Subset of K().i st P[X, K().i]
holds K().i inherits_inf_of X, J().i
proof let X be Subset of product K() such that
A4: P[X, product K()] and
A5: ex_inf_of X, product J();
set f = "/\"(X, product J());
product K() is SubRelStr of product J() by A2,Th39;
then the carrier of product K() c= the carrier of product J()
by YELLOW_0:def 13;
then X c= the carrier of product J() by XBOOLE_1:1;
then reconsider Y = X as Subset of product J();
A6: dom f = I() by WAYBEL_3:27;
now let i be Element of I();
P[pi(X, i), K().i] by A1,A4;
then A7: K().i inherits_inf_of pi(X, i), J().i by A3;
ex_inf_of pi(Y,i), J().i by A5,Th34;
then inf pi(Y,i) in the carrier of K().i by A7,Def7;
then f.i in the carrier of K().i by A5,Th36;
hence f.i is Element of K().i;
end;
then "/\"(X, product J()) is Element of product K() by A6,WAYBEL_3:27;
hence thesis;
end;
scheme PowerInfsInheriting
{ I() -> non empty set,
L() -> non empty Poset,
S() -> non empty full SubRelStr of L(),
P[set, set] }:
for X being Subset of S()|^I() st P[X, S()|^I()]
holds S()|^I() inherits_inf_of X, L()|^I()
provided
A1: for X being Subset of S()|^I() st P[X, S()|^I()]
for i being Element of I() holds P[pi(X, i), S()]
and
A2: for X being Subset of S() st P[X, S()] holds S() inherits_inf_of X, L()
proof
defpred p[set,set] means P[$1,$2];
reconsider K = I() --> S(), J = I() --> L() as
Poset-yielding non-Empty ManySortedSet of I();
A3: S()|^I() = product K & L()|^I() = product J by YELLOW_1:def 5;
A4: now let X be Subset of product K such that
A5: p[X, product K];
let i be Element of I();
K.i = S() by FUNCOP_1:13;
hence p[pi(X, i), K.i] by A1,A3,A5;
end;
A6: now let i be Element of I();
K.i = S() & J.i = L() by FUNCOP_1:13;
hence K.i is full SubRelStr of J.i;
end;
A7: now let i be Element of I(), X be Subset of K.i such that
A8: p[X, K.i];
K.i = S() & J.i = L() by FUNCOP_1:13;
hence K.i inherits_inf_of X, J.i by A2,A8;
end;
for X being Subset of product K st p[X, product K]
holds product K inherits_inf_of X, product J
from ProductInfsInheriting(A4,A6,A7);
hence thesis by A3;
end;
definition
let I be set;
let L be non empty RelStr;
let X be non empty Subset of L|^I;
let i be set;
cluster pi(X,i) -> non empty;
coherence
proof L|^I = product (I --> L) by YELLOW_1:def 5;
then reconsider Y = X as non empty Subset of product (I --> L);
consider f being Element of Y;
f in the carrier of product (I --> L); then
f in product Carrier (I --> L) by YELLOW_1:def 4; then
reconsider f as Function by AMI_1:22;
f.i in pi(X,i) by CARD_3:def 6;
hence thesis;
end;
end;
theorem
for L being non empty Poset
for S being directed-sups-inheriting non empty full SubRelStr of L
for X be non empty set
holds S|^X is directed-sups-inheriting SubRelStr of L|^X
proof let L be non empty Poset;
let S be directed-sups-inheriting non empty full SubRelStr of L;
let X be non empty set;
reconsider SX = S|^X as full non empty SubRelStr of L|^X by Th41;
defpred P[set, non empty reflexive RelStr] means
$1 is directed non empty Subset of $2;
A1: now let A be Subset of S|^X; assume P[A,S|^X];
then reconsider B = A as directed non empty Subset of S|^X;
let i be Element of X;
product (X --> S) = S|^X & (X --> S).i = S
by FUNCOP_1:13,YELLOW_1:def 5;
then pi(B, i) is directed non empty Subset of S by Th37;
hence P[pi(A, i),S];
end;
A2: now let X be Subset of S; assume P[X,S];
then
ex_sup_of X,L implies ex_sup_of X, S & sup X = "\/"(X, L) by WAYBEL_0:7;
hence S inherits_sup_of X, L by Th42;
end;
SX is directed-sups-inheriting
proof let A be directed Subset of SX;
for A being Subset of S|^X st P[A,S|^X]
holds S|^X inherits_sup_of A, L|^X
from PowerSupsInheriting(A1,A2);
then A <> {} implies S|^X inherits_sup_of A, L|^X;
hence thesis by Def6;
end;
hence thesis;
end;
definition
let I be non empty set;
let J be RelStr-yielding non-Empty ManySortedSet of I;
let X be non empty Subset of product J;
let i be set;
cluster pi(X,i) -> non empty;
coherence
proof consider f being Element of X;
f in the carrier of product J; then
f in product Carrier J by YELLOW_1:def 4; then
reconsider f as Function by AMI_1:22;
f.i in pi(X,i) by CARD_3:def 6;
hence thesis;
end;
end;
theorem Th45:
for X being non empty set
for L being up-complete (non empty Poset)
holds L|^X is up-complete
proof let X be non empty set;
let L be up-complete (non empty Poset);
A1: L|^X = product (X --> L) by YELLOW_1:def 5;
now let A be non empty directed Subset of L|^X;
reconsider B = A as non empty directed Subset of product (X --> L) by A1;
now let x be Element of X;
A2: (X --> L).x = L by FUNCOP_1:13;
pi(B,x) is directed non empty by Th37;
hence ex_sup_of pi(A,x), (X --> L).x by A2,WAYBEL_0:75;
end;
hence ex_sup_of A,L|^X by A1,Th33;
end;
hence thesis by WAYBEL_0:75;
end;
definition
let L be up-complete (non empty Poset);
let X be non empty set;
cluster L|^X -> up-complete;
coherence by Th45;
end;
begin :: Topological retracts
definition
let T be TopSpace;
cluster the topology of T -> non empty;
coherence by PRE_TOPC:def 1;
end;
theorem Th46:
for T being non empty TopSpace, S being non empty SubSpace of T
for f being ::continuous
map of T,S st f is_a_retraction
holds rng f = the carrier of S
proof let T be non empty TopSpace, S be non empty SubSpace of T;
let f be map of T,S such that
A1: for W being Point of T st W in the carrier of S holds f.W=W;
thus rng f c= the carrier of S;
[#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12;
then A2: the carrier of S c= the carrier of T by PRE_TOPC:def 9;
let x be set; assume
A3: x in the carrier of S;
then x in the carrier of T by A2;
then f.x = x & x in dom f by A1,A3,FUNCT_2:def 1;
hence thesis by FUNCT_1:def 5;
end;
theorem
for T being non empty TopSpace, S being non empty SubSpace of T
for f being continuous map of T,S st f is_a_retraction
holds f is idempotent
proof let T be non empty TopSpace, S be non empty SubSpace of T;
let f be continuous map of T,S such that
A1: f is_a_retraction;
[#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12;
then A2: the carrier of S c= the carrier of T by PRE_TOPC:def 9;
A3: dom f = the carrier of T & rng f = the carrier of S
by A1,Th46,FUNCT_2:def 1;
then A4: dom (f*f) = the carrier of T by A2,RELAT_1:46;
now let x be set; assume x in the carrier of T;
then (f*f).x = f.(f.x) & f.x in rng f by A3,FUNCT_1:23,def 5;
hence (f*f).x = f.x by A1,A2,A3,BORSUK_1:def 19;
end;
then f*f = f by A3,A4,FUNCT_1:9;
hence thesis by QUANTAL1:def 9;
end;
theorem Th48:
for T being non empty TopSpace, V being open Subset of T
holds chi(V, the carrier of T) is continuous map of T, Sierpinski_Space
proof let T be non empty TopSpace, V be open Subset of T;
the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
then reconsider c = chi(V, the carrier of T) as map of T, Sierpinski_Space;
c = chi(c"{1}, the carrier of T) by FUNCT_3:49;
then A1: V = c"{1} by FUNCT_3:47;
A2: c"{} = {}T by RELAT_1:171;
A3: c"{0,1} = the carrier of T by FUNCT_2:48 .= [#]T by PRE_TOPC:12;
now let W be Subset of Sierpinski_Space;
assume W is open;
then W in the topology of Sierpinski_Space by PRE_TOPC:def 5;
then W in {{}, {1}, {0,1}} by WAYBEL18:def 9;
hence c"W is open by A1,A2,A3,ENUMSET1:13;
end;
hence thesis by TOPS_2:55;
end;
theorem
for T being non empty TopSpace, x,y being Element of T
st for W being open Subset of T st y in W holds x in W
holds (0,1) --> (y,x) is continuous map of Sierpinski_Space, T
proof let T be non empty TopSpace;
let x,y be Element of T such that
A1: for W being open Subset of T st y in W holds x in W;
A2: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
then reconsider i = (0,1) --> (y,x) as map of Sierpinski_Space, T;
A3: i.0 = y & i.1 = x by FUNCT_4:66;
A4: 0 in {0,1} & 1 in {0,1} & 0 in {0} & not 1 in {0} by TARSKI:def 1,def 2;
now let W be Subset of T; assume
W is open;
then A5: y in W & x in W or not y in W & x in W or not y in W & not x in
W by A1;
i"W = {} or i"W = {0} or i"W = {1} or i"W = {0,1} by A2,ZFMISC_1:42;
then i"W in {{}, {1}, {0,1}} by A3,A4,A5,ENUMSET1:14,FUNCT_2:46;
then i"W in the topology of Sierpinski_Space by WAYBEL18:def 9;
hence i"W is open by PRE_TOPC:def 5;
end;
hence thesis by TOPS_2:55;
end;
theorem
for T being non empty TopSpace, x,y being Element of T
for V being open Subset of T
st x in V & not y in V
holds chi(V, the carrier of T)*((0,1) --> (y,x)) = id Sierpinski_Space
proof let T be non empty TopSpace;
let x,y be Element of T, V be open Subset of T such that
A1: x in V & not y in V;
A2: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
then reconsider i = (0,1) --> (y,x) as map of Sierpinski_Space, T;
reconsider c = chi(V, the carrier of T) as map of T, Sierpinski_Space
by Th48;
A3: i.0 = y & i.1 = x by FUNCT_4:66;
A4: c.x = 1 & c.y = 0 by A1,FUNCT_3:def 3;
now
thus c*i is map of Sierpinski_Space, Sierpinski_Space;
let a be Element of Sierpinski_Space;
a = 0 or a = 1 by A2,TARSKI:def 2;
hence (c*i).a = a by A3,A4,FUNCT_2:21
.= (id Sierpinski_Space).a by GRCAT_1:11;
end;
hence thesis by YELLOW_2:9;
end;
theorem
for T being non empty 1-sorted, V,W being Subset of T
for S being TopAugmentation of BoolePoset 1
for f, g being map of T, S
st f = chi(V, the carrier of T) & g = chi(W, the carrier of T)
holds V c= W iff f <= g
proof let T be non empty 1-sorted, V,W be Subset of T;
let S be TopAugmentation of BoolePoset 1;
A1: the RelStr of S = BoolePoset 1 by YELLOW_9:def 4;
let c1, c2 be map of T, S such that
A2: c1 = chi(V, the carrier of T) & c2 = chi(W, the carrier of T);
hereby assume
A3: V c= W;
now let z be set; assume z in the carrier of T;
then reconsider x = z as Element of T;
reconsider a = c1.x, b = c2.x as Element of BoolePoset 1
by A1;
x in V & x in W or not x in V by A3;
then c1.x = 1 & c2.x = 1 or c1.x = 0 by A2,FUNCT_3:def 3;
then c1.x c= c2.x by XBOOLE_1:2;
then a <= b by YELLOW_1:2;
then c1.x <= c2.x by A1,YELLOW_0:1;
hence ex a,b being Element of S st a = c1.z & b = c2.z & a <= b;
end;
hence c1 <= c2 by YELLOW_2:def 1;
end;
assume A4: c1 <= c2;
let x be set; assume
A5: x in V & not x in W;
then reconsider x as Element of T;
reconsider a = c1.x, b = c2.x as Element of BoolePoset 1
by A1;
ex a,b being Element of S st a = c1.x & b = c2.x & a <= b by A4,YELLOW_2:
def 1;
then c1.x = 1 & c2.x = 0 & a <= b by A1,A2,A5,FUNCT_3:def 3,YELLOW_0:1;
then 1 c= 0 & 0 c= 1 & 0 <> 1 by XBOOLE_1:2,YELLOW_1:2;
hence thesis by XBOOLE_0:def 10;
end;
theorem
for L being non empty RelStr, X being non empty set
for R being full non empty SubRelStr of L|^X
st for a being set holds a is Element of R iff
ex x being Element of L st a = X --> x
holds L, R are_isomorphic
proof let L be non empty RelStr, X be non empty set;
let R be full non empty SubRelStr of L|^X such that
A1: for a being set holds a is Element of R iff
ex x being Element of L st a = X --> x;
deffunc F(set) = X --> $1;
consider f being ManySortedSet of the carrier of L such that
A2: for i being Element of L holds f.i = F(i) from LambdaDMS;
A3: dom f = the carrier of L by PBOOLE:def 3;
rng f c= the carrier of R
proof let y be set; assume y in rng f;
then consider x being set such that
A4: x in dom f & y = f.x by FUNCT_1:def 5;
reconsider x as Element of L by A3,A4;
y = X --> x by A2,A4;
then y is Element of R by A1;
hence thesis;
end;
then f is Function of the carrier of L, the carrier of R by A3,FUNCT_2:4;
then reconsider f as map of L, R;
take f;
A5: rng f = the carrier of R
proof thus rng f c= the carrier of R;
let x be set; assume x in the carrier of R;
then reconsider a = x as Element of R;
consider i being Element of L such that
A6: a = X --> i by A1;
a = f.i by A2,A6;
hence thesis by A3,FUNCT_1:def 5;
end;
A7: f is one-to-one
proof let x,y be Element of L;
f.x = X --> x & f.y = X --> y by A2;
then f.x = [:X,{x}:] & f.y = [:X,{y}:] by FUNCOP_1:def 2;
then f.x = f.y implies {x} = {y} by ZFMISC_1:134;
hence thesis by ZFMISC_1:6;
end;
now let x,y be Element of L;
A8: f.x = X --> x & f.y = X --> y by A2;
reconsider a = f.x, b = f.y as Element of L|^X by YELLOW_0:59;
hereby assume
A9: x <= y;
X --> x <= X --> y
proof let i be set; assume i in X;
then (X --> x).i = x & (X --> y).i = y by FUNCOP_1:13;
hence ex p,q being Element of L st
p = (X --> x).i & q = (X --> y).i & p <= q by A9;
end;
then a <= b & f.x in the carrier of R by A8,WAYBEL10:12;
hence f.x <= f.y by YELLOW_0:61;
end;
A10: L|^X = product (X --> L) by YELLOW_1:def 5;
reconsider a' = a, b' = b as Element of product (X --> L) by YELLOW_1:def
5;
consider i being Element of X;
A11: (X --> L).i = L by FUNCOP_1:13;
assume f.x <= f.y;
then a <= b by YELLOW_0:60;
then a'.i <= b'.i by A10,WAYBEL_3:28;
then x <= (X --> y).i by A8,A11,FUNCOP_1:13;
hence x <= y by FUNCOP_1:13;
end;
hence f is isomorphic by A5,A7,WAYBEL_0:66;
end;
theorem
for S,T being non empty TopSpace holds
S, T are_homeomorphic iff
ex f being continuous map of S,T, g being continuous map of T,S
st f*g = id T & g*f = id S
proof let S,T be non empty TopSpace;
A1: id T = id the carrier of T & id S = id the carrier of S by GRCAT_1:def 11;
A2: [#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12;
hereby assume S, T are_homeomorphic;
then consider f being map of S,T such that
A3: f is_homeomorphism by T_0TOPSP:def 1;
reconsider f as continuous map of S,T by A3,TOPS_2:def 5;
reconsider g = f" as continuous map of T,S by A3,TOPS_2:def 5;
take f,g;
f is one-to-one & rng f = [#]T & dom f = [#]S by A3,TOPS_2:def 5;
hence f*g = id T & g*f = id S by A1,A2,TOPS_2:65;
end;
given f being continuous map of S,T, g being continuous map of T,S such that
A4: f*g = id T & g*f = id S;
take f;
A5: f is one-to-one & rng f = [#]T & dom f = [#]S by A1,A2,A4,FUNCT_2:29,def 1
;
then g = f qua Function" by A1,A2,A4,FUNCT_2:36
.= f" by A5,TOPS_2:def 4;
hence f is_homeomorphism by A5,TOPS_2:def 5;
end;
theorem Th54:
for T, S, R being non empty TopSpace
for f being map of T,S, g being map of S,T, h being map of S, R
st f*g = id S & h is_homeomorphism
holds (h*f)*(g*(h")) = id R
proof let T, S, R be non empty TopSpace;
let f be map of T,S, g be map of S,T, h be map of S, R such that
A1: f*g = id S and
A2: h is_homeomorphism;
A3: h is one-to-one & rng h = [#]R & dom h = [#]S by A2,TOPS_2:def 5;
thus (h*f)*(g*(h")) = (h*f)*g*(h") by RELAT_1:55
.= h*(f*g)*(h") by RELAT_1:55
.= h*(id the carrier of S)*(h") by A1,GRCAT_1:def 11
.= h*(h") by FUNCT_2:23
.= id rng h by A3,TOPS_2:65
.= id the carrier of R by A3,PRE_TOPC:12
.= id R by GRCAT_1:def 11;
end;
theorem Th55:
for T, S, R being non empty TopSpace
st S is_Retract_of T & S, R are_homeomorphic
holds R is_Retract_of T
proof let T, S, R be non empty TopSpace;
given f being continuous map of S,T, g being continuous map of T,S such that
A1: g*f = id S;
given h being map of S,R such that
A2: h is_homeomorphism;
A3: h is continuous & h" is continuous by A2,TOPS_2:def 5;
then reconsider f' = f*(h") as continuous map of R,T by TOPS_2:58;
reconsider g' = h*g as continuous map of T,R by A3,TOPS_2:58;
take f',g'; thus thesis by A1,A2,Th54;
end;
theorem Th56:
for T being non empty TopSpace, S being non empty SubSpace of T
holds incl(S,T) is continuous
proof let T be non empty TopSpace, S be non empty SubSpace of T;
the carrier of S c= the carrier of T by BORSUK_1:35;
then incl(S,T) = id the carrier of S by YELLOW_9:def 1
.= id S by GRCAT_1:def 11;
hence thesis by TOPMETR:7;
end;
theorem Th57:
for T being non empty TopSpace
for S being non empty SubSpace of T, f being continuous map of T,S
st f is_a_retraction
holds f*incl(S,T) = id S
proof let T be non empty TopSpace, S be non empty SubSpace of T;
let f be continuous map of T,S such that
A1: f is_a_retraction;
[#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12;
then A2: the carrier of S c= the carrier of T by PRE_TOPC:def 9;
then A3: incl(S,T) = id the carrier of S by YELLOW_9:def 1;
now let x be Element of S;
x in the carrier of S;
then reconsider y = x as Point of T by A2;
thus (f*incl(S,T)).x = f.((incl(S,T)).x) by FUNCT_2:21
.= f.x by A3,FUNCT_1:35 .= y by A1,BORSUK_1:def 19
.= (id S).x by GRCAT_1:11;
end;
hence thesis by YELLOW_2:9;
end;
theorem Th58:
for T being non empty TopSpace, S being non empty SubSpace of T
st S is_a_retract_of T
holds S is_Retract_of T
proof let T be non empty TopSpace, S be non empty SubSpace of T;
given f be continuous map of T,S such that
A1: f is_a_retraction;
reconsider g = incl(S,T) as continuous map of S,T by Th56;
take g,f; thus thesis by A1,Th57;
end;
theorem
for R,T being non empty TopSpace holds
R is_Retract_of T iff
ex S being non empty SubSpace of T
st S is_a_retract_of T & S,R are_homeomorphic
proof let R,T be non empty TopSpace;
hereby assume R is_Retract_of T;
then consider f being map of T,T such that
A1: f is continuous & f*f = f & Image f, R are_homeomorphic
by WAYBEL18:def 8;
reconsider S = Image f as non empty SubSpace of T;
take S; f = corestr f by WAYBEL18:def 7;
then reconsider f as continuous map of T,S by A1,WAYBEL18:11;
[#]S = the carrier of S & [#]T = the carrier of T by PRE_TOPC:12;
then the carrier of S c= the carrier of T by PRE_TOPC:def 9;
then rng f c= the carrier of T by XBOOLE_1:1;
then reconsider rf = rng f as Subset of T;
now let x be Point of T; assume x in the carrier of S;
then x in the carrier of T|rf by WAYBEL18:def 6;
then x in [#](T|rf) by PRE_TOPC:12;
then x in rng f by PRE_TOPC:def 10;
then ex y being set st y in dom f & x = f.y by FUNCT_1:def 5;
hence f.x = x by A1,FUNCT_1:23;
end;
then f is_a_retraction by BORSUK_1:def 19;
hence S is_a_retract_of T & S, R are_homeomorphic by A1,BORSUK_1:def 20;
end;
given S being non empty SubSpace of T such that
A2: S is_a_retract_of T & S,R are_homeomorphic;
S is_Retract_of T by A2,Th58;
hence R is_Retract_of T by A2,Th55;
end;