begin
theorem Th1:
theorem Th2:
definition
let L1,
L2,
T1,
T2 be
RelStr ;
let f be
Function of
L1,
T1;
let g be
Function of
L2,
T2;
[:redefine func [:f,g:] -> Function of
[:L1,L2:],
[:T1,T2:];
coherence
[:f,g:] is Function of [:L1,L2:],[:T1,T2:]
end;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem
theorem Th22:
theorem
canceled;
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
begin
theorem Th35:
:: 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;
:: deftheorem Def2 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:] ) );
theorem Th36:
:: 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 b3 being kernel Function of L,L holds
( b3 = kernel_op R iff for x being Element of L holds b3 . x = inf (Class ((EqRel R),x)) );
theorem Th37:
theorem Th38:
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 ) )
theorem Th39:
:: 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);
theorem
theorem Th41:
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:
( the
carrier of
it = Class (EqRel R) & ( for
x,
y being
Element of
it holds
(
x <= y iff
"/\" (
x,
L)
<= "/\" (
y,
L) ) ) );
existence
ex b1 being strict complete continuous LATTICE st
( the carrier of b1 = Class (EqRel R) & ( for x, y being Element of b1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) )
uniqueness
for b1, b2 being strict complete continuous LATTICE st the carrier of b1 = Class (EqRel R) & ( for x, y being Element of b1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) & the carrier of b2 = Class (EqRel R) & ( for x, y being Element of b2 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) holds
b1 = b2
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 b3 being strict complete continuous LATTICE holds
( b3 = L ./. R iff ( the carrier of b3 = Class (EqRel R) & ( for x, y being Element of b3 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) ) );
theorem
theorem
theorem
theorem