:: by Grzegorz Bancerek

::

:: Received September 7, 1999

:: Copyright (c) 1999-2018 Association of Mizar Users

::$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

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

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 ;

ex b_{1} being Function of S,T st

( b_{1} is directed-sups-preserving & b_{1} is monotone )

end;
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 Function of ,;

existence ex b

( b

proof end;

registration

let S be 1-sorted ;

ex b_{1} being Function of S,S st b_{1} is idempotent

end;
cluster Relation-like the carrier of S -defined the carrier of S -valued Function-like V24( the carrier of S) quasi_total idempotent for Function of ,;

existence ex b

proof 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

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

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

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;

end;
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 );

( 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 );

( f is directed-sups-preserving Function of T,S & ex g being directed-sups-preserving Function of S,T st f * g = id S );

:: 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 ) );

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 ) );

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;

end;
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;

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;

ex f being Function of T,S st f is_an_UPS_retraction_of T,S;

:: 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 );

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 );

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

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

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

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

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

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 #)

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 )

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 ) ) )

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 ) )

( 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 )

( 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 (Image h) = id (Image h) & S, Image h are_isomorphic )

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 (Image h) = id (Image h) & 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 )

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

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

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

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

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

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

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 )

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

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

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;

end;
attr R is Poset-yielding means :Def5: :: YELLOW16:def 5

for x being set st x in rng R holds

x is Poset;

for x being set st x in rng R holds

x is Poset;

:: 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 );

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 b_{1} being Relation st b_{1} is Poset-yielding holds

( b_{1} is RelStr-yielding & b_{1} is reflexive-yielding )

end;
for b

( b

proof 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

end;
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;

registration

let I be set ;

ex b_{1} being ManySortedSet of I st

( b_{1} is Poset-yielding & b_{1} is non-Empty )

end;
cluster Relation-like I -defined Function-like V24(I) non-Empty Poset-yielding for ManySortedSet of ;

existence ex b

( b

proof end;

registration

let I be non empty set ;

let J be non-Empty Poset-yielding ManySortedSet of I;

coherence

( product J is transitive & product J is antisymmetric )

end;
let J be non-Empty Poset-yielding ManySortedSet of I;

coherence

( product J is transitive & product J is antisymmetric )

proof 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

end;
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;

Lm1: now :: thesis: for I being non empty set

for J being non-Empty Poset-yielding ManySortedSet of I

for X being Subset of (product J) st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds

f <= g ) )

for J being non-Empty Poset-yielding ManySortedSet of I

for X being Subset of (product J) st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) 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 (product J) st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds

f <= g ) )

let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis: for X being Subset of (product J) st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds

f <= g ) )

let X be Subset of (product J); :: thesis: ( ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) implies ex f being Element of (product J) st

( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds

f <= g ) ) )

deffunc H_{1}( 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 = H_{1}(i)
from PBOOLE:sch 5();

then reconsider f = 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 ; :: thesis: ex f being Element of (product J) st

( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) 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 (product J) 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 (product J) st X is_<=_than g holds

f <= g ) )

thus f is_>=_than X :: thesis: for g being Element of (product J) st X is_<=_than g holds

f <= g

assume A7: X is_<=_than g ; :: thesis: f <= g

end;
for X being Subset of (product J) st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds

f <= g ) )

let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis: for X being Subset of (product J) st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds

f <= g ) )

let X be Subset of (product J); :: thesis: ( ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) implies ex f being Element of (product J) st

( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds

f <= g ) ) )

deffunc H

consider f being ManySortedSet of I such that

A1: for i being Element of I holds f . i = H

A2: now :: thesis: for i being Element of I holds f . i is Element of (J . i)

dom f = I
by PARTFUN1:def 2;
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;
f . i = sup (pi (X,i)) by A1;

hence f . i is Element of (J . i) ; :: thesis: verum

then reconsider f = 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 ; :: thesis: ex f being Element of (product J) st

( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) 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 (product J) 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 (product J) st X is_<=_than g holds

