:: WAYBEL20 semantic presentation

theorem Th1: :: WAYBEL20:1

for b₁ being set
for b₂ being Subset of (id b₁) holds proj1 b₂ = proj2 b₂

proof end;

theorem Th2: :: WAYBEL20:2

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂ holds [:b₃,b₃:] " (id b₂) is Equivalence_Relation of b₁

proof end;

definition

let c₁, c₂, c₃, c₄ be RelStr ;
let c₅ be Function of c₁,c₃;
let c₆ be Function of c₂,c₄;
redefine func [: as [:c₅,c₆:] -> Function of [:a₁,a₂:],[:a₃,a₄:];
coherence

proof end;

end;

theorem Th3: :: WAYBEL20:3

for b₁, b₂ being Function
for b₃ being set holds
( proj1 ([:b₁,b₂:] .: b₃) c= b₁ .: (proj1 b₃) & proj2 ([:b₁,b₂:] .: b₃) c= b₂ .: (proj2 b₃) )

proof end;

theorem Th4: :: WAYBEL20:4

for b₁, b₂ being Function
for b₃ being set st b₃ c= [:(dom b₁),(dom b₂):] holds
( proj1 ([:b₁,b₂:] .: b₃) = b₁ .: (proj1 b₃) & proj2 ([:b₁,b₂:] .: b₃) = b₂ .: (proj2 b₃) )

proof end;

theorem Th5: :: WAYBEL20:5

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

proof end;

theorem Th6: :: WAYBEL20:6

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

proof end;

theorem Th7: :: WAYBEL20:7

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being Subset of [:b₁,b₂:] st ex_inf_of b₃,[:b₁,b₂:] holds
inf b₃ = [(inf (proj1 b₃)),(inf (proj2 b₃))]

proof end;

theorem Th8: :: WAYBEL20:8

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being Subset of [:b₁,b₂:] st ex_sup_of b₃,[:b₁,b₂:] holds
sup b₃ = [(sup (proj1 b₃)),(sup (proj2 b₃))]

proof end;

theorem Th9: :: WAYBEL20:9

for b₁, b₂, b₃, b₄ being non empty antisymmetric RelStr
for b₅ being Function of b₁,b₃
for b₆ being Function of b₂,b₄ st b₅ is infs-preserving & b₆ is infs-preserving holds
[:b₅,b₆:] is infs-preserving

proof end;

theorem Th10: :: WAYBEL20:10

for b₁, b₂, b₃, b₄ being non empty reflexive antisymmetric RelStr
for b₅ being Function of b₁,b₃
for b₆ being Function of b₂,b₄ st b₅ is filtered-infs-preserving & b₆ is filtered-infs-preserving holds
[:b₅,b₆:] is filtered-infs-preserving

proof end;

theorem Th11: :: WAYBEL20:11

for b₁, b₂, b₃, b₄ being non empty antisymmetric RelStr
for b₅ being Function of b₁,b₃
for b₆ being Function of b₂,b₄ st b₅ is sups-preserving & b₆ is sups-preserving holds
[:b₅,b₆:] is sups-preserving

proof end;

theorem Th12: :: WAYBEL20:12

for b₁, b₂, b₃, b₄ being non empty reflexive antisymmetric RelStr
for b₅ being Function of b₁,b₃
for b₆ being Function of b₂,b₄ st b₅ is directed-sups-preserving & b₆ is directed-sups-preserving holds
[:b₅,b₆:] is directed-sups-preserving

proof end;

theorem Th13: :: WAYBEL20:13

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

proof end;

theorem Th14: :: WAYBEL20:14

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

proof end;

theorem Th15: :: WAYBEL20:15

for b₁, b₂ being non empty RelStr st b₁,b₂ are_isomorphic & b₁ is reflexive holds
b₂ is reflexive

proof end;

theorem Th16: :: WAYBEL20:16

for b₁, b₂ being non empty RelStr st b₁,b₂ are_isomorphic & b₁ is transitive holds
b₂ is transitive

proof end;

theorem Th17: :: WAYBEL20:17

for b₁, b₂ being non empty RelStr st b₁,b₂ are_isomorphic & b₁ is antisymmetric holds
b₂ is antisymmetric

proof end;

theorem Th18: :: WAYBEL20:18

for b₁, b₂ being non empty RelStr st b₁,b₂ are_isomorphic & b₁ is complete holds
b₂ is complete

proof end;

theorem Th19: :: WAYBEL20:19

for b₁ being non empty transitive RelStr
for b₂ being Function of b₁,b₁ st b₂ is infs-preserving holds
corestr b₂ is infs-preserving

proof end;

theorem Th20: :: WAYBEL20:20

for b₁ being non empty transitive RelStr
for b₂ being Function of b₁,b₁ st b₂ is filtered-infs-preserving holds
corestr b₂ is filtered-infs-preserving

proof end;

theorem Th21: :: WAYBEL20:21

for b₁ being non empty transitive RelStr
for b₂ being Function of b₁,b₁ st b₂ is sups-preserving holds
corestr b₂ is sups-preserving

proof end;

theorem Th22: :: WAYBEL20:22

for b₁ being non empty transitive RelStr
for b₂ being Function of b₁,b₁ st b₂ is directed-sups-preserving holds
corestr b₂ is directed-sups-preserving

proof end;

theorem Th23: :: WAYBEL20:23

canceled;

theorem Th24: :: WAYBEL20:24

for b₁, b₂ being non empty reflexive antisymmetric RelStr
for b₃ being Function of b₁,b₂ st b₃ is filtered-infs-preserving holds
b₃ is monotone

proof end;

theorem Th25: :: WAYBEL20:25

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₃ is monotone holds
for b₄ being Subset of b₁ st b₄ is filtered holds
b₃ .: b₄ is filtered

proof end;

theorem Th26: :: WAYBEL20:26

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 infs-preserving & b₅ is infs-preserving holds
b₅ * b₄ is infs-preserving

proof end;

theorem Th27: :: WAYBEL20:27

for b₁, b₂, b₃ being non empty reflexive antisymmetric RelStr
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is filtered-infs-preserving & b₅ is filtered-infs-preserving holds
b₅ * b₄ is filtered-infs-preserving

proof end;

theorem Th28: :: WAYBEL20:28

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 sups-preserving & b₅ is sups-preserving holds
b₅ * b₄ is sups-preserving

proof end;

theorem Th29: :: WAYBEL20:29

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

proof end;

theorem Th30: :: WAYBEL20:30

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is antisymmetric lower-bounded RelStr ) holds
product b₂ is lower-bounded

