:: WAYBEL34 semantic presentation

registration

let c₁, c₂ be complete LATTICE;
cluster Galois Connection of a₁,a₂;
existence

proof end;

end;

theorem Th1: :: WAYBEL34:1

for b₁, b₂, b₃, b₄ being non empty RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₃,the InternalRel of b₃ #) & RelStr(# the carrier of b₂,the InternalRel of b₂ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) holds
for b₅ being Connection of b₁,b₂
for b₆ being Connection of b₃,b₄ st b₅ = b₆ & b₅ is Galois holds
b₆ is Galois

proof end;

definition

let c₁, c₂ be LATTICE;
let c₃ be Function of c₁,c₂;
assume ( c₁ is complete & c₂ is complete & c₃ is infs-preserving ) ;
then E2: c₃ has_a_lower_adjoint by WAYBEL_1:17;
func LowerAdj c₃ -> Function of a₂,a₁ means :Def1: :: WAYBEL34:def 1
[a₃,a₄] is Galois;
uniqueness

proof end;

existence by E2, WAYBEL_1:def 11;

end;

:: deftheorem Def1 defines LowerAdj WAYBEL34:def 1 :

definition

let c₁, c₂ be LATTICE;
let c₃ be Function of c₂,c₁;
assume ( c₁ is complete & c₂ is complete & c₃ is sups-preserving ) ;
then E3: c₃ has_an_upper_adjoint by WAYBEL_1:18;
func UpperAdj c₃ -> Function of a₁,a₂ means :Def2: :: WAYBEL34:def 2
[a₄,a₃] is Galois;
existence by E3, WAYBEL_1:def 12;
correctness

proof end;

end;

:: deftheorem Def2 defines UpperAdj WAYBEL34:def 2 :

E4: now

let c₁, c₂ be LATTICE;
assume ( c₁ is complete & c₂ is complete ) ;
then reconsider c₃ = c₁, c₄ = c₂ as complete LATTICE ;
let c₅ be Function of c₁,c₂;
assume c₅ is infs-preserving ;
then reconsider c₆ = c₅ as infs-preserving Function of c₃,c₄ ;
[c₆,(LowerAdj c₆)] is Galois by Def1;
then ( LowerAdj c₆ is lower_adjoint & LowerAdj c₆ is monotone ) by WAYBEL_1:9, WAYBEL_1:def 12;
hence ( LowerAdj c₅ is monotone & LowerAdj c₅ is lower_adjoint & LowerAdj c₅ is sups-preserving ) by WAYBEL_1:18;

end;

E5: now

let c₁, c₂ be LATTICE;
assume ( c₁ is complete & c₂ is complete ) ;
then reconsider c₃ = c₁, c₄ = c₂ as complete LATTICE ;
let c₅ be Function of c₁,c₂;
assume c₅ is sups-preserving ;
then reconsider c₆ = c₅ as sups-preserving Function of c₃,c₄ ;
[(UpperAdj c₆),c₆] is Galois by Def2;
then ( UpperAdj c₆ is upper_adjoint & UpperAdj c₆ is monotone ) by WAYBEL_1:9, WAYBEL_1:def 11;
hence ( UpperAdj c₅ is monotone & UpperAdj c₅ is upper_adjoint & UpperAdj c₅ is infs-preserving ) by WAYBEL_1:17;

end;

registration

let c₁, c₂ be complete LATTICE;
let c₃ be infs-preserving Function of c₁,c₂;
cluster LowerAdj a₃ -> lower_adjoint ;
coherence by Lemma4;

end;

registration

let c₁, c₂ be complete LATTICE;
let c₃ be sups-preserving Function of c₂,c₁;
cluster UpperAdj a₃ -> upper_adjoint ;
coherence by Lemma5;

end;

theorem Th2: :: WAYBEL34:2