f <= g ) )

thus f is_>=_than X :: thesis: for g being Element of (product J) st X is_<=_than g holds

f <= g

proof

let g be Element of (product J); :: thesis: ( X is_<=_than g implies f <= g )
let x be Element of (product J); :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= f )

assume A4: x in X ; :: thesis: x <= f

end;
assume A4: x in X ; :: thesis: x <= f

now :: thesis: for i being Element of I holds x . i <= f . i

hence
x <= f
by WAYBEL_3:28; :: thesis: verum
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 A4, CARD_3:def 6;

ex_sup_of pi (X,i),J . i by A3;

then f . i is_>=_than pi (X,i) by A5, YELLOW_0:30;

hence x . i <= f . i by A6; :: thesis: verum

end;
A5: f . i = sup (pi (X,i)) by A1;

A6: x . i in pi (X,i) by A4, CARD_3:def 6;

ex_sup_of pi (X,i),J . i by A3;

then f . i is_>=_than pi (X,i) by A5, YELLOW_0:30;

hence x . i <= f . i by A6; :: thesis: verum

assume A7: X is_<=_than g ; :: thesis: f <= g

now :: thesis: for i being Element of I holds f . i <= g . i

hence
f <= g
by WAYBEL_3:28; :: thesis: verum
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)

hence f . i <= g . i by A8, A9, YELLOW_0:30; :: thesis: verum

end;
A8: ex_sup_of pi (X,i),J . i by A3;

A9: g . i is_>=_than pi (X,i)

proof

f . i = sup (pi (X,i))
by A1;
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 (product J) by A10;

h <= g by A7, A10;

hence a <= g . i by A11, WAYBEL_3:28; :: thesis: verum

end;
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 (product J) by A10;

h <= g by A7, A10;

hence a <= g . i by A11, WAYBEL_3:28; :: thesis: verum

hence f . i <= g . i by A8, A9, YELLOW_0:30; :: thesis: verum

Lm2: now :: thesis: for I being non empty set

for J being non-Empty Poset-yielding ManySortedSet of I

for X being Subset of (product J) st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds

f >= g ) )

for J being non-Empty Poset-yielding ManySortedSet of I

for X being Subset of (product J) st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) 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 (product J) st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds

f >= g ) )

let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis: for X being Subset of (product J) st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds

f >= g ) )

let X be Subset of (product J); :: thesis: ( ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) implies ex f being Element of (product J) st

( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds

f >= g ) ) )

deffunc H_{1}( 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 = H_{1}(i)
from PBOOLE:sch 5();

then reconsider f = 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 ; :: thesis: ex f being Element of (product J) st

( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) 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 (product J) 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 (product J) st X is_>=_than g holds

f >= g ) )

thus f is_<=_than X :: thesis: for g being Element of (product J) st X is_>=_than g holds

f >= g

assume A7: X is_>=_than g ; :: thesis: f >= g

end;
for X being Subset of (product J) st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds

f >= g ) )

let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis: for X being Subset of (product J) st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds

ex f being Element of (product J) st

( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds

f >= g ) )

let X be Subset of (product J); :: thesis: ( ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) implies ex f being Element of (product J) st

( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds

f >= g ) ) )

deffunc H

consider f being ManySortedSet of I such that

A1: for i being Element of I holds f . i = H

A2: now :: thesis: for i being Element of I holds f . i is Element of (J . i)

dom f = I
by PARTFUN1:def 2;
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;
f . i = inf (pi (X,i)) by A1;

hence f . i is Element of (J . i) ; :: thesis: verum

then reconsider f = 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 ; :: thesis: ex f being Element of (product J) st

( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) 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 (product J) 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 (product J) st X is_>=_than g holds

f >= g ) )

thus f is_<=_than X :: thesis: for g being Element of (product J) st X is_>=_than g holds

f >= g

proof

let g be Element of (product J); :: thesis: ( X is_>=_than g implies f >= g )
let x be Element of (product J); :: according to LATTICE3:def 8 :: thesis: ( not x in X or f <= x )

