:: Filters - Part II. Quotient Lattices Modulo Filters andDirect Product of Two Lattices
:: by Grzegorz Bancerek
::
:: Received April 19, 1991
:: Copyright (c) 1991 Association of Mizar Users
deffunc H1( LattStr ) -> M5([:the carrier of $1,the carrier of $1:],the carrier of $1) = the L_join of $1;
deffunc H2( LattStr ) -> M5([:the carrier of $1,the carrier of $1:],the carrier of $1) = the L_meet of $1;
theorem Th1: :: FILTER_1:1
theorem :: FILTER_1:2
definition
let D be non
empty set ;
let R be
Relation;
mode UnOp of
D,
R -> UnOp of
D means :
Def1:
:: FILTER_1:def 1
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:
:: FILTER_1:def 2
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 :: FILTER_1:def 3
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:
:: FILTER_1:def 4
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: :: FILTER_1:3
theorem Th4: :: FILTER_1:4
theorem Th5: :: FILTER_1:5
theorem Th6: :: FILTER_1:6
theorem Th7: :: FILTER_1:7
theorem :: FILTER_1:8
theorem Th9: :: FILTER_1:9
theorem Th10: :: FILTER_1:10
theorem :: FILTER_1:11
theorem Th12: :: FILTER_1:12
theorem Th13: :: FILTER_1:13
theorem Th14: :: FILTER_1:14
:: deftheorem Def5 defines /\/ FILTER_1:def 5 :
:: deftheorem Def6 defines /\/ FILTER_1:def 6 :
theorem Th15: :: FILTER_1:15
theorem Th16: :: FILTER_1:16
theorem Th17: :: FILTER_1:17
theorem Th18: :: FILTER_1:18
theorem Th19: :: FILTER_1:19
theorem Th20: :: FILTER_1:20
theorem :: FILTER_1:21
theorem Th22: :: FILTER_1:22
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 :: FILTER_1:sch 5
AuxCart2{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
P1[
set ,
set ] } :
for
d,
d' being
Element of
[:F1(),F2():] holds
P1[
d,
d']
provided
A1:
for
d1,
d1' being
Element of
F1()
for
d2,
d2' being
Element of
F2() holds
P1[
[d1,d2],
[d1',d2']]
scheme :: FILTER_1:sch 6
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: :: FILTER_1:23
theorem Th24: :: FILTER_1:24
theorem Th25: :: FILTER_1:25
theorem Th26: :: FILTER_1:26
theorem :: FILTER_1:27
theorem Th28: :: FILTER_1:28
theorem Th29: :: FILTER_1:29
theorem Th30: :: FILTER_1:30
theorem Th31: :: FILTER_1:31
definition
let L1,
L2 be non
empty LattStr ;
func [:L1,L2:] -> strict LattStr equals :: FILTER_1:def 7
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: :: FILTER_1:32
theorem Th33: :: FILTER_1:33
:: deftheorem defines are_isomorphic FILTER_1:def 9 :
theorem :: FILTER_1:34
theorem :: FILTER_1:35
theorem :: FILTER_1:36
theorem Th37: :: FILTER_1:37
theorem :: FILTER_1:38
theorem Th39: :: FILTER_1:39
theorem Th40: :: FILTER_1:40
theorem Th41: :: FILTER_1:41
theorem Th42: :: FILTER_1:42
theorem Th43: :: FILTER_1:43
theorem Th44: :: FILTER_1:44
theorem Th45: :: FILTER_1:45
theorem Th46: :: FILTER_1:46
theorem :: FILTER_1:47
theorem :: FILTER_1:48
theorem :: FILTER_1:49
theorem :: FILTER_1:50
theorem Th51: :: FILTER_1:51
theorem Th52: :: FILTER_1:52
theorem Th53: :: FILTER_1:53
theorem Th54: :: FILTER_1:54
theorem :: FILTER_1:55
theorem Th56: :: FILTER_1:56
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: :: FILTER_1:57
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: :: FILTER_1:58
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: :: FILTER_1:59
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: :: FILTER_1:60
theorem Th61: :: FILTER_1:61
theorem :: FILTER_1:62