begin
deffunc H1( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1;
deffunc H2( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_meet of $1;
definition
let D be non
empty set ;
let R be
Relation;
existence
ex b1 being UnOp of D st
for x, y being Element of D st [x,y] in R holds
[(b1 . x),(b1 . y)] in R
existence
ex b1 being BinOp of D st
for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds
[(b1 . (x1,x2)),(b1 . (y1,y2))] in R
end;
definition
let D be non
empty set ;
let R be
Equivalence_Relation of
D;
let b be
BinOp of
D;
assume A1:
b is
BinOp of
D,
R
;
existence
ex b1 being BinOp of (Class R) st
for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b1 . (x,y) = Class (R,(b . (x1,y1)))
uniqueness
for b1, b2 being BinOp of (Class R) st ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b1 . (x,y) = Class (R,(b . (x1,y1))) ) & ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b2 . (x,y) = Class (R,(b . (x1,y1))) ) holds
b1 = b2
end;
theorem Th21:
for
D1,
D2 being non
empty set for
a1,
b1 being
Element of
D1 for
a2,
b2 being
Element of
D2 for
f1 being
BinOp of
D1 for
f2 being
BinOp of
D2 holds
|:f1,f2:| . (
[a1,a2],
[b1,b2])
= [(f1 . (a1,b1)),(f2 . (a2,b2))]
scheme
AuxCart2{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
P1[
set ,
set ] } :
for
d,
d9 being
Element of
[:F1(),F2():] holds
P1[
d,
d9]
provided
A1:
for
d1,
d19 being
Element of
F1()
for
d2,
d29 being
Element of
F2() holds
P1[
[d1,d2],
[d19,d29]]
scheme
AuxCart3{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
P1[
set ,
set ,
set ] } :
for
a,
b,
c being
Element of
[:F1(),F2():] holds
P1[
a,
b,
c]
provided
A1:
for
a1,
b1,
c1 being
Element of
F1()
for
a2,
b2,
c2 being
Element of
F2() holds
P1[
[a1,a2],
[b1,b2],
[c1,c2]]
Lm1:
for I being I_Lattice
for FI being Filter of I
for i, j, k being Element of I st i => j in FI holds
( i => (j "\/" k) in FI & i => (k "\/" j) in FI & (i "/\" k) => j in FI & (k "/\" i) => j in FI )
Lm2:
for I being I_Lattice
for FI being Filter of I
for i, k, j being Element of I st i => k in FI & j => k in FI holds
(i "\/" j) => k in FI
Lm3:
for I being I_Lattice
for FI being Filter of I
for i, j, k being Element of I st i => j in FI & i => k in FI holds
i => (j "/\" k) in FI
Lm4:
for I being I_Lattice
for FI being Filter of I
for i, j being Element of I holds
( i in Class ((equivalence_wrt FI),j) iff i <=> j in FI )