:: Retracts and Inheritance
:: by Grzegorz Bancerek
::
:: Copyright (c) 1999-2021 Association of Mizar Users

theorem :: YELLOW16:1
canceled;

::$CT theorem :: YELLOW16:2 for X being set for L being non empty RelStr for S being non empty SubRelStr of L for f, g being Function of X, the carrier of S for f9, g9 being Function of X, the carrier of L st f9 = f & g9 = g & f <= g holds f9 <= g9 proof end; theorem :: YELLOW16:3 for X being set for L being non empty RelStr for S being non empty full SubRelStr of L for f, g being Function of X, the carrier of S for f9, g9 being Function of X, the carrier of L st f9 = f & g9 = g & f9 <= g9 holds f <= g proof end; registration let S be non empty RelStr ; let T be non empty reflexive antisymmetric RelStr ; cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V24( the carrier of S) quasi_total monotone directed-sups-preserving for Element of bool [: the carrier of S, the carrier of T:]; existence ex b1 being Function of S,T st ( b1 is directed-sups-preserving & b1 is monotone ) proof end; end; theorem :: YELLOW16:4 for f, g being Function st f is idempotent & rng g c= rng f & rng g c= dom f holds f * g = g proof end; registration let S be 1-sorted ; cluster Relation-like the carrier of S -defined the carrier of S -valued Function-like V24( the carrier of S) quasi_total idempotent for Element of bool [: the carrier of S, the carrier of S:]; existence ex b1 being Function of S,S st b1 is idempotent proof end; end; theorem Th4: :: YELLOW16:5 for L being non empty up-complete Poset for S being non empty full directed-sups-inheriting SubRelStr of L holds S is up-complete proof end; theorem Th5: :: YELLOW16:6 for L being non empty up-complete Poset for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds Image f is directed-sups-inheriting proof end; theorem Th6: :: YELLOW16:7 for T being non empty RelStr for S being non empty SubRelStr of T for f being Function of T,S st f * (incl (S,T)) = id S holds f is idempotent Function of T,T proof end; definition let S, T be non empty Poset; let f be Function; pred f is_a_retraction_of T,S means :: YELLOW16:def 1 ( f is directed-sups-preserving Function of T,S & f | the carrier of S = id S & S is full directed-sups-inheriting SubRelStr of T ); pred f is_an_UPS_retraction_of T,S means :: YELLOW16:def 2 ( f is directed-sups-preserving Function of T,S & ex g being directed-sups-preserving Function of S,T st f * g = id S ); end; :: deftheorem defines is_a_retraction_of YELLOW16:def 1 : for S, T being non empty Poset for f being Function holds ( f is_a_retraction_of T,S iff ( f is directed-sups-preserving Function of T,S & f | the carrier of S = id S & S is full directed-sups-inheriting SubRelStr of T ) ); :: deftheorem defines is_an_UPS_retraction_of YELLOW16:def 2 : for S, T being non empty Poset for f being Function holds ( f is_an_UPS_retraction_of T,S iff ( f is directed-sups-preserving Function of T,S & ex g being directed-sups-preserving Function of S,T st f * g = id S ) ); definition let S, T be non empty Poset; pred S is_a_retract_of T means :: YELLOW16:def 3 ex f being Function of T,S st f is_a_retraction_of T,S; pred S is_an_UPS_retract_of T means :: YELLOW16:def 4 ex f being Function of T,S st f is_an_UPS_retraction_of T,S; end; :: deftheorem defines is_a_retract_of YELLOW16:def 3 : for S, T being non empty Poset holds ( S is_a_retract_of T iff ex f being Function of T,S st f is_a_retraction_of T,S ); :: deftheorem defines is_an_UPS_retract_of YELLOW16:def 4 : for S, T being non empty Poset holds ( S is_an_UPS_retract_of T iff ex f being Function of T,S st f is_an_UPS_retraction_of T,S ); theorem Th7: :: YELLOW16:8 for S, T being non empty Poset for f being Function st f is_a_retraction_of T,S holds f * (incl (S,T)) = id S proof end; theorem Th8: :: YELLOW16:9 for S being non empty Poset for T being non empty up-complete Poset for f being Function st f is_a_retraction_of T,S holds f is_an_UPS_retraction_of T,S proof end; theorem Th9: :: YELLOW16:10 for S, T being non empty Poset for f being Function st f is_a_retraction_of T,S holds rng f = the carrier of S proof end; theorem Th10: :: YELLOW16:11 for S, T being non empty Poset for f being Function st f is_an_UPS_retraction_of T,S holds rng f = the carrier of S proof end; theorem Th11: :: YELLOW16:12 for S, T being non empty Poset for f being Function st f is_a_retraction_of T,S holds f is idempotent Function of T,T proof end; theorem Th12: :: YELLOW16:13 for T, S being non empty Poset for f being Function of T,T st f is_a_retraction_of T,S holds Image f = RelStr(# the carrier of S, the InternalRel of S #) proof end; theorem Th13: :: YELLOW16:14 for T being non empty up-complete Poset for S being non empty Poset for f being Function of T,T st f is_a_retraction_of T,S holds ( f is directed-sups-preserving & f is projection ) proof end; theorem Th14: :: YELLOW16:15 for S, T being non empty reflexive transitive RelStr for f being Function of S,T holds ( f is isomorphic iff ( f is monotone & ex g being monotone Function of T,S st ( f * g = id T & g * f = id S ) ) ) proof end; theorem Th15: :: YELLOW16:16 for S, T being non empty Poset holds ( S,T are_isomorphic iff ex f being monotone Function of S,T ex g being monotone Function of T,S st ( f * g = id T & g * f = id S ) ) proof end; theorem :: YELLOW16:17 for S, T being non empty up-complete Poset st S,T are_isomorphic holds ( S is_an_UPS_retract_of T & T is_an_UPS_retract_of S ) proof end; theorem Th17: :: YELLOW16:18 for T, S being non empty Poset for f being monotone Function of T,S for g being monotone Function of S,T st f * g = id S holds ex h being projection Function of T,T st ( h = g * f & h | the carrier of () = id () & S, Image h are_isomorphic ) proof end; theorem Th18: :: YELLOW16:19 for T being non empty up-complete Poset for S being non empty Poset for f being Function st f is_an_UPS_retraction_of T,S holds ex h being directed-sups-preserving projection Function of T,T st ( h is_a_retraction_of T, Image h & S, Image h are_isomorphic ) proof end; theorem Th19: :: YELLOW16:20 for L being non empty up-complete Poset for S being non empty Poset st S is_a_retract_of L holds S is up-complete proof end; theorem Th20: :: YELLOW16:21 for L being non empty complete Poset for S being non empty Poset st S is_a_retract_of L holds S is complete proof end; theorem Th21: :: YELLOW16:22 for L being complete continuous LATTICE for S being non empty Poset st S is_a_retract_of L holds S is continuous proof end; theorem :: YELLOW16:23 for L being non empty up-complete Poset for S being non empty Poset st S is_an_UPS_retract_of L holds S is up-complete proof end; theorem :: YELLOW16:24 for L being non empty complete Poset for S being non empty Poset st S is_an_UPS_retract_of L holds S is complete proof end; theorem :: YELLOW16:25 for L being complete continuous LATTICE for S being non empty Poset st S is_an_UPS_retract_of L holds S is continuous proof end; theorem Th25: :: YELLOW16:26 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 end; theorem :: YELLOW16:27 for L being non empty transitive RelStr for S being non empty full directed-sups-inheriting SubRelStr of L for R being non empty directed-sups-inheriting SubRelStr of S holds R is directed-sups-inheriting SubRelStr of L proof end; theorem :: YELLOW16:28 for L being non empty up-complete Poset for S1, S2 being non empty full directed-sups-inheriting SubRelStr of L st S1 is SubRelStr of S2 holds S1 is full directed-sups-inheriting SubRelStr of S2 proof end; definition let R be Relation; attr R is Poset-yielding means :Def5: :: YELLOW16:def 5 for x being set st x in rng R holds x is Poset; end; :: deftheorem Def5 defines Poset-yielding YELLOW16:def 5 : for R being Relation holds ( R is Poset-yielding iff for x being set st x in rng R holds x is Poset ); registration coherence for b1 being Relation st b1 is Poset-yielding holds ( b1 is RelStr-yielding & b1 is reflexive-yielding ) proof 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); :: original: pi redefine func pi (Y,i) -> Subset of L; coherence pi (Y,i) is Subset of L proof end; end; registration let X be set ; let S be Poset; coherence proof end; end; registration let I be set ; existence ex b1 being ManySortedSet of I st ( b1 is Poset-yielding & b1 is non-Empty ) proof end; end; registration let I be non empty set ; let J be non-Empty Poset-yielding ManySortedSet of I; coherence proof end; end; definition let I be non empty set ; let J be non-Empty Poset-yielding ManySortedSet of I; let i be Element of I; :: original: . redefine func J . i -> non empty Poset; coherence J . i is non empty Poset proof end; end; Lm1: now :: thesis: for I being non empty set for J being non-Empty Poset-yielding ManySortedSet of I for X being Subset of () st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds ex f being Element of () st ( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of () st X is_<=_than g holds f <= g ) ) let I be non empty set ; :: thesis: for J being non-Empty Poset-yielding ManySortedSet of I for X being Subset of () st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds ex f being Element of () st ( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of () st X is_<=_than g holds f <= g ) ) let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis: for X being Subset of () st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds ex f being Element of () st ( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of () st X is_<=_than g holds f <= g ) ) let X be Subset of (); :: thesis: ( ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) implies ex f being Element of () st ( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of () st X is_<=_than g holds f <= g ) ) ) deffunc H1( Element of I) -> Element of the carrier of (J .$1) = sup (pi (X,$1)); consider f being ManySortedSet of I such that A1: for i being Element of I holds f . i = H1(i) from PBOOLE:sch 5(); A2: now :: thesis: for i being Element of I holds f . i is Element of (J . i) let i be Element of I; :: thesis: f . i is Element of (J . i) f . i = sup (pi (X,i)) by A1; hence f . i is Element of (J . i) ; :: thesis: verum end; dom f = I by PARTFUN1:def 2; then reconsider f = f as Element of () by ; assume A3: for i being Element of I holds ex_sup_of pi (X,i),J . i ; :: thesis: ex f being Element of () st ( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of () st X is_<=_than g holds f <= g ) ) take f = f; :: thesis: ( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of () st X is_<=_than g holds f <= g ) ) thus for i being Element of I holds f . i = sup (pi (X,i)) by A1; :: thesis: ( f is_>=_than X & ( for g being Element of () st X is_<=_than g holds f <= g ) ) thus f is_>=_than X :: thesis: for g being Element of () st X is_<=_than g holds f <= g proof let x be Element of (); :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= f ) assume A4: x in X ; :: thesis: x <= f now :: thesis: for i being Element of I holds x . i <= f . i let i be Element of I; :: thesis: x . i <= f . i A5: f . i = sup (pi (X,i)) by A1; A6: x . i in pi (X,i) by ; ex_sup_of pi (X,i),J . i by A3; then f . i is_>=_than pi (X,i) by ; hence x . i <= f . i by A6; :: thesis: verum end; hence x <= f by WAYBEL_3:28; :: thesis: verum end; let g be Element of (); :: thesis: ( X is_<=_than g implies f <= g ) assume A7: X is_<=_than g ; :: thesis: f <= g now :: thesis: for i being Element of I holds f . i <= g . i let i be Element of I; :: thesis: f . i <= g . i A8: ex_sup_of pi (X,i),J . i by A3; A9: g . i is_>=_than pi (X,i) proof let a be Element of (J . i); :: according to LATTICE3:def 9 :: thesis: ( not a in pi (X,i) or a <= g . i ) assume a in pi (X,i) ; :: thesis: a <= g . i then consider h being Function such that A10: h in X and A11: a = h . i by CARD_3:def 6; reconsider h = h as Element of () by A10; h <= g by ; hence a <= g . i by ; :: thesis: verum end; f . i = sup (pi (X,i)) by A1; hence f . i <= g . i by ; :: thesis: verum end; hence f <= g by WAYBEL_3:28; :: thesis: verum end; Lm2: now :: thesis: for I being non empty set for J being non-Empty Poset-yielding ManySortedSet of I for X being Subset of () st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds ex f being Element of () st ( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of () st X is_>=_than g holds f >= g ) ) let I be non empty set ; :: thesis: for J being non-Empty Poset-yielding ManySortedSet of I for X being Subset of () st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds ex f being Element of () st ( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of () st X is_>=_than g holds f >= g ) ) let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis: for X being Subset of () st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds ex f being Element of () st ( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of () st X is_>=_than g holds f >= g ) ) let X be Subset of (); :: thesis: ( ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) implies ex f being Element of () st ( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of () st X is_>=_than g holds f >= g ) ) ) deffunc H1( Element of I) -> Element of the carrier of (J .$1) = inf (pi (X,\$1));
consider f being ManySortedSet of I such that
A1: for i being Element of I holds f . i = H1(i) from PBOOLE:sch 5();
A2: now :: thesis: for i being Element of I holds f . i is Element of (J . i)
let i be Element of I; :: thesis: f . i is Element of (J . i)
f . i = inf (pi (X,i)) by A1;
hence f . i is Element of (J . i) ; :: thesis: verum
end;
dom f = I by PARTFUN1:def 2;
then reconsider f = f as Element of () by ;
assume A3: for i being Element of I holds ex_inf_of pi (X,i),J . i ; :: thesis: ex f being Element of () st
( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of () st X is_>=_than g holds
f >= g ) )

