:: Kernel Projections and Quotient Lattices
:: by Piotr Rudnicki
::
:: Received July 6, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem Th1: :: WAYBEL20:1
theorem Th2: :: WAYBEL20:2
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;
theorem Th3: :: WAYBEL20:3
theorem Th4: :: WAYBEL20:4
theorem Th5: :: WAYBEL20:5
theorem Th6: :: WAYBEL20:6
theorem Th7: :: WAYBEL20:7
theorem Th8: :: WAYBEL20:8
theorem Th9: :: WAYBEL20:9
theorem :: WAYBEL20:10
theorem :: WAYBEL20:11
theorem Th12: :: WAYBEL20:12
theorem Th13: :: WAYBEL20:13
theorem Th14: :: WAYBEL20:14
theorem Th15: :: WAYBEL20:15
theorem Th16: :: WAYBEL20:16
theorem Th17: :: WAYBEL20:17
theorem Th18: :: WAYBEL20:18
theorem Th19: :: WAYBEL20:19
theorem :: WAYBEL20:20
theorem :: WAYBEL20:21
theorem Th22: :: WAYBEL20:22
theorem :: WAYBEL20:23
canceled;
theorem Th24: :: WAYBEL20:24
theorem Th25: :: WAYBEL20:25
theorem Th26: :: WAYBEL20:26
theorem :: WAYBEL20:27
theorem :: WAYBEL20:28
theorem :: WAYBEL20:29
theorem :: WAYBEL20:30
theorem :: WAYBEL20:31
theorem :: WAYBEL20:32
theorem :: WAYBEL20:33
theorem :: WAYBEL20:34
theorem Th35: :: WAYBEL20:35
:: deftheorem Def1 defines EqRel WAYBEL20:def 1 :
:: deftheorem Def2 defines CLCongruence WAYBEL20:def 2 :
theorem Th36: :: WAYBEL20:36
:: deftheorem Def3 defines kernel_op WAYBEL20:def 3 :
theorem Th37: :: WAYBEL20:37
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 ) )
theorem Th39: :: WAYBEL20:39
:: deftheorem defines kernel_congruence WAYBEL20:def 4 :
theorem :: WAYBEL20:40
theorem Th41: :: WAYBEL20:41
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
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 :
theorem :: WAYBEL20:42
theorem :: WAYBEL20:43
theorem :: WAYBEL20:44
theorem :: WAYBEL20:45