assume A4: x in X ; :: thesis: f <= x

end;
assume A4: x in X ; :: thesis: f <= x

now :: thesis: for i being Element of I holds x . i >= f . i

hence
f <= x
by WAYBEL_3:28; :: thesis: verum
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 A4, CARD_3:def 6;

ex_inf_of pi (X,i),J . i by A3;

then f . i is_<=_than pi (X,i) by A5, YELLOW_0:31;

hence x . i >= f . i by A6; :: thesis: verum

end;
A5: f . i = inf (pi (X,i)) by A1;

A6: x . i in pi (X,i) by A4, CARD_3:def 6;

ex_inf_of pi (X,i),J . i by A3;

then f . i is_<=_than pi (X,i) by A5, YELLOW_0:31;

hence x . i >= f . i by A6; :: thesis: verum

assume A7: X is_>=_than g ; :: thesis: f >= g

now :: thesis: for i being Element of I holds f . i >= g . i

hence
f >= g
by WAYBEL_3:28; :: thesis: verum
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)

hence f . i >= g . i by A8, A9, YELLOW_0:31; :: thesis: verum

end;
A8: ex_inf_of pi (X,i),J . i by A3;

A9: g . i is_<=_than pi (X,i)

proof

f . i = inf (pi (X,i))
by A1;
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 (product J) by A10;

h >= g by A7, A10;

hence a >= g . i by A11, WAYBEL_3:28; :: thesis: verum

end;
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 (product J) by A10;

h >= g by A7, A10;

hence a >= g . i by A11, WAYBEL_3:28; :: thesis: verum

hence f . i >= g . i by A8, A9, YELLOW_0:31; :: thesis: verum

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 (product J)

for 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) )

for J being non-Empty Poset-yielding ManySortedSet of I

for f being Element of (product J)

for 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 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 (product J)

for 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) )

for J being non-Empty Poset-yielding ManySortedSet of I

for f being Element of (product J)

for 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 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 (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 )

for J being non-Empty Poset-yielding 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 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 (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 )

for J being non-Empty Poset-yielding 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 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 (product J) st ex_sup_of X, product J holds

for i being Element of I holds (sup X) . i = sup (pi (X,i))

for J being non-Empty Poset-yielding ManySortedSet of I

for X being Subset of (product J) 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 (product J) st ex_inf_of X, product J holds

for i being Element of I holds (inf X) . i = inf (pi (X,i))

for J being non-Empty Poset-yielding ManySortedSet of I

for X being Subset of (product J) 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 (product J)

for i being Element of I holds pi (X,i) is directed

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 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

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

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

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

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 ;

end;
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 );

( 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 );

( ex_inf_of X,T implies "/\" (X,T) in the carrier of S );

:: 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 ) );

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 ) );

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;

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;

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{ F_{1}() -> non empty set , F_{2}() -> non-Empty Poset-yielding ManySortedSet of F_{1}(), F_{3}() -> non-Empty Poset-yielding ManySortedSet of F_{1}(), P_{1}[ set , set ] } :