take f = f; :: thesis: ( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of () st X is_>=_than g holds
f >= g ) )

thus for i being Element of I holds f . i = inf (pi (X,i)) by A1; :: thesis: ( f is_<=_than X & ( for g being Element of () st X is_>=_than g holds
f >= g ) )

thus f is_<=_than X :: thesis: for g being Element of () st X is_>=_than g holds
f >= g
proof
let x be Element of (); :: according to LATTICE3:def 8 :: thesis: ( not x in X or f <= x )
assume A4: x in X ; :: thesis: f <= x
now :: thesis: for i being Element of I holds x . i >= f . i
let i be Element of I; :: thesis: x . i >= f . i
A5: f . i = inf (pi (X,i)) by A1;
A6: x . i in pi (X,i) by ;
ex_inf_of pi (X,i),J . i by A3;
then f . i is_<=_than pi (X,i) by ;
hence x . i >= f . i by A6; :: thesis: verum
end;
hence f <= x by WAYBEL_3:28; :: thesis: verum
end;
let g be Element of (); :: thesis: ( X is_>=_than g implies f >= g )
assume A7: X is_>=_than g ; :: thesis: f >= g
now :: thesis: for i being Element of I holds f . i >= g . i
let i be Element of I; :: thesis: f . i >= g . i
A8: ex_inf_of pi (X,i),J . i by A3;
A9: g . i is_<=_than pi (X,i)
proof
let a be Element of (J . i); :: according to LATTICE3:def 8 :: thesis: ( not a in pi (X,i) or g . i <= a )
assume a in pi (X,i) ; :: thesis: g . i <= a
then consider h being Function such that
A10: h in X and
A11: a = h . i by CARD_3:def 6;
reconsider h = h as Element of () by A10;
h >= g by ;
hence a >= g . i by ; :: thesis: verum
end;
f . i = inf (pi (X,i)) by A1;
hence f . i >= g . i by ; :: thesis: verum
end;
hence f >= g by WAYBEL_3:28; :: thesis: verum
end;

