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 :
:: deftheorem Def2 defines CLCongruence WAYBEL20:def 2 :
theorem Th36:
:: deftheorem Def3 defines kernel_op WAYBEL20:def 3 :
theorem Th37:
theorem Th38:
theorem Th39:
:: deftheorem defines kernel_congruence WAYBEL20:def 4 :
theorem
theorem Th41:
definition
let L be
complete continuous LATTICE;
let R be non
empty Subset of ;
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 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 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 holds
( x <= y iff "/\" x,L <= "/\" y,L ) ) & the carrier of b2 = Class (EqRel R) & ( for x, y being Element of holds
( x <= y iff "/\" x,L <= "/\" y,L ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines ./. WAYBEL20:def 5 :
theorem
theorem
theorem
theorem