proof end;

theorem Th31: :: WAYBEL20:31

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is antisymmetric upper-bounded RelStr ) holds
product b₂ is upper-bounded

proof end;

theorem Th32: :: WAYBEL20:32

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is antisymmetric lower-bounded RelStr ) holds
for b₃ being Element of b₁ holds (Bottom (product b₂)) . b₃ = Bottom (b₂ . b₃)

proof end;

theorem Th33: :: WAYBEL20:33

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is antisymmetric upper-bounded RelStr ) holds
for b₃ being Element of b₁ holds (Top (product b₂)) . b₃ = Top (b₂ . b₃)

proof end;

theorem Th34: :: WAYBEL20:34

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is complete continuous LATTICE ) holds
product b₂ is continuous

proof end;

theorem Th35: :: WAYBEL20:35

for b₁, b₂ being complete continuous LATTICE
for b₃ being CLHomomorphism of b₁,b₂
for b₄ being Subset of [:b₁,b₁:] st b₄ = [:b₃,b₃:] " (id the carrier of b₂) holds
subrelstr b₄ is CLSubFrame of [:b₁,b₁:]

proof end;

definition

let c₁ be RelStr ;
let c₂ be Subset of [:c₁,c₁:];
assume E23: c₂ is Equivalence_Relation of the carrier of c₁ ;
func EqRel c₂ -> Equivalence_Relation of the carrier of a₁ equals :Def1: :: WAYBEL20:def 1
a₂;
correctness by E23;

end;

:: deftheorem Def1 defines EqRel WAYBEL20:def 1 :

definition

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

end;

:: deftheorem Def2 defines CLCongruence WAYBEL20:def 2 :

theorem Th36: :: WAYBEL20:36