theorem Th28: :: YELLOW16:29
for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for f being Element of ()
for X being Subset of () holds
( f is_>=_than X iff for i being Element of I holds f . i is_>=_than pi (X,i) )
proof end;

theorem Th29: :: YELLOW16:30
for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for f being Element of ()
for X being Subset of () holds
( f is_<=_than X iff for i being Element of I holds f . i is_<=_than pi (X,i) )
proof end;

theorem Th30: :: YELLOW16:31
for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of () holds
( ex_sup_of X, product J iff for i being Element of I holds ex_sup_of pi (X,i),J . i )
proof end;

theorem Th31: :: YELLOW16:32
for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of () holds
( ex_inf_of X, product J iff for i being Element of I holds ex_inf_of pi (X,i),J . i )
proof end;

theorem Th32: :: YELLOW16:33
for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of () st ex_sup_of X, product J holds
for i being Element of I holds (sup X) . i = sup (pi (X,i))
proof end;

theorem Th33: :: YELLOW16:34
for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of () st ex_inf_of X, product J holds
for i being Element of I holds (inf X) . i = inf (pi (X,i))
proof end;

theorem Th34: :: YELLOW16:35
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
for X being directed Subset of ()
for i being Element of I holds pi (X,i) is directed
proof end;

theorem Th35: :: YELLOW16:36
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 end;

