:: WAYBEL20 semantic presentation

theorem Th1: :: WAYBEL20:1

for X being set
for S being Subset of (id X) holds proj1 S = proj2 S

proof end;

theorem Th2: :: WAYBEL20:2

for X, Y being non empty set
for f being Function of X,Y holds [:f,f:] " (id Y) is Equivalence_Relation of X

proof end;

definition

let L1, L2, T1, T2 be RelStr ;
let f be Function of L1,T1;
let g be Function of L2,T2;
:: original: [:
redefine func [:f,g:] -> Function of [:L1,L2:],[:T1,T2:];
coherence

proof end;

end;

theorem Th3: :: WAYBEL20:3

for f, g being Function
for X being set holds
( proj1 ([:f,g:] .: X) c= f .: (proj1 X) & proj2 ([:f,g:] .: X) c= g .: (proj2 X) )

proof end;

theorem Th4: :: WAYBEL20:4

for f, g being Function
for X being set st X c= [:(dom f),(dom g):] holds
( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) )

proof end;

theorem Th5: :: WAYBEL20:5

for S being non empty antisymmetric RelStr st ex_inf_of {} ,S holds
S is upper-bounded

proof end;

theorem Th6: :: WAYBEL20:6

for S being non empty antisymmetric RelStr st ex_sup_of {} ,S holds
S is lower-bounded

proof end;

theorem Th7: :: WAYBEL20:7

for L1, L2 being non empty antisymmetric RelStr
for D being Subset of [:L1,L2:] st ex_inf_of D,[:L1,L2:] holds
inf D = [(inf (proj1 D)),(inf (proj2 D))]

proof end;

theorem Th8: :: WAYBEL20:8

for L1, L2 being non empty antisymmetric RelStr
for D being Subset of [:L1,L2:] st ex_sup_of D,[:L1,L2:] holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]

proof end;

theorem Th9: :: WAYBEL20:9

for L1, L2, T1, T2 being non empty antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is infs-preserving & g is infs-preserving holds
[:f,g:] is infs-preserving

proof end;

theorem :: WAYBEL20:10

for L1, L2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
[:f,g:] is filtered-infs-preserving

proof end;

theorem :: WAYBEL20:11

for L1, L2, T1, T2 being non empty antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is sups-preserving & g is sups-preserving holds
[:f,g:] is sups-preserving

proof end;

theorem Th12: :: WAYBEL20:12

for L1, L2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is directed-sups-preserving & g is directed-sups-preserving holds
[:f,g:] is directed-sups-preserving

proof end;

theorem Th13: :: WAYBEL20:13

for L being non empty antisymmetric RelStr
for X being Subset of [:L,L:] st X c= id the carrier of L & ex_inf_of X,[:L,L:] holds
inf X in id the carrier of L

proof end;

theorem Th14: :: WAYBEL20:14

for L being non empty antisymmetric RelStr
for X being Subset of [:L,L:] st X c= id the carrier of L & ex_sup_of X,[:L,L:] holds
sup X in id the carrier of L

proof end;

theorem Th15: :: WAYBEL20:15

for L, M being non empty RelStr st L,M are_isomorphic & L is reflexive holds
M is reflexive

proof end;

theorem Th16: :: WAYBEL20:16

for L, M being non empty RelStr st L,M are_isomorphic & L is transitive holds
M is transitive

proof end;

theorem Th17: :: WAYBEL20:17

for L, M being non empty RelStr st L,M are_isomorphic & L is antisymmetric holds
M is antisymmetric

proof end;

theorem Th18: :: WAYBEL20:18

for L, M being non empty RelStr st L,M are_isomorphic & L is complete holds
M is complete

proof end;

theorem Th19: :: WAYBEL20:19

for L being non empty transitive RelStr
for k being Function of L,L st k is infs-preserving holds
corestr k is infs-preserving

proof end;

theorem :: WAYBEL20:20

for L being non empty transitive RelStr
for k being Function of L,L st k is filtered-infs-preserving holds
corestr k is filtered-infs-preserving

proof end;

theorem :: WAYBEL20:21

for L being non empty transitive RelStr
for k being Function of L,L st k is sups-preserving holds
corestr k is sups-preserving

proof end;

theorem Th22: :: WAYBEL20:22

for L being non empty transitive RelStr
for k being Function of L,L st k is directed-sups-preserving holds
corestr k is directed-sups-preserving

proof end;

theorem :: WAYBEL20:23

canceled;

theorem Th24: :: WAYBEL20:24

for S, T being non empty reflexive antisymmetric RelStr
for f being Function of S,T st f is filtered-infs-preserving holds
f is monotone

proof end;

theorem Th25: :: WAYBEL20:25

for S, T being non empty RelStr
for f being Function of S,T st f is monotone holds
for X being Subset of S st X is filtered holds
f .: X is filtered

proof end;

theorem Th26: :: WAYBEL20:26

for L1, L2, L3 being non empty RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is infs-preserving & g is infs-preserving holds
g * f is infs-preserving

proof end;