ProductSupsInheriting{ F

for X being Subset of (product F_{3}()) st P_{1}[X, product F_{3}()] holds

product F_{3}() inherits_sup_of X, product F_{2}()

providedproduct F

A1:
for X being Subset of (product F_{3}()) st P_{1}[X, product F_{3}()] holds

for i being Element of F_{1}() holds P_{1}[ pi (X,i),F_{3}() . i]
and

A2: for i being Element of F_{1}() holds F_{3}() . i is full SubRelStr of F_{2}() . i
and

A3: for i being Element of F_{1}()

for X being Subset of (F_{3}() . i) st P_{1}[X,F_{3}() . i] holds

F_{3}() . i inherits_sup_of X,F_{2}() . i

for i being Element of F

A2: for i being Element of F

A3: for i being Element of F

for X being Subset of (F

F

proof end;

scheme :: YELLOW16:sch 2

PowerSupsInheriting{ F_{1}() -> non empty set , F_{2}() -> non empty Poset, F_{3}() -> non empty full SubRelStr of F_{2}(), P_{1}[ set , set ] } :

PowerSupsInheriting{ F

for X being Subset of (F_{3}() |^ F_{1}()) st P_{1}[X,F_{3}() |^ F_{1}()] holds

F_{3}() |^ F_{1}() inherits_sup_of X,F_{2}() |^ F_{1}()

providedF

A1:
for X being Subset of (F_{3}() |^ F_{1}()) st P_{1}[X,F_{3}() |^ F_{1}()] holds

for i being Element of F_{1}() holds P_{1}[ pi (X,i),F_{3}()]
and

A2: for X being Subset of F_{3}() st P_{1}[X,F_{3}()] holds

F_{3}() inherits_sup_of X,F_{2}()

for i being Element of F

A2: for X being Subset of F

F

proof end;

scheme :: YELLOW16:sch 3

ProductInfsInheriting{ F_{1}() -> non empty set , F_{2}() -> non-Empty Poset-yielding ManySortedSet of F_{1}(), F_{3}() -> non-Empty Poset-yielding ManySortedSet of F_{1}(), P_{1}[ set , set ] } :

ProductInfsInheriting{ F

for X being Subset of (product F_{3}()) st P_{1}[X, product F_{3}()] holds

product F_{3}() inherits_inf_of X, product F_{2}()

providedproduct F

A1:
for X being Subset of (product F_{3}()) st P_{1}[X, product F_{3}()] holds

for i being Element of F_{1}() holds P_{1}[ pi (X,i),F_{3}() . i]
and

A2: for i being Element of F_{1}() holds F_{3}() . i is full SubRelStr of F_{2}() . i
and

A3: for i being Element of F_{1}()

for X being Subset of (F_{3}() . i) st P_{1}[X,F_{3}() . i] holds

F_{3}() . i inherits_inf_of X,F_{2}() . i

for i being Element of F

A2: for i being Element of F

A3: for i being Element of F

for X being Subset of (F

F

proof end;

scheme :: YELLOW16:sch 4

PowerInfsInheriting{ F_{1}() -> non empty set , F_{2}() -> non empty Poset, F_{3}() -> non empty full SubRelStr of F_{2}(), P_{1}[ set , set ] } :

PowerInfsInheriting{ F

for X being Subset of (F_{3}() |^ F_{1}()) st P_{1}[X,F_{3}() |^ F_{1}()] holds

F_{3}() |^ F_{1}() inherits_inf_of X,F_{2}() |^ F_{1}()

providedF

A1:
for X being Subset of (F_{3}() |^ F_{1}()) st P_{1}[X,F_{3}() |^ F_{1}()] holds

for i being Element of F_{1}() holds P_{1}[ pi (X,i),F_{3}()]
and

A2: for X being Subset of F_{3}() st P_{1}[X,F_{3}()] holds

F_{3}() inherits_inf_of X,F_{2}()

for i being Element of F

A2: for X being Subset of F

F

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 ;

coherence

not pi (X,i) is empty

end;
let L be non empty RelStr ;

let X be non empty Subset of (L |^ I);

let i be set ;

coherence

not pi (X,i) is empty

proof 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

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 (product J);

let i be set ;

coherence

not pi (X,i) is empty

end;
let J be RelStr-yielding non-Empty ManySortedSet of I;

let X be non empty Subset of (product J);

let i be set ;

coherence

not pi (X,i) is empty

proof end;

registration

let L be non empty up-complete Poset;

let X be non empty set ;

coherence

L |^ X is up-complete by Th42;

end;
let X be non empty set ;

coherence

L |^ X is up-complete by Th42;

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

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

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

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

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

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 {0}

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 )

for V, W being Subset of T

for S being TopAugmentation of BoolePoset {0}

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

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 ) )

( 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

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

R is_Retract_of T

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

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

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 ) )

( 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;