theorem Th36: :: YELLOW16:37
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 end;

theorem :: YELLOW16:38
for L being non empty RelStr
for S being non empty SubRelStr of L
for X being set holds S |^ X is SubRelStr of L |^ X
proof end;

theorem Th38: :: YELLOW16:39
for L being non empty RelStr
for S being non empty full SubRelStr of L
for X being set holds S |^ X is full SubRelStr of L |^ X
proof end;

definition
let S, T be non empty RelStr ;
let X be set ;
pred S inherits_sup_of X,T means :: YELLOW16:def 6
( ex_sup_of X,T implies "\/" (X,T) in the carrier of S );
pred S inherits_inf_of X,T means :: YELLOW16:def 7
( ex_inf_of X,T implies "/\" (X,T) in the carrier of S );
end;

:: deftheorem defines inherits_sup_of YELLOW16:def 6 :
for S, T being non empty RelStr
for X being set holds
( S inherits_sup_of X,T iff ( ex_sup_of X,T implies "\/" (X,T) in the carrier of S ) );

:: deftheorem defines inherits_inf_of YELLOW16:def 7 :
for S, T being non empty RelStr
for X being set holds
( S inherits_inf_of X,T iff ( ex_inf_of X,T implies "/\" (X,T) in the carrier of S ) );

theorem :: YELLOW16:40
for T being non empty transitive RelStr
for S being non empty full 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) ) ) ) by YELLOW_0:64;