for b₁ being complete LATTICE
for b₂ being non empty Subset of [:b₁,b₁:] st b₂ is CLCongruence holds
for b₃ being Element of b₁ holds [(inf (Class (EqRel b₂),b₃)),b₃] in b₂

proof end;

definition

let c₁ be complete LATTICE;
let c₂ be non empty Subset of [:c₁,c₁:];
assume E26: c₂ is CLCongruence ;
func kernel_op c₂ -> kernel Function of a₁,a₁ means :Def3: :: WAYBEL20:def 3
for b₁ being Element of a₁ holds a₃ . b₁ = inf (Class (EqRel a₂),b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines kernel_op WAYBEL20:def 3 :

theorem Th37: :: WAYBEL20:37

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

proof end;

theorem Th38: :: WAYBEL20:38

for b₁ being complete continuous LATTICE
for b₂ being Subset of [:b₁,b₁:]
for b₃ being kernel Function of b₁,b₁ st b₃ is directed-sups-preserving & b₂ = [:b₃,b₃:] " (id the carrier of b₁) holds
ex b₄ being strict complete continuous LATTICE st
( the carrier of b₄ = Class (EqRel b₂) & the InternalRel of b₄ = { [(Class (EqRel b₂),b₅),(Class (EqRel b₂),b₆)] where B is Element of b₁, B is Element of b₁ : b₃ . b₅ <= b₃ . b₆ } & ( for b₅ being Function of b₁,b₄ st ( for b₆ being Element of b₁ holds b₅ . b₆ = Class (EqRel b₂),b₆ ) holds
b₅ is CLHomomorphism of b₁,b₄ ) )

proof end;

theorem Th39: :: WAYBEL20:39

for b₁ being complete continuous LATTICE
for b₂ being Subset of [:b₁,b₁:] st b₂ is Equivalence_Relation of the carrier of b₁ & ex b₃ being complete continuous LATTICE st
( the carrier of b₃ = Class (EqRel b₂) & ( for b₄ being Function of b₁,b₃ st ( for b₅ being Element of b₁ holds b₄ . b₅ = Class (EqRel b₂),b₅ ) holds
b₄ is CLHomomorphism of b₁,b₃ ) ) holds
subrelstr b₂ is CLSubFrame of [:b₁,b₁:]

proof end;

registration

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

proof end;

end;

definition

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

proof end;

end;

:: deftheorem Def4 defines kernel_congruence WAYBEL20:def 4 :

theorem Th40: :: WAYBEL20:40

for b₁ being non empty reflexive RelStr
for b₂ being kernel Function of b₁,b₁ holds kernel_congruence b₂ is Equivalence_Relation of the carrier of b₁ by Th2;

theorem Th41: :: WAYBEL20:41

for b₁ being complete continuous LATTICE
for b₂ being directed-sups-preserving kernel Function of b₁,b₁ holds kernel_congruence b₂ is CLCongruence

proof end;

definition

let c₁ be complete continuous LATTICE;
let c₂ be non empty Subset of [:c₁,c₁:];
assume E32: c₂ is CLCongruence ;
func c₁ ./. c₂ -> strict complete continuous LATTICE means :Def5: :: WAYBEL20:def 5
( the carrier of a₃ = Class (EqRel a₂) & ( for b₁, b₂ being Element of a₃ holds
( b₁ <= b₂ iff "/\" b₁,a₁ <= "/\" b₂,a₁ ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th42: :: WAYBEL20:42

for b₁ being complete continuous LATTICE
for b₂ being non empty Subset of [:b₁,b₁:] st b₂ is CLCongruence holds
for b₃ being set holds
( b₃ is Element of (b₁ ./. b₂) iff ex b₄ being Element of b₁ st b₃ = Class (EqRel b₂),b₄ )

proof end;

theorem Th43: :: WAYBEL20:43

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

theorem Th44: :: WAYBEL20:44

for b₁ being complete continuous LATTICE
for b₂ being directed-sups-preserving kernel Function of b₁,b₁ holds b₂ = kernel_op (kernel_congruence b₂)

proof end;

theorem Th45: :: WAYBEL20:45

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

proof end;