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;
theorem Th1:
theorem
definition
let D be non
empty set ;
let R be
Relation;
mode UnOp of
D,
R -> UnOp of
D means :
Def1:
for
x,
y being
Element of
D st
[x,y] in R holds
[(it . x),(it . y)] in R;
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
mode BinOp of
D,
R -> BinOp of
D means :
Def2:
for
x1,
y1,
x2,
y2 being
Element of
D st
[x1,y1] in R &
[x2,y2] in R holds
[(it . x1,x2),(it . y1,y2)] 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;
:: deftheorem Def1 defines UnOp FILTER_1:def 1 :
:: deftheorem Def2 defines BinOp FILTER_1:def 2 :
definition
let D be non
empty set ;
let R be
Equivalence_Relation of
D;
let u be
UnOp of
D;
assume A1:
u is
UnOp of
D,
R
;
func u /\/ R -> UnOp of
(Class R) means
for
x,
y being
set st
x in Class R &
y in x holds
it . x = Class R,
(u . y);
existence
ex b1 being UnOp of (Class R) st
for x, y being set st x in Class R & y in x holds
b1 . x = Class R,(u . y)
uniqueness
for b1, b2 being UnOp of (Class R) st ( for x, y being set st x in Class R & y in x holds
b1 . x = Class R,(u . y) ) & ( for x, y being set st x in Class R & y in x holds
b2 . x = Class R,(u . y) ) holds
b1 = b2
end;
:: deftheorem defines /\/ FILTER_1:def 3 :
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
;
func b /\/ R -> BinOp of
(Class R) means :
Def4:
for
x,
y,
x1,
y1 being
set st
x in Class R &
y in Class R &
x1 in x &
y1 in y holds
it . x,
y = Class R,
(b . x1,y1);
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;
:: deftheorem Def4 defines /\/ FILTER_1:def 4 :
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
:: deftheorem Def5 defines /\/ FILTER_1:def 5 :
:: deftheorem Def6 defines /\/ FILTER_1:def 6 :
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
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]]
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
definition
let L1,
L2 be non
empty LattStr ;
func [:L1,L2:] -> strict LattStr equals
LattStr(#
[:the carrier of L1,the carrier of L2:],
|:the L_join of L1,the L_join of L2:|,
|:the L_meet of L1,the L_meet of L2:| #);
correctness
coherence
LattStr(# [:the carrier of L1,the carrier of L2:],|:the L_join of L1,the L_join of L2:|,|:the L_meet of L1,the L_meet of L2:| #) is strict LattStr ;
;
end;
:: deftheorem defines [: FILTER_1:def 7 :
:: deftheorem defines LattRel FILTER_1:def 8 :
theorem Th32:
theorem Th33:
:: deftheorem defines are_isomorphic FILTER_1:def 9 :
theorem
theorem
theorem
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem
theorem
theorem
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem
theorem Th56:
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 )
theorem Th57:
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
theorem Th58:
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
theorem Th59:
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 )
theorem Th60:
theorem Th61:
theorem