theorem :: YELLOW16:41
for T being non empty transitive RelStr
for S being non empty full 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) ) ) ) by YELLOW_0:63;

scheme :: YELLOW16:sch 1
ProductSupsInheriting{ F1() -> non empty set , F2() -> non-Empty Poset-yielding ManySortedSet of F1(), F3() -> non-Empty Poset-yielding ManySortedSet of F1(), P1[ set , set ] } :
for X being Subset of (product F3()) st P1[X, product F3()] holds
product F3() inherits_sup_of X, product F2()
provided
A1: for X being Subset of (product F3()) st P1[X, product F3()] holds
for i being Element of F1() holds P1[ pi (X,i),F3() . i] and
A2: for i being Element of F1() holds F3() . i is full SubRelStr of F2() . i and
A3: for i being Element of F1()
for X being Subset of (F3() . i) st P1[X,F3() . i] holds
F3() . i inherits_sup_of X,F2() . i
proof end;

scheme :: YELLOW16:sch 2
PowerSupsInheriting{ F1() -> non empty set , F2() -> non empty Poset, F3() -> non empty full SubRelStr of F2(), P1[ set , set ] } :
for X being Subset of (F3() |^ F1()) st P1[X,F3() |^ F1()] holds
F3() |^ F1() inherits_sup_of X,F2() |^ F1()
provided
A1: for X being Subset of (F3() |^ F1()) st P1[X,F3() |^ F1()] holds
for i being Element of F1() holds P1[ pi (X,i),F3()] and
A2: for X being Subset of F3() st P1[X,F3()] holds
F3() inherits_sup_of X,F2()
proof end;

scheme :: YELLOW16:sch 3
ProductInfsInheriting{ F1() -> non empty set , F2() -> non-Empty Poset-yielding ManySortedSet of F1(), F3() -> non-Empty Poset-yielding ManySortedSet of F1(), P1[ set , set ] } :
for X being Subset of (product F3()) st P1[X, product F3()] holds
product F3() inherits_inf_of X, product F2()
provided
A1: for X being Subset of (product F3()) st P1[X, product F3()] holds
for i being Element of F1() holds P1[ pi (X,i),F3() . i] and
A2: for i being Element of F1() holds F3() . i is full SubRelStr of F2() . i and
A3: for i being Element of F1()
for X being Subset of (F3() . i) st P1[X,F3() . i] holds
F3() . i inherits_inf_of X,F2() . i
proof end;

