:: by Piotr Rudnicki

::

:: Received July 6, 1998

:: Copyright (c) 1998-2019 Association of Mizar Users

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

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

[:f,g:] is Function of [:L1,L2:],[:T1,T2:]

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

[:f,g:] is Function of [:L1,L2:],[:T1,T2:]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

for k being Function of L,L st k is directed-sups-preserving holds

corestr k is directed-sups-preserving

proof end;

theorem Th23: :: WAYBEL20:23

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

for f being Function of S,T st f is filtered-infs-preserving holds

f is monotone

proof end;

theorem Th24: :: WAYBEL20:24

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

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

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

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

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

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

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

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

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

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

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

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: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 upper-bounded RelStr ) holds

product J is upper-bounded

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: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 lower-bounded RelStr ) holds

for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i)

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: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 upper-bounded RelStr ) holds

for i being Element of I holds (Top (product J)) . i = Top (J . i)

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

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

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 Th34: :: WAYBEL20:34

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

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 ;

correctness

coherence

R is Equivalence_Relation of the carrier of L;

by A1;

end;
let R be Subset of [:L,L:];

assume A1: R is Equivalence_Relation of the carrier of L ;

correctness

coherence

R is Equivalence_Relation of the carrier of L;

by A1;

:: deftheorem Def1 defines EqRel WAYBEL20:def 1 :

for L being RelStr

for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L holds

EqRel R = R;

for L being RelStr

for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L holds

EqRel R = R;

definition

let L be non empty RelStr ;

let R be Subset of [:L,L:];

end;
let R be Subset of [:L,L:];

attr R is CLCongruence means :: WAYBEL20:def 2

( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] );

( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] );

:: deftheorem defines CLCongruence WAYBEL20:def 2 :

for L being non empty RelStr

for R being Subset of [:L,L:] holds

( R is CLCongruence iff ( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] ) );

for L being non empty RelStr

for R being Subset of [:L,L:] holds

( R is CLCongruence iff ( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] ) );

theorem Th35: :: WAYBEL20:35

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

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 ;

ex b_{1} being kernel Function of L,L st

for x being Element of L holds b_{1} . x = inf (Class ((EqRel R),x))

for b_{1}, b_{2} being kernel Function of L,L st ( for x being Element of L holds b_{1} . x = inf (Class ((EqRel R),x)) ) & ( for x being Element of L holds b_{2} . x = inf (Class ((EqRel R),x)) ) holds

b_{1} = b_{2}

end;
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 for x being Element of L holds it . x = inf (Class ((EqRel R),x));

ex b

for x being Element of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines kernel_op WAYBEL20:def 3 :

for L being complete LATTICE

for R being non empty Subset of [:L,L:] st R is CLCongruence holds

for b_{3} being kernel Function of L,L holds

( b_{3} = kernel_op R iff for x being Element of L holds b_{3} . x = inf (Class ((EqRel R),x)) );

for L being complete LATTICE

for R being non empty Subset of [:L,L:] st R is CLCongruence holds

for b

( b

theorem Th36: :: WAYBEL20:36

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

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 Th37: :: WAYBEL20:37

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

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 Th38: :: WAYBEL20:38

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

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 ;

ex b_{1} being Function of L,L st

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

end;
cluster non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V17( the carrier of L) V28( the carrier of L, the carrier of L) directed-sups-preserving kernel for Element of bool [: the carrier of L, the carrier of L:];

existence ex b

( b

proof end;

definition

let L be non empty reflexive RelStr ;

let k be kernel Function of L,L;

[:k,k:] " (id the carrier of L) is non empty Subset of [:L,L:]

end;
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 [:k,k:] " (id the carrier of L);

[:k,k:] " (id the carrier of L) is non empty Subset of [:L,L:]

proof end;

:: deftheorem defines kernel_congruence WAYBEL20:def 4 :

for L being non empty reflexive RelStr

for k being kernel Function of L,L holds kernel_congruence k = [:k,k:] " (id the carrier of L);

for L being non empty reflexive RelStr

for k being kernel Function of L,L holds kernel_congruence k = [:k,k:] " (id the carrier of L);

theorem :: WAYBEL20:39

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;

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

theorem Th40: :: WAYBEL20:40

for L being complete continuous LATTICE

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

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 ;

ex b_{1} being strict complete continuous LATTICE st

( the carrier of b_{1} = Class (EqRel R) & ( for x, y being Element of b_{1} holds

( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) )

for b_{1}, b_{2} being strict complete continuous LATTICE st the carrier of b_{1} = Class (EqRel R) & ( for x, y being Element of b_{1} holds

( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) & the carrier of b_{2} = Class (EqRel R) & ( for x, y being Element of b_{2} holds

( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) holds

b_{1} = b_{2}

end;
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 ( the carrier of it = Class (EqRel R) & ( for x, y being Element of it holds

( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) );

ex b

( the carrier of b

( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) )

proof end;

uniqueness for b

( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) & the carrier of b

( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) holds

b

proof end;

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

for L being complete continuous LATTICE

for R being non empty Subset of [:L,L:] st R is CLCongruence holds

for b_{3} being strict complete continuous LATTICE holds

( b_{3} = L ./. R iff ( the carrier of b_{3} = Class (EqRel R) & ( for x, y being Element of b_{3} holds

( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) ) );

for L being complete continuous LATTICE

for R being non empty Subset of [:L,L:] st R is CLCongruence holds

for b

( b

( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) ) );

theorem :: WAYBEL20:41

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

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

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

for R being non empty Subset of [:L,L:] st R is CLCongruence holds

R = kernel_congruence (kernel_op R) by Th36;

theorem :: WAYBEL20:43

for L being complete continuous LATTICE

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

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

proof end;

theorem :: WAYBEL20:44

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 )

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;

:: Lemma 2.10, p. 61, see WAYBEL15:16