environ
vocabularies HIDDEN, SUBSET_1, RELAT_1, XBOOLE_0, FUNCT_1, ZFMISC_1, EQREL_1, RELAT_2, ORDERS_2, STRUCT_0, TARSKI, YELLOW_0, LATTICES, LATTICE3, ORDINAL2, WAYBEL_0, WELLORD1, CAT_1, XXREAL_0, REWRITE1, WAYBEL_1, GROUP_6, SEQM_3, YELLOW_1, WAYBEL_3, PBOOLE, CARD_3, FINSET_1, FUNCT_4, WAYBEL16, WAYBEL_5, BINOP_1, SETFAM_1, WAYBEL20;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, SETFAM_1, RELAT_2, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, BINOP_1, FUNCT_2, FINSET_1, DOMAIN_1, EQREL_1, FUNCT_3, FUNCT_7, STRUCT_0, ORDERS_2, LATTICE3, QUANTAL1, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL16;
definitions TARSKI, RELAT_2, LATTICE3, LATTICE5, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_3;
theorems TARSKI, ZFMISC_1, RELAT_1, RELAT_2, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_5, FUNCT_7, CARD_3, ORDERS_2, QUANTAL1, EQREL_1, YELLOW_0, YELLOW_2, YELLOW_3, YELLOW10, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL13, WAYBEL15, WAYBEL16, WAYBEL17, XBOOLE_0, XBOOLE_1, PARTFUN1, ORDERS_1, XTUPLE_0;
schemes YELLOW_0, FUNCT_2, PBOOLE;
registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, FUNCT_2, FINSET_1, STRUCT_0, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_2, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL10, YELLOW_9, RELSET_1;
constructors HIDDEN, DOMAIN_1, FUNCT_7, MONOID_0, QUANTAL1, ORDERS_3, WAYBEL_1, YELLOW_3, WAYBEL16, RELSET_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities YELLOW_0, WAYBEL_3, YELLOW_2, BINOP_1, STRUCT_0;
expansions RELAT_2, LATTICE3, LATTICE5, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_3;
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 Th37:
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 ) )
definition
let L be
complete continuous LATTICE;
let R be non
empty Subset of
[:L,L:];
assume A1:
R is
CLCongruence
;
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;
:: Lemma 2.10, p. 61, see WAYBEL15:16