scheme :: YELLOW16:sch 4
PowerInfsInheriting{ F1() -> non empty set , F2() -> non empty Poset, F3() -> non empty full SubRelStr of F2(), P1[ set , set ] } :
for X being Subset of (F3() |^ F1()) st P1[X,F3() |^ F1()] holds
F3() |^ F1() inherits_inf_of X,F2() |^ F1()
provided
A1: for X being Subset of (F3() |^ F1()) st P1[X,F3() |^ F1()] holds
for i being Element of F1() holds P1[ pi (X,i),F3()] and
A2: for X being Subset of F3() st P1[X,F3()] holds
F3() inherits_inf_of X,F2()
proof end;

registration
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
not pi (X,i) is empty
proof end;
end;

theorem :: YELLOW16:42
for L being non empty Poset
for S being non empty full directed-sups-inheriting SubRelStr of L
for X being non empty set holds S |^ X is directed-sups-inheriting SubRelStr of L |^ X
proof end;

registration
let I be non empty set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
let X be non empty Subset of ();
let i be set ;
cluster pi (X,i) -> non empty ;
coherence
not pi (X,i) is empty
proof end;
end;

theorem Th42: :: YELLOW16:43
for X being non empty set
for L being non empty up-complete Poset holds L |^ X is up-complete
proof end;

registration
let L be non empty up-complete Poset;
let X be non empty set ;
cluster L |^ X -> up-complete ;
coherence
L |^ X is up-complete
by Th42;
end;

theorem Th43: :: YELLOW16:44
for T being non empty TopSpace
for S being non empty SubSpace of T
for f being Function of T,S st f is being_a_retraction holds
rng f = the carrier of S
proof end;

theorem :: YELLOW16:45
for T being non empty TopSpace
for S being non empty SubSpace of T
for f being continuous Function of T,S st f is being_a_retraction holds
f is idempotent
proof end;

theorem Th45: :: YELLOW16:46
for T being non empty TopSpace
for V being open Subset of T holds chi (V, the carrier of T) is continuous Function of T,Sierpinski_Space
proof end;

theorem :: YELLOW16:47
for T being non empty TopSpace
for 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 Function of Sierpinski_Space,T
proof end;

theorem :: YELLOW16:48
for T being non empty TopSpace
for 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 end;

theorem :: YELLOW16:49
for T being non empty 1-sorted
for V, W being Subset of T
for S being TopAugmentation of BoolePoset
for f, g being Function 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 end;

theorem :: YELLOW16:50
for L being non empty RelStr
for X being non empty set
for R being non empty full 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 end;

theorem :: YELLOW16:51
for S, T being non empty TopSpace holds
( S,T are_homeomorphic iff ex f being continuous Function of S,T ex g being continuous Function of T,S st
( f * g = id T & g * f = id S ) )
proof end;

theorem Th51: :: YELLOW16:52
for T, S, R being non empty TopSpace
for f being Function of T,S
for g being Function of S,T
for h being Function of S,R st f * g = id S & h is being_homeomorphism holds
(h * f) * (g * (h ")) = id R
proof end;

theorem Th52: :: YELLOW16:53
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 end;

theorem Th53: :: YELLOW16:54
for T being non empty TopSpace
for S being non empty SubSpace of T holds incl (S,T) is continuous
proof end;

theorem Th54: :: YELLOW16:55
for T being non empty TopSpace
for S being non empty SubSpace of T
for f being continuous Function of T,S st f is being_a_retraction holds
f * (incl (S,T)) = id S
proof end;

theorem Th55: :: YELLOW16:56
for T being non empty TopSpace
for S being non empty SubSpace of T st S is_a_retract_of T holds
S is_Retract_of T
proof end;

theorem :: YELLOW16:57
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 end;