for b₁, b₂ being complete LATTICE
for b₃ being infs-preserving Function of b₁,b₂
for b₄ being Element of b₂ holds (LowerAdj b₃) . b₄ = inf (b₃ " (uparrow b₄))

proof end;

theorem Th3: :: WAYBEL34:3

for b₁, b₂ being complete LATTICE
for b₃ being sups-preserving Function of b₂,b₁
for b₄ being Element of b₁ holds (UpperAdj b₃) . b₄ = sup (b₃ " (downarrow b₄))

proof end;

definition

let c₁, c₂ be RelStr ;
let c₃ be Function of the carrier of c₁,the carrier of c₂;
func c₃ opp -> Function of (a₁ opp ),(a₂ opp ) equals :: WAYBEL34:def 3
a₃;
coherence ;

end;

:: deftheorem Def3 defines opp WAYBEL34:def 3 :

registration

let c₁, c₂ be complete LATTICE;
let c₃ be infs-preserving Function of c₁,c₂;
cluster a₃ opp -> lower_adjoint ;
coherence

proof end;

end;

registration

let c₁, c₂ be complete LATTICE;
let c₃ be sups-preserving Function of c₁,c₂;
cluster a₃ opp -> upper_adjoint ;
coherence

proof end;

end;

theorem Th4: :: WAYBEL34:4

for b₁, b₂ being complete LATTICE
for b₃ being infs-preserving Function of b₁,b₂ holds LowerAdj b₃ = UpperAdj (b₃ opp )

proof end;

theorem Th5: :: WAYBEL34:5

for b₁, b₂ being complete LATTICE
for b₃ being sups-preserving Function of b₁,b₂ holds LowerAdj (b₃ opp ) = UpperAdj b₃

proof end;

theorem Th6: :: WAYBEL34:6

for b₁ being non empty RelStr holds [(id b₁),(id b₁)] is Galois

proof end;

theorem Th7: :: WAYBEL34:7

for b₁ being complete LATTICE holds
( LowerAdj (id b₁) = id b₁ & UpperAdj (id b₁) = id b₁ )

proof end;

theorem Th8: :: WAYBEL34:8

for b₁, b₂, b₃ being complete LATTICE
for b₄ being infs-preserving Function of b₁,b₂
for b₅ being infs-preserving Function of b₂,b₃ holds LowerAdj (b₅ * b₄) = (LowerAdj b₄) * (LowerAdj b₅)

proof end;

theorem Th9: :: WAYBEL34:9

for b₁, b₂, b₃ being complete LATTICE
for b₄ being sups-preserving Function of b₁,b₂
for b₅ being sups-preserving Function of b₂,b₃ holds UpperAdj (b₅ * b₄) = (UpperAdj b₄) * (UpperAdj b₅)

proof end;

theorem Th10: :: WAYBEL34:10

for b₁, b₂ being complete LATTICE
for b₃ being infs-preserving Function of b₁,b₂ holds UpperAdj (LowerAdj b₃) = b₃

proof end;

theorem Th11: :: WAYBEL34:11

for b₁, b₂ being complete LATTICE
for b₃ being sups-preserving Function of b₁,b₂ holds LowerAdj (UpperAdj b₃) = b₃

proof end;

theorem Th12: :: WAYBEL34:12

for b₁ being non empty AltCatStr
for b₂, b₃, b₄ being set st b₄ in the Arrows of b₁ . b₂,b₃ holds
ex b₅, b₆ being object of b₁ st
( b₅ = b₂ & b₆ = b₃ & b₄ in <^b₅,b₆^> & b₄ is Morphism of b₅,b₆ )

proof end;

definition

let c₁ be non empty set ;
defpred S₁[ LATTICE] means a₁ is complete;
defpred S₂[ LATTICE, LATTICE, Function of a₁,a₂] means a₃ is infs-preserving;
given c₂ being Element of c₁ such that E13: not c₂ is empty ;
func c₁ -INF_category -> strict lattice-wise category means :Def4: :: WAYBEL34:def 4
( ( for b₁ being LATTICE holds
( b₁ is object of a₂ iff ( b₁ is strict & b₁ is complete & the carrier of b₁ in a₁ ) ) ) & ( for b₁, b₂ being object of a₂
for b₃ being monotone Function of (latt b₁),(latt b₂) holds
( b₃ in <^b₁,b₂^> iff b₃ is infs-preserving ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines -INF_category WAYBEL34:def 4 :

Lemma14: for b₁ being with_non-empty_element set
for b₂, b₃ being LATTICE
for b₄ being Function of b₂,b₃ holds
( b₄ in the Arrows of (b₁ -INF_category ) . b₂,b₃ iff ( b₂ in the carrier of (b₁ -INF_category ) & b₃ in the carrier of (b₁ -INF_category ) & b₂ is complete & b₃ is complete & b₄ is infs-preserving ) )

proof end;

definition

let c₁ be non empty set ;
defpred S₁[ LATTICE] means a₁ is complete;
defpred S₂[ LATTICE, LATTICE, Function of a₁,a₂] means a₃ is sups-preserving;
given c₂ being Element of c₁ such that E15: not c₂ is empty ;
func c₁ -SUP_category -> strict lattice-wise category means :Def5: :: WAYBEL34:def 5
( ( for b₁ being LATTICE holds
( b₁ is object of a₂ iff ( b₁ is strict & b₁ is complete & the carrier of b₁ in a₁ ) ) ) & ( for b₁, b₂ being object of a₂
for b₃ being monotone Function of (latt b₁),(latt b₂) holds
( b₃ in <^b₁,b₂^> iff b₃ is sups-preserving ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines -SUP_category WAYBEL34:def 5 :

Lemma16: for b₁ being with_non-empty_element set
for b₂, b₃ being LATTICE
for b₄ being Function of b₂,b₃ holds
( b₄ in the Arrows of (b₁ -SUP_category ) . b₂,b₃ iff ( b₂ in the carrier of (b₁ -SUP_category ) & b₃ in the carrier of (b₁ -SUP_category ) & b₂ is complete & b₃ is complete & b₄ is sups-preserving ) )

proof end;

registration

let c₁ be with_non-empty_element set ;
cluster a₁ -INF_category -> strict lattice-wise with_complete_lattices ;
coherence

proof end;

cluster a₁ -SUP_category -> strict lattice-wise with_complete_lattices ;
coherence

proof end;

end;

theorem Th13: :: WAYBEL34:13

for b₁ being with_non-empty_element set
for b₂ being LATTICE holds
( b₂ is object of (b₁ -INF_category ) iff ( b₂ is strict & b₂ is complete & the carrier of b₂ in b₁ ) )

proof end;

theorem Th14: :: WAYBEL34:14

for b₁ being with_non-empty_element set
for b₂, b₃ being object of (b₁ -INF_category )
for b₄ being set holds
( b₄ in <^b₂,b₃^> iff b₄ is infs-preserving Function of (latt b₂),(latt b₃) )

proof end;

theorem Th15: :: WAYBEL34:15

for b₁ being with_non-empty_element set
for b₂ being LATTICE holds
( b₂ is object of (b₁ -SUP_category ) iff ( b₂ is strict & b₂ is complete & the carrier of b₂ in b₁ ) )

proof end;

theorem Th16: :: WAYBEL34:16

for b₁ being with_non-empty_element set
for b₂, b₃ being object of (b₁ -SUP_category )
for b₄ being set holds
( b₄ in <^b₂,b₃^> iff b₄ is sups-preserving Function of (latt b₂),(latt b₃) )

proof end;

theorem Th17: :: WAYBEL34:17

for b₁ being with_non-empty_element set holds the carrier of (b₁ -INF_category ) = the carrier of (b₁ -SUP_category )

proof end;

definition

let c₁ be with_non-empty_element set ;
set c₂ = c₁ -INF_category ;
set c₃ = c₁ -SUP_category ;
deffunc H₁( LATTICE) -> LATTICE = a₁;
deffunc H₂( LATTICE, LATTICE, Function of a₁,a₂) -> Function of a₂,a₁ = LowerAdj a₃;
defpred S₁[ LATTICE, LATTICE, Function of a₁,a₂] means ( a₁ is complete & a₂ is complete & a₃ is infs-preserving );
defpred S₂[ LATTICE, LATTICE, Function of a₁,a₂] means ( a₁ is complete & a₂ is complete & a₃ is sups-preserving );
E22: for b₁, b₂ being LATTICE
for b₃ being Function of b₁,b₂ holds
( b₃ in the Arrows of (c₁ -INF_category ) . b₁,b₂ iff ( b₁ in the carrier of (c₁ -INF_category ) & b₂ in the carrier of (c₁ -INF_category ) & S₁[b₁,b₂,b₃] ) ) by Lemma14;
E23: for b₁, b₂ being LATTICE
for b₃ being Function of b₁,b₂ holds
( b₃ in the Arrows of (c₁ -SUP_category ) . b₁,b₂ iff ( b₁ in the carrier of (c₁ -SUP_category ) & b₂ in the carrier of (c₁ -SUP_category ) & S₂[b₁,b₂,b₃] ) ) by Lemma16;
E24: for b₁ being LATTICE st b₁ in the carrier of (c₁ -INF_category ) holds
H₁(b₁) in the carrier of (c₁ -SUP_category ) by Th17;
E25: for b₁, b₂ being LATTICE
for b₃ being Function of b₁,b₂ st S₁[b₁,b₂,b₃] holds
( H₂(b₁,b₂,b₃) is Function of H₁(b₂),H₁(b₁) & S₂[H₁(b₂),H₁(b₁),H₂(b₁,b₂,b₃)] ) by Lemma4;

E26: now

let c₄ be LATTICE;
assume c₄ in the carrier of (c₁ -INF_category ) ;
then c₄ is complete by YELLOW21:def 5;
hence H₂(c₄,c₄, id c₄) = id H₁(c₄) by Th7;

end;

E27: for b₁, b₂, b₃ being LATTICE
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st S₁[b₁,b₂,b₄] & S₁[b₂,b₃,b₅] holds
H₂(b₁,b₃,b₅ * b₄) = H₂(b₁,b₂,b₄) * H₂(b₂,b₃,b₅) by Th8;
func c₁ LowerAdj -> strict contravariant Functor of a₁ -INF_category ,a₁ -SUP_category means :Def6: :: WAYBEL34:def 6
( ( for b₁ being object of (a₁ -INF_category ) holds a₂ . b₁ = latt b₁ ) & ( for b₁, b₂ being object of (a₁ -INF_category ) st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ holds a₂ . b₃ = LowerAdj (@ b₃) ) );
existence

proof end;

uniqueness

proof end;

deffunc H₃( LATTICE, LATTICE, Function of a₁,a₂) -> Function of a₂,a₁ = UpperAdj a₃;
E28: for b₁ being LATTICE st b₁ in the carrier of (c₁ -SUP_category ) holds
H₁(b₁) in the carrier of (c₁ -INF_category ) by Th17;
E29: for b₁, b₂ being LATTICE
for b₃ being Function of b₁,b₂ st S₂[b₁,b₂,b₃] holds
( H₃(b₁,b₂,b₃) is Function of H₁(b₂),H₁(b₁) & S₁[H₁(b₂),H₁(b₁),H₃(b₁,b₂,b₃)] ) by Lemma5;

E30: now

let c₄ be LATTICE;
assume c₄ in the carrier of (c₁ -SUP_category ) ;
then c₄ is complete by YELLOW21:def 5;
hence H₃(c₄,c₄, id c₄) = id H₁(c₄) by Th7;

end;

E31: for b₁, b₂, b₃ being LATTICE
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st S₂[b₁,b₂,b₄] & S₂[b₂,b₃,b₅] holds
H₃(b₁,b₃,b₅ * b₄) = H₃(b₁,b₂,b₄) * H₃(b₂,b₃,b₅) by Th9;
func c₁ UpperAdj -> strict contravariant Functor of a₁ -SUP_category ,a₁ -INF_category means :Def7: :: WAYBEL34:def 7
( ( for b₁ being object of (a₁ -SUP_category ) holds a₂ . b₁ = latt b₁ ) & ( for b₁, b₂ being object of (a₁ -SUP_category ) st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ holds a₂ . b₃ = UpperAdj (@ b₃) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines LowerAdj WAYBEL34:def 6 :

:: deftheorem Def7 defines UpperAdj WAYBEL34:def 7 :

registration

let c₁ be with_non-empty_element set ;
cluster a₁ LowerAdj -> strict contravariant bijective ;
coherence

proof end;

cluster a₁ UpperAdj -> strict contravariant bijective ;
coherence

proof end;

end;

theorem Th18: :: WAYBEL34:18

for b₁ being with_non-empty_element set holds
( (b₁ LowerAdj ) " = b₁ UpperAdj & (b₁ UpperAdj ) " = b₁ LowerAdj )

proof end;

theorem Th19: :: WAYBEL34:19

for b₁ being with_non-empty_element set holds
( (b₁ LowerAdj ) * (b₁ UpperAdj ) = id (b₁ -SUP_category ) & (b₁ UpperAdj ) * (b₁ LowerAdj ) = id (b₁ -INF_category ) )

proof end;

theorem Th20: :: WAYBEL34:20

for b₁ being with_non-empty_element set holds b₁ -INF_category ,b₁ -SUP_category are_anti-isomorphic

proof end;

theorem Th21: :: WAYBEL34:21

canceled;

theorem Th22: :: WAYBEL34:22

canceled;

theorem Th23: :: WAYBEL34:23

for b₁, b₂ being complete LATTICE
for b₃ being infs-preserving Function of b₁,b₂ holds
( b₃ is directed-sups-preserving iff for b₄ being Scott TopAugmentation of b₂
for b₅ being Scott TopAugmentation of b₁
for b₆ being open Subset of b₄ holds uparrow ((LowerAdj b₃) .: b₆) is open Subset of b₅ )

proof end;

definition

let c₁, c₂ be non empty reflexive RelStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is waybelow-preserving means :Def8: :: WAYBEL34:def 8
for b₁, b₂ being Element of a₁ st b₁ << b₂ holds
a₃ . b₁ << a₃ . b₂;

end;

:: deftheorem Def8 defines waybelow-preserving WAYBEL34:def 8 :

theorem Th24: :: WAYBEL34:24

for b₁, b₂ being complete LATTICE
for b₃ being infs-preserving Function of b₁,b₂ st b₃ is directed-sups-preserving holds
LowerAdj b₃ is waybelow-preserving

proof end;

theorem Th25: :: WAYBEL34:25

for b₁ being complete LATTICE
for b₂ being complete continuous LATTICE
for b₃ being infs-preserving Function of b₁,b₂ st LowerAdj b₃ is waybelow-preserving holds
b₃ is directed-sups-preserving

proof end;

definition

let c₁, c₂ be TopSpace;
let c₃ be Function of c₁,c₂;
attr a₃ is relatively_open means :Def9: :: WAYBEL34:def 9
for b₁ being open Subset of a₁ holds a₃ .: b₁ is open Subset of (a₂ | (rng a₃));

end;

:: deftheorem Def9 defines relatively_open WAYBEL34:def 9 :

theorem Th26: :: WAYBEL34:26

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ holds
( b₃ is relatively_open iff corestr b₃ is open )

proof end;

theorem Th27: :: WAYBEL34:27

for b₁, b₂ being complete LATTICE
for b₃ being infs-preserving Function of b₁,b₂
for b₄ being Scott TopAugmentation of b₂
for b₅ being Scott TopAugmentation of b₁
for b₆ being open Subset of b₄ holds (LowerAdj b₃) .: b₆ = (rng (LowerAdj b₃)) /\ (uparrow ((LowerAdj b₃) .: b₆))

proof end;

theorem Th28: :: WAYBEL34:28

for b₁, b₂ being complete LATTICE
for b₃ being infs-preserving Function of b₁,b₂
for b₄ being Scott TopAugmentation of b₂
for b₅ being Scott TopAugmentation of b₁ st ( for b₆ being open Subset of b₄ holds uparrow ((LowerAdj b₃) .: b₆) is open Subset of b₅ ) holds
for b₆ being Function of b₄,b₅ st b₆ = LowerAdj b₃ holds
b₆ is relatively_open

proof end;

registration

let c₁, c₂ be complete LATTICE;
let c₃ be sups-preserving Function of c₁,c₂;
cluster Image a₃ -> complete ;
coherence by YELLOW_2:36;

end;

theorem Th29: :: WAYBEL34:29

for b₁, b₂ being complete LATTICE
for b₃ being infs-preserving Function of b₁,b₂
for b₄ being Scott TopAugmentation of b₂
for b₅ being Scott TopAugmentation of b₁
for b₆ being Scott TopAugmentation of Image (LowerAdj b₃)
for b₇ being Function of b₄,b₅
for b₈ being Function of b₄,b₆ st b₇ = LowerAdj b₃ & b₈ = b₇ & b₇ is relatively_open holds
b₈ is open

proof end;

theorem Th30: :: WAYBEL34:30

for b₁, b₂, b₃, b₄ being TopStruct st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & TopStruct(# the carrier of b₃,the topology of b₃ #) = TopStruct(# the carrier of b₄,the topology of b₄ #) & b₃ is SubSpace of b₁ holds
b₄ is SubSpace of b₂

proof end;

theorem Th31: :: WAYBEL34:31

for b₁ being TopStruct holds b₁ | ([#] b₁) = TopStruct(# the carrier of b₁,the topology of b₁ #)

proof end;

theorem Th32: :: WAYBEL34:32

for b₁, b₂ being complete LATTICE
for b₃ being infs-preserving Function of b₁,b₂ st b₃ is one-to-one holds
for b₄ being Scott TopAugmentation of b₂
for b₅ being Scott TopAugmentation of b₁
for b₆ being Function of b₄,b₅ st b₆ = LowerAdj b₃ holds
( b₃ is directed-sups-preserving iff b₆ is open )

proof end;

registration

let c₁ be complete LATTICE;
let c₂ be projection Function of c₁,c₁;
cluster Image a₂ -> complete ;
coherence by WAYBEL_1:57;

end;

theorem Th33: :: WAYBEL34:33

for b₁ being complete LATTICE
for b₂ being kernel Function of b₁,b₁ holds
( corestr b₂ is infs-preserving & inclusion b₂ is sups-preserving & LowerAdj (corestr b₂) = inclusion b₂ & UpperAdj (inclusion b₂) = corestr b₂ )

proof end;

theorem Th34: :: WAYBEL34:34

for b₁ being complete LATTICE
for b₂ being kernel Function of b₁,b₁ holds
( b₂ is directed-sups-preserving iff corestr b₂ is directed-sups-preserving )

proof end;

theorem Th35: :: WAYBEL34:35

for b₁ being complete LATTICE
for b₂ being kernel Function of b₁,b₁ holds
( b₂ is directed-sups-preserving iff for b₃ being Scott TopAugmentation of Image b₂
for b₄ being Scott TopAugmentation of b₁
for b₅ being Subset of b₁ st b₅ is open Subset of b₃ holds
uparrow b₅ is open Subset of b₄ )

proof end;

theorem Th36: :: WAYBEL34:36

for b₁ being complete LATTICE
for b₂ being non empty full sups-inheriting SubRelStr of b₁
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₅ = b₃ & b₆ = b₄ & b₃ << b₄ holds
b₅ << b₆

proof end;

theorem Th37: :: WAYBEL34:37

for b₁ being complete LATTICE
for b₂ being kernel Function of b₁,b₁ st b₂ is directed-sups-preserving holds
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of (Image b₂) st b₅ = b₃ & b₆ = b₄ holds
( b₃ << b₄ iff b₅ << b₆ )

proof end;

theorem Th38: :: WAYBEL34:38

for b₁ being complete LATTICE
for b₂ being kernel Function of b₁,b₁ st Image b₂ is continuous & ( for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of (Image b₂) st b₅ = b₃ & b₆ = b₄ holds
( b₃ << b₄ iff b₅ << b₆ ) ) holds
b₂ is directed-sups-preserving

proof end;

theorem Th39: :: WAYBEL34:39

for b₁ being complete LATTICE
for b₂ being closure Function of b₁,b₁ holds
( corestr b₂ is sups-preserving & inclusion b₂ is infs-preserving & UpperAdj (corestr b₂) = inclusion b₂ & LowerAdj (inclusion b₂) = corestr b₂ )

proof end;

theorem Th40: :: WAYBEL34:40

for b₁ being complete LATTICE
for b₂ being closure Function of b₁,b₁ holds
( Image b₂ is directed-sups-inheriting iff inclusion b₂ is directed-sups-preserving )

proof end;

theorem Th41: :: WAYBEL34:41

for b₁ being complete LATTICE
for b₂ being closure Function of b₁,b₁ holds
( Image b₂ is directed-sups-inheriting iff for b₃ being Scott TopAugmentation of Image b₂
for b₄ being Scott TopAugmentation of b₁
for b₅ being Function of b₄,b₃ st b₅ = b₂ holds
b₅ is open )

proof end;

theorem Th42: :: WAYBEL34:42

for b₁ being complete LATTICE
for b₂ being closure Function of b₁,b₁ st Image b₂ is directed-sups-inheriting holds
corestr b₂ is waybelow-preserving

proof end;

theorem Th43: :: WAYBEL34:43

for b₁ being complete continuous LATTICE
for b₂ being closure Function of b₁,b₁ st corestr b₂ is waybelow-preserving holds
Image b₂ is directed-sups-inheriting

proof end;

definition

let c₁ be non empty set ;
set c₂ = c₁ -INF_category ;
defpred S₁[ set ] means verum;
defpred S₂[ object of (c₁ -INF_category ), object of (c₁ -INF_category ), Morphism of a₁,a₂] means @ a₃ is directed-sups-preserving;
E40: ex b₁ being object of (c₁ -INF_category ) st S₁[b₁] ;
E41: for b₁, b₂, b₃ being object of (c₁ -INF_category ) st S₁[b₁] & S₁[b₂] & S₁[b₃] & <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃ st S₂[b₁,b₂,b₄] & S₂[b₂,b₃,b₅] holds
S₂[b₁,b₃,b₅ * b₄]

proof end;

E42: for b₁ being object of (c₁ -INF_category ) st S₁[b₁] holds
S₂[b₁,b₁, idm b₁]

proof end;

func c₁ -INF(SC)_category -> non empty strict subcategory of a₁ -INF_category means :Def10: :: WAYBEL34:def 10
( ( for b₁ being object of (a₁ -INF_category ) holds b₁ is object of a₂ ) & ( for b₁, b₂ being object of (a₁ -INF_category )
for b₃, b₄ being object of a₂ st b₃ = b₁ & b₄ = b₂ & <^b₁,b₂^> <> {} holds
for b₅ being Morphism of b₁,b₂ holds
( b₅ in <^b₃,b₄^> iff @ b₅ is directed-sups-preserving ) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def10 defines -INF(SC)_category WAYBEL34:def 10 :

definition

let c₁ be with_non-empty_element set ;
E41: ex b₁ being non empty set st b₁ in c₁ by SETFAM_1:def 11;
set c₂ = c₁ -SUP_category ;
defpred S₁[ set ] means verum;
defpred S₂[ object of (c₁ -SUP_category ), object of (c₁ -SUP_category ), Morphism of a₁,a₂] means UpperAdj (@ a₃) is directed-sups-preserving;
E42: ex b₁ being object of (c₁ -SUP_category ) st S₁[b₁] ;
E43: for b₁, b₂, b₃ being object of (c₁ -SUP_category ) st S₁[b₁] & S₁[b₂] & S₁[b₃] & <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃ st S₂[b₁,b₂,b₄] & S₂[b₂,b₃,b₅] holds
S₂[b₁,b₃,b₅ * b₄]

proof end;

E44: for b₁ being object of (c₁ -SUP_category ) st S₁[b₁] holds
S₂[b₁,b₁, idm b₁]

proof end;

func c₁ -SUP(SO)_category -> non empty strict subcategory of a₁ -SUP_category means :Def11: :: WAYBEL34:def 11
( ( for b₁ being object of (a₁ -SUP_category ) holds b₁ is object of a₂ ) & ( for b₁, b₂ being object of (a₁ -SUP_category )
for b₃, b₄ being object of a₂ st b₃ = b₁ & b₄ = b₂ & <^b₁,b₂^> <> {} holds
for b₅ being Morphism of b₁,b₂ holds
( b₅ in <^b₃,b₄^> iff UpperAdj (@ b₅) is directed-sups-preserving ) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def11 defines -SUP(SO)_category WAYBEL34:def 11 :

theorem Th44: :: WAYBEL34:44

for b₁ being non empty RelStr
for b₂ being non empty reflexive antisymmetric RelStr
for b₃ being Element of b₂
for b₄ being non empty Subset of b₁ holds
( b₁ --> b₃ preserves_sup_of b₄ & b₁ --> b₃ preserves_inf_of b₄ )

proof end;

theorem Th45: :: WAYBEL34:45

for b₁ being non empty RelStr
for b₂ being non empty reflexive antisymmetric lower-bounded RelStr holds b₁ --> (Bottom b₂) is sups-preserving

proof end;

theorem Th46: :: WAYBEL34:46

for b₁ being non empty RelStr
for b₂ being non empty reflexive antisymmetric upper-bounded RelStr holds b₁ --> (Top b₂) is infs-preserving

proof end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive antisymmetric upper-bounded RelStr ;
cluster a₁ --> (Top a₂) -> infs-preserving directed-sups-preserving ;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster a₁ --> (Bottom a₂) -> sups-preserving filtered-infs-preserving ;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive antisymmetric upper-bounded RelStr ;
cluster infs-preserving directed-sups-preserving Relation of the carrier of a₁,the carrier of a₂;
existence

proof end;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster sups-preserving filtered-infs-preserving Relation of the carrier of a₁,the carrier of a₂;
existence

proof end;

end;

theorem Th47: :: WAYBEL34:47

for b₁ being with_non-empty_element set
for b₂ being LATTICE holds
( b₂ is object of (b₁ -INF(SC)_category ) iff ( b₂ is strict & b₂ is complete & the carrier of b₂ in b₁ ) )

proof end;

theorem Th48: :: WAYBEL34:48

for b₁ being with_non-empty_element set
for b₂, b₃ being object of (b₁ -INF(SC)_category )
for b₄ being set holds
( b₄ in <^b₂,b₃^> iff b₄ is infs-preserving directed-sups-preserving Function of (latt b₂),(latt b₃) )

proof end;

theorem Th49: :: WAYBEL34:49

for b₁ being with_non-empty_element set
for b₂ being LATTICE holds
( b₂ is object of (b₁ -SUP(SO)_category ) iff ( b₂ is strict & b₂ is complete & the carrier of b₂ in b₁ ) )

proof end;

theorem Th50: :: WAYBEL34:50

for b₁ being with_non-empty_element set
for b₂, b₃ being object of (b₁ -SUP(SO)_category )
for b₄ being set holds
( b₄ in <^b₂,b₃^> iff ex b₅ being sups-preserving Function of (latt b₂),(latt b₃) st
( b₅ = b₄ & UpperAdj b₅ is directed-sups-preserving ) )

proof end;

theorem Th51: :: WAYBEL34:51

for b₁ being with_non-empty_element set holds b₁ -INF(SC)_category = Intersect (b₁ -INF_category ),(b₁ -UPS_category )

proof end;

definition

let c₁ be with_non-empty_element set ;
defpred S₁[ object of (c₁ -INF(SC)_category )] means latt a₁ is continuous;
consider c₂ being non empty set such that
E48: c₂ in c₁ by SETFAM_1:def 11;
consider c₃ being upper-bounded well-ordering Order of c₂;
set c₄ = RelStr(# c₂,c₃ #);
func c₁ -CL_category -> non empty strict full subcategory of a₁ -INF(SC)_category means :Def12: :: WAYBEL34:def 12
for b₁ being object of (a₁ -INF(SC)_category ) holds
( b₁ is object of a₂ iff latt b₁ is continuous );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def12 defines -CL_category WAYBEL34:def 12 :

registration

let c₁ be with_non-empty_element set ;
cluster a₁ -CL_category -> non empty strict full with_complete_lattices ;
coherence ;

end;

theorem Th52: :: WAYBEL34:52

for b₁ being with_non-empty_element set
for b₂ being LATTICE st the carrier of b₂ in b₁ holds
( b₂ is object of (b₁ -CL_category ) iff ( b₂ is strict & b₂ is complete & b₂ is continuous ) )

proof end;

theorem Th53: :: WAYBEL34:53

for b₁ being with_non-empty_element set
for b₂, b₃ being object of (b₁ -CL_category )
for b₄ being set holds
( b₄ in <^b₂,b₃^> iff b₄ is infs-preserving directed-sups-preserving Function of (latt b₂),(latt b₃) )

proof end;

definition

let c₁ be with_non-empty_element set ;
defpred S₁[ object of (c₁ -SUP(SO)_category )] means latt a₁ is continuous;
consider c₂ being non empty set such that
E51: c₂ in c₁ by SETFAM_1:def 11;
consider c₃ being upper-bounded well-ordering Order of c₂;
set c₄ = RelStr(# c₂,c₃ #);
func c₁ -CL-opp_category -> non empty strict full subcategory of a₁ -SUP(SO)_category means :Def13: :: WAYBEL34:def 13
for b₁ being object of (a₁ -SUP(SO)_category ) holds
( b₁ is object of a₂ iff latt b₁ is continuous );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def13 defines -CL-opp_category WAYBEL34:def 13 :

theorem Th54: :: WAYBEL34:54

for b₁ being with_non-empty_element set
for b₂ being LATTICE st the carrier of b₂ in b₁ holds
( b₂ is object of (b₁ -CL-opp_category ) iff ( b₂ is strict & b₂ is complete & b₂ is continuous ) )

proof end;

theorem Th55: :: WAYBEL34:55

for b₁ being with_non-empty_element set
for b₂, b₃ being object of (b₁ -CL-opp_category )
for b₄ being set holds
( b₄ in <^b₂,b₃^> iff ex b₅ being sups-preserving Function of (latt b₂),(latt b₃) st
( b₅ = b₄ & UpperAdj b₅ is directed-sups-preserving ) )

proof end;

theorem Th56: :: WAYBEL34:56

for b₁ being with_non-empty_element set holds b₁ -INF(SC)_category ,b₁ -SUP(SO)_category are_anti-isomorphic_under b₁ LowerAdj

proof end;

theorem Th57: :: WAYBEL34:57

for b₁ being with_non-empty_element set holds b₁ -SUP(SO)_category ,b₁ -INF(SC)_category are_anti-isomorphic_under b₁ UpperAdj

proof end;

theorem Th58: :: WAYBEL34:58

for b₁ being with_non-empty_element set holds b₁ -CL_category ,b₁ -CL-opp_category are_anti-isomorphic_under b₁ LowerAdj

proof end;

theorem Th59: :: WAYBEL34:59

for b₁ being with_non-empty_element set holds b₁ -CL-opp_category ,b₁ -CL_category are_anti-isomorphic_under b₁ UpperAdj

proof end;

definition

let c₁, c₂ be non empty reflexive RelStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is compact-preserving means :: WAYBEL34:def 14
for b₁ being Element of a₁ st b₁ is compact holds
a₃ . b₁ is compact;

end;

:: deftheorem Def14 defines compact-preserving WAYBEL34:def 14 :

theorem Th60: :: WAYBEL34:60

for b₁, b₂ being complete LATTICE
for b₃ being sups-preserving Function of b₂,b₁ st b₃ is waybelow-preserving holds
b₃ is compact-preserving

proof end;

theorem Th61: :: WAYBEL34:61

for b₁, b₂ being complete LATTICE
for b₃ being sups-preserving Function of b₂,b₁ st b₂ is algebraic & b₃ is compact-preserving holds
b₃ is waybelow-preserving

proof end;

theorem Th62: :: WAYBEL34:62

for b₁, b₂, b₃ being non empty RelStr
for b₄ being Subset of b₁
for b₅ being Function of b₁,b₂
for b₆ being Function of b₂,b₃ st b₅ preserves_sup_of b₄ & b₆ preserves_sup_of b₅ .: b₄ holds
b₆ * b₅ preserves_sup_of b₄

proof end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is finite-sups-preserving means :: WAYBEL34:def 15
for b₁ being finite Subset of a₁ holds a₃ preserves_sup_of b₁;
attr a₃ is bottom-preserving means :Def16: :: WAYBEL34:def 16
a₃ preserves_sup_of {} a₁;

end;

:: deftheorem Def15 defines finite-sups-preserving WAYBEL34:def 15 :

:: deftheorem Def16 defines bottom-preserving WAYBEL34:def 16 :

theorem Th63: :: WAYBEL34:63

for b₁, b₂, b₃ being non empty RelStr
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is finite-sups-preserving & b₅ is finite-sups-preserving holds
b₅ * b₄ is finite-sups-preserving

proof end;

definition

let c₁, c₂ be non empty antisymmetric lower-bounded RelStr ;
let c₃ be Function of c₁,c₂;
redefine attr a₃ is bottom-preserving means :Def17: :: WAYBEL34:def 17
a₃ . (Bottom a₁) = Bottom a₂;
compatibility

proof end;

end;

:: deftheorem Def17 defines bottom-preserving WAYBEL34:def 17 :

definition

let c₁ be non empty RelStr ;
let c₂ be SubRelStr of c₁;
attr a₂ is finite-sups-inheriting means :Def18: :: WAYBEL34:def 18
for b₁ being finite Subset of a₂ st ex_sup_of b₁,a₁ holds
"\/" b₁,a₁ in the carrier of a₂;
attr a₂ is bottom-inheriting means :Def19: :: WAYBEL34:def 19
Bottom a₁ in the carrier of a₂;

end;

:: deftheorem Def18 defines finite-sups-inheriting WAYBEL34:def 18 :

:: deftheorem Def19 defines bottom-inheriting WAYBEL34:def 19 :

registration

let c₁, c₂ be non empty RelStr ;
cluster sups-preserving -> bottom-preserving Relation of the carrier of a₁,the carrier of a₂;
coherence

proof end;

end;

registration

let c₁ be non empty antisymmetric lower-bounded RelStr ;
cluster finite-sups-inheriting -> join-inheriting bottom-inheriting SubRelStr of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
cluster sups-inheriting -> finite-sups-inheriting SubRelStr of a₁;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty lower-bounded Poset;
cluster sups-preserving bottom-preserving Relation of the carrier of a₁,the carrier of a₂;
existence

proof end;

end;

registration

let c₁ be non empty antisymmetric lower-bounded RelStr ;
cluster full bottom-inheriting -> non empty lower-bounded full SubRelStr of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty antisymmetric lower-bounded RelStr ;
cluster non empty lower-bounded full join-inheriting sups-inheriting finite-sups-inheriting bottom-inheriting SubRelStr of a₁;
existence

proof end;

end;

theorem Th64: :: WAYBEL34:64

for b₁ being non empty antisymmetric lower-bounded RelStr
for b₂ being non empty full bottom-inheriting SubRelStr of b₁ holds Bottom b₂ = Bottom b₁

proof end;

registration

let c₁ be non empty lower-bounded with_suprema Poset;
cluster full join-inheriting bottom-inheriting -> non empty lower-bounded full join-inheriting finite-sups-inheriting bottom-inheriting SubRelStr of a₁;
coherence

proof end;

end;

theorem Th65: :: WAYBEL34:65

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₃ is finite-sups-preserving holds
( b₃ is join-preserving & b₃ is bottom-preserving )

proof end;

theorem Th66: :: WAYBEL34:66

for b₁, b₂ being lower-bounded with_suprema Poset
for b₃ being Function of b₁,b₂ st b₃ is join-preserving & b₃ is bottom-preserving holds
b₃ is finite-sups-preserving

proof end;

registration

let c₁, c₂ be non empty RelStr ;
cluster sups-preserving -> finite-sups-preserving Relation of the carrier of a₁,the carrier of a₂;
coherence

proof end;

cluster finite-sups-preserving -> join-preserving bottom-preserving Relation of the carrier of a₁,the carrier of a₂;
coherence by Th65;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster sups-preserving join-preserving finite-sups-preserving bottom-preserving Relation of the carrier of a₁,the carrier of a₂;
existence

proof end;

end;

registration

let c₁ be non empty lower-bounded Poset;
cluster CompactSublatt a₁ -> lower-bounded ;
coherence

proof end;

end;

theorem Th67: :: WAYBEL34:67

for b₁ being RelStr
for b₂ being non empty RelStr
for b₃ being Function of b₁,b₂
for b₄ being SubRelStr of b₁
for b₅ being SubRelStr of b₂ st b₃ .: the carrier of b₄ c= the carrier of b₅ holds
b₃ | the carrier of b₄ is Function of b₄,b₅

proof end;

theorem Th68: :: WAYBEL34:68

for b₁, b₂ being LATTICE
for b₃ being join-preserving Function of b₁,b₂
for b₄ being non empty full join-inheriting SubRelStr of b₁
for b₅ being non empty full join-inheriting SubRelStr of b₂
for b₆ being Function of b₄,b₅ st b₆ = b₃ | the carrier of b₄ holds
b₆ is join-preserving

proof end;

theorem Th69: :: WAYBEL34:69

for b₁, b₂ being lower-bounded LATTICE
for b₃ being finite-sups-preserving Function of b₁,b₂
for b₄ being non empty full finite-sups-inheriting SubRelStr of b₁
for b₅ being non empty full finite-sups-inheriting SubRelStr of b₂
for b₆ being Function of b₄,b₅ st b₆ = b₃ | the carrier of b₄ holds
b₆ is finite-sups-preserving

proof end;

registration

let c₁ be complete LATTICE;
cluster CompactSublatt a₁ -> lower-bounded finite-sups-inheriting bottom-inheriting ;
coherence

proof end;

end;

theorem Th70: :: WAYBEL34:70

for b₁, b₂ being complete LATTICE
for b₃ being sups-preserving Function of b₂,b₁ holds
( b₃ is compact-preserving iff b₃ | the carrier of (CompactSublatt b₂) is finite-sups-preserving Function of (CompactSublatt b₂),(CompactSublatt b₁) )

proof end;

theorem Th71: :: WAYBEL34:71

for b₁, b₂ being complete LATTICE st b₂ is algebraic holds
for b₃ being infs-preserving Function of b₁,b₂ holds
( b₃ is directed-sups-preserving iff (LowerAdj b₃) | the carrier of (CompactSublatt b₂) is finite-sups-preserving Function of (CompactSublatt b₂),(CompactSublatt b₁) )

proof end;