:: YELLOW16 semantic presentation

theorem :: YELLOW16:1

for a, b being Relation holds a * b = a (#) b

proof end;

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 f', g' being Function of X,the carrier of L st f' = f & g' = g & f <= g holds
f' <= g'

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 f', g' being Function of X,the carrier of L st f' = f & g' = g & f' <= g' holds
f <= g

proof end;

registration

let S be non empty RelStr ;
let T be non empty reflexive antisymmetric RelStr ;
cluster monotone directed-sups-preserving M5(the carrier of S,the carrier of T);
existence

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 idempotent M5(the carrier of S,the carrier of S);
existence

proof end;

end;

theorem Th5: :: 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 Th6: :: 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 :: YELLOW16:7

canceled;

theorem Th8: :: YELLOW16:8

for S, T being non empty 1-sorted
for f being Function of T,S
for g being Function of S,T st f * g = id S holds
rng f = the carrier of S

proof end;

theorem Th9: :: YELLOW16:9

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 :Def1: :: 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 :Def2: :: 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 Def1 defines is_a_retraction_of YELLOW16:def 1 :

:: deftheorem Def2 defines is_an_UPS_retraction_of YELLOW16:def 2 :

definition

let S, T be non empty Poset;
pred S is_a_retract_of T means :Def3: :: 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 :Def4: :: YELLOW16:def 4
ex f being Function of T,S st f is_an_UPS_retraction_of T,S;

end;

:: deftheorem Def3 defines is_a_retract_of YELLOW16:def 3 :

:: deftheorem Def4 defines is_an_UPS_retract_of YELLOW16:def 4 :

theorem Th10: :: YELLOW16:10

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 Th11: :: YELLOW16:11

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 Th12: :: YELLOW16:12

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 Th13: :: YELLOW16:13

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 Th14: :: YELLOW16:14

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 Th15: :: YELLOW16:15

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 Th16: :: YELLOW16:16

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 Th17: :: YELLOW16:17

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 Th18: :: YELLOW16:18

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

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 Th20: :: YELLOW16:20

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 )

proof end;

theorem Th21: :: YELLOW16:21

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 Th22: :: YELLOW16:22

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 Th23: :: YELLOW16:23

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 Th24: :: YELLOW16:24

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

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

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

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 Th28: :: YELLOW16:28

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

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

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 :

registration

cluster Poset-yielding -> RelStr-yielding reflexive-yielding set ;
coherence

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

proof end;

end;

registration

let X be set ;
let S be Poset;
cluster K104(X,S) -> Poset-yielding ;
coherence

proof end;

end;

registration

let I be set ;
cluster RelStr-yielding non-Empty reflexive-yielding Poset-yielding ManySortedSet of I;
existence

proof end;

end;

registration

let I be non empty set ;
let J be non-Empty Poset-yielding ManySortedSet of I;
cluster product J -> transitive antisymmetric ;
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

proof end;

end;

Lm1: now

let I be non empty set ; :: thesis:
let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis:
let X be Subset of (product J); :: thesis:
deffunc H₁( 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₁(i) from PBOOLE:sch 5( R );
A2: dom f = I by PBOOLE:def 3;

now

let i be Element of I; :: thesis:
f . i = sup (pi X,i) by A1;
hence f . i is Element of (J . i) ; :: thesis:

end;

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:
take f = f; :: thesis:
thus for i being Element of I holds f . i = sup (pi X,i) by A1; :: thesis:
thus f is_>=_than X :: thesis:

proof

let x be Element of (product J); :: according to LATTICE3:def 9 :: thesis:
assume A4: x in X ; :: thesis:

now

let i be Element of I; :: thesis:
( 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; :: thesis:

end;

hence x <= f by WAYBEL_3:28; :: thesis:

end;

let g be Element of (product J); :: thesis:
assume A5: X is_<=_than g ; :: thesis:

now

let i be Element of I; :: thesis:
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); :: according to LATTICE3:def 9 :: thesis:
assume a in pi X,i ; :: thesis:
then consider h being Function such that
A7: ( h in X & a = h . i ) by CARD_3:def 6;
reconsider h = 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; :: thesis:

end;

hence f . i <= g . i by A6, YELLOW_0:30; :: thesis:

end;

hence f <= g by WAYBEL_3:28; :: thesis:

end;

Lm2: now

let I be non empty set ; :: thesis:
let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis:
let X be Subset of (product J); :: thesis:
deffunc H₁( 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₁(i) from PBOOLE:sch 5( R );
A2: dom f = I by PBOOLE:def 3;

now

let i be Element of I; :: thesis:
f . i = inf (pi X,i) by A1;
hence f . i is Element of (J . i) ; :: thesis:

end;

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:
take f = f; :: thesis:
thus for i being Element of I holds f . i = inf (pi X,i) by A1; :: thesis:
thus f is_<=_than X :: thesis:

proof

let x be Element of (product J); :: according to LATTICE3:def 8 :: thesis:
assume A4: x in X ; :: thesis:

now

let i be Element of I; :: thesis:
( 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; :: thesis:

end;

hence f <= x by WAYBEL_3:28; :: thesis:

end;

let g be Element of (product J); :: thesis:
assume A5: X is_>=_than g ; :: thesis:

now

let i be Element of I; :: thesis:
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); :: according to LATTICE3:def 8 :: thesis:
assume a in pi X,i ; :: thesis:
then consider h being Function such that
A7: ( h in X & a = h . i ) by CARD_3:def 6;
reconsider h = 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; :: thesis:

end;

hence f . i >= g . i by A6, YELLOW_0:31; :: thesis:

end;

hence f >= g by WAYBEL_3:28; :: thesis:

end;

theorem Th31: :: YELLOW16:31

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 )

proof end;

theorem Th32: :: YELLOW16:32

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 )