theorem :: WAYBEL20:27

for L1, L2, L3 being non empty reflexive antisymmetric RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
g * f is filtered-infs-preserving

proof end;

theorem :: WAYBEL20:28

for L1, L2, L3 being non empty RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is sups-preserving & g is sups-preserving holds
g * f is sups-preserving

proof end;

theorem :: WAYBEL20:29

for L1, L2, L3 being non empty reflexive antisymmetric RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds
g * f is directed-sups-preserving

proof end;

theorem :: WAYBEL20:30

for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds
product J is lower-bounded

proof end;

theorem :: WAYBEL20:31

for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds
product J is upper-bounded

proof end;

theorem :: WAYBEL20:32

for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds
for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i)

proof end;

theorem :: WAYBEL20:33

for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds
for i being Element of I holds (Top (product J)) . i = Top (J . i)

proof end;

theorem :: WAYBEL20:34

for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete continuous LATTICE ) holds
product J is continuous

proof end;

theorem Th35: :: WAYBEL20:35

for L, T being complete continuous LATTICE
for g being CLHomomorphism of L,T
for S being Subset of [:L,L:] st S = [:g,g:] " (id the carrier of T) holds
subrelstr S is CLSubFrame of [:L,L:]

proof end;

definition

let L be RelStr ;
let R be Subset of [:L,L:];
assume A1: R is Equivalence_Relation of the carrier of L ;
func EqRel R -> Equivalence_Relation of the carrier of L equals :Def1: :: WAYBEL20:def 1
R;
correctness by A1;

end;

:: deftheorem Def1 defines EqRel WAYBEL20:def 1 :

definition

let L be non empty RelStr ;
let R be Subset of [:L,L:];
attr R is CLCongruence means :Def2: :: WAYBEL20:def 2
( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] );

end;

:: deftheorem Def2 defines CLCongruence WAYBEL20:def 2 :

theorem Th36: :: WAYBEL20:36

for L being complete LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for x being Element of L holds [(inf (Class (EqRel R),x)),x] in R

proof end;

definition

let L be complete LATTICE;
let R be non empty Subset of [:L,L:];
assume A1: R is CLCongruence ;
func kernel_op R -> kernel Function of L,L means :Def3: :: WAYBEL20:def 3
for x being Element of L holds it . x = inf (Class (EqRel R),x);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines kernel_op WAYBEL20:def 3 :

theorem Th37: :: WAYBEL20:37

for L being complete LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) )

proof end;

theorem Th38: :: WAYBEL20:38

for L being complete continuous LATTICE
for R being Subset of [:L,L:]
for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds
ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class (EqRel R),x),(Class (EqRel R),y)] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class (EqRel R),x ) holds
g is CLHomomorphism of L,LR ) )

proof end;

theorem Th39: :: WAYBEL20:39

for L being complete continuous LATTICE
for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L & ex LR being complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class (EqRel R),x ) holds
g is CLHomomorphism of L,LR ) ) holds
subrelstr R is CLSubFrame of [:L,L:]

proof end;

registration

let L be non empty reflexive RelStr ;
cluster directed-sups-preserving kernel Relation of the carrier of L,the carrier of L;
existence

proof end;

end;

definition

let L be non empty reflexive RelStr ;
let k be kernel Function of L,L;
func kernel_congruence k -> non empty Subset of [:L,L:] equals :: WAYBEL20:def 4
[:k,k:] " (id the carrier of L);
coherence

proof end;

end;

:: deftheorem defines kernel_congruence WAYBEL20:def 4 :

theorem Th40: :: WAYBEL20:40

for L being non empty reflexive RelStr
for k being kernel Function of L,L holds kernel_congruence k is Equivalence_Relation of the carrier of L by Th2;

theorem Th41: :: WAYBEL20:41

for L being complete continuous LATTICE
for k being directed-sups-preserving kernel Function of L,L holds kernel_congruence k is CLCongruence

proof end;

definition

let L be complete continuous LATTICE;
let R be non empty Subset of [:L,L:];
assume A1: R is CLCongruence ;
func L ./. R -> strict complete continuous LATTICE means :Def5: :: WAYBEL20:def 5
( the carrier of it = Class (EqRel R) & ( for x, y being Element of it holds
( x <= y iff "/\" x,L <= "/\" y,L ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines ./. WAYBEL20:def 5 :

theorem :: WAYBEL20:42

for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for x being set holds
( x is Element of (L ./. R) iff ex y being Element of L st x = Class (EqRel R),y )

proof end;

theorem :: WAYBEL20:43

for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
R = kernel_congruence (kernel_op R) by Th37;

theorem :: WAYBEL20:44

for L being complete continuous LATTICE
for k being directed-sups-preserving kernel Function of L,L holds k = kernel_op (kernel_congruence k)

proof end;

theorem :: WAYBEL20:45

for L being complete continuous LATTICE
for p being projection Function of L,L st p is infs-preserving holds
( Image p is continuous LATTICE & Image p is infs-inheriting )

proof end;