proof end;

theorem Th33: :: 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) 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 Th34: :: 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) 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 Th35: :: YELLOW16:35

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)

proof end;

theorem Th36: :: YELLOW16:36

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)

proof end;

theorem Th37: :: YELLOW16:37

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

theorem Th38: :: YELLOW16:38

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 Th39: :: YELLOW16:39

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

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 Th41: :: YELLOW16:41

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 :Def6: :: YELLOW16:def 6
( ex_sup_of X,T implies "\/" X,T in the carrier of S );
pred S inherits_inf_of X,T means :Def7: :: YELLOW16:def 7
( ex_inf_of X,T implies "/\" X,T in the carrier of S );

end;

:: deftheorem Def6 defines inherits_sup_of YELLOW16:def 6 :

:: deftheorem Def7 defines inherits_inf_of YELLOW16:def 7 :

theorem Th42: :: YELLOW16:42

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

proof end;

theorem :: YELLOW16:43

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

proof end;

scheme :: YELLOW16:sch 1
ProductSupsInheriting{ F₁() -> non empty set , F₂() -> non-Empty Poset-yielding ManySortedSet of F₁(), F₃() -> non-Empty Poset-yielding ManySortedSet of F₁(), P₁[ set , set ] } :

for X being Subset of (product F₃()) st P₁[X, product F₃()] holds
product F₃() inherits_sup_of X, product F₂()

provided

A1: for X being Subset of (product F₃()) st P₁[X, product F₃()] holds
for i being Element of F₁() holds P₁[ pi X,i,F₃() . i] and
A2: for i being Element of F₁() holds F₃() . i is full SubRelStr of F₂() . i and
A3: for i being Element of F₁()
for X being Subset of (F₃() . i) st P₁[X,F₃() . i] holds
F₃() . i inherits_sup_of X,F₂() . i

proof end;

scheme :: YELLOW16:sch 2
PowerSupsInheriting{ F₁() -> non empty set , F₂() -> non empty Poset, F₃() -> non empty full SubRelStr of F₂(), P₁[ set , set ] } :

for X being Subset of (F₃() |^ F₁()) st P₁[X,F₃() |^ F₁()] holds
F₃() |^ F₁() inherits_sup_of X,F₂() |^ F₁()

provided

A1: for X being Subset of (F₃() |^ F₁()) st P₁[X,F₃() |^ F₁()] holds
for i being Element of F₁() holds P₁[ pi X,i,F₃()] and
A2: for X being Subset of F₃() st P₁[X,F₃()] holds
F₃() inherits_sup_of X,F₂()

proof end;

scheme :: YELLOW16:sch 3
ProductInfsInheriting{ F₁() -> non empty set , F₂() -> non-Empty Poset-yielding ManySortedSet of F₁(), F₃() -> non-Empty Poset-yielding ManySortedSet of F₁(), P₁[ set , set ] } :

for X being Subset of (product F₃()) st P₁[X, product F₃()] holds
product F₃() inherits_inf_of X, product F₂()

provided

proof end;

scheme :: YELLOW16:sch 4
PowerInfsInheriting{ F₁() -> non empty set , F₂() -> non empty Poset, F₃() -> non empty full SubRelStr of F₂(), P₁[ set , set ] } :

for X being Subset of (F₃() |^ F₁()) st P₁[X,F₃() |^ F₁()] holds
F₃() |^ F₁() inherits_inf_of X,F₂() |^ F₁()

provided

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

proof end;

end;

theorem :: YELLOW16:44

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 (product J);
let i be set ;
cluster pi X,i -> non empty ;
coherence

proof end;

end;

theorem Th45: :: YELLOW16:45

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 by Th45;

end;

registration

let T be TopSpace;
cluster the topology of T -> non empty ;
coherence by PRE_TOPC:def 1;

end;

theorem Th46: :: YELLOW16:46

for T being non empty TopSpace
for S being non empty SubSpace of T
for f being Function of T,S st f is_a_retraction holds
rng f = the carrier of S

proof end;

theorem :: YELLOW16:47

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_a_retraction holds
f is idempotent

proof end;

theorem Th48: :: YELLOW16:48

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

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

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

for T being non empty 1-sorted
for V, W being Subset of T
for S being TopAugmentation of BoolePoset 1
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:52

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

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 Th54: :: YELLOW16:54

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_homeomorphism holds
(h * f) * (g * (h " )) = id R

proof end;

theorem Th55: :: YELLOW16:55

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 Th56: :: YELLOW16:56

for T being non empty TopSpace
for S being non empty SubSpace of T holds incl S,T is continuous

proof end;

theorem Th57: :: YELLOW16:57

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_a_retraction holds
f * (incl S,T) = id S

proof end;

theorem Th58: :: YELLOW16:58

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

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;