:: Filters - Part II. Quotient Lattices Modulo Filters and
:: Direct Product of Two Lattices
:: by Grzegorz Bancerek
::
:: Received April 19, 1991
:: Copyright (c) 1991-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies LATTICES, CARD_FIL, SUBSET_1, XBOOLE_0, RELAT_1, EQREL_1,
FILTER_0, BINOP_1, PBOOLE, FUNCT_1, MCART_1, TARSKI, LATTICE2, STRUCT_0,
XBOOLEAN, FUNCT_4, ZFMISC_1, WELLORD1, XXREAL_2, PARTFUN1, FILTER_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, BINOP_1, EQREL_1, DOMAIN_1, WELLORD1, FUNCT_3, FUNCT_4,
STRUCT_0, LATTICES, FILTER_0, LATTICE2;
constructors WELLORD1, BINOP_1, FUNCT_3, FUNCT_4, EQREL_1, REALSET1, FILTER_0,
LATTICE2, RELSET_1;
registrations SUBSET_1, FUNCT_1, PARTFUN1, FUNCT_2, EQREL_1, STRUCT_0,
LATTICES, FILTER_0, LATTICE2, RELSET_1, RELAT_1;
requirements SUBSET, BOOLE;
begin
reserve L,L1,L2 for Lattice,
F1,F2 for Filter of L,
p,q,r,s for Element of L,
p1,q1,r1,s1 for Element of L1,
p2,q2,r2,s2 for Element of L2,
X,x,x1,x2,y,y1,y2 for set,
D,D1,D2 for non empty set,
R for Relation,
RD for Equivalence_Relation of D,
a,b,d for Element of D,
a1,b1,c1 for Element of D1,
a2,b2,c2 for Element of D2,
B for B_Lattice,
FB for Filter of B,
I for I_Lattice,
FI for Filter of I ,
i,i1,i2,j,j1,j2,k for Element of I,
f1,g1 for BinOp of D1,
f2,g2 for BinOp of D2;
theorem :: FILTER_1:1
F1 /\ F2 is Filter of L;
theorem :: FILTER_1:2
<.p.) = <.q.) implies p = q;
definition
let L,F1,F2;
redefine func F1 /\ F2 -> Filter of L;
end;
definition
let D,R;
mode UnOp of D,R -> UnOp of D means
:: FILTER_1:def 1
for x,y being Element of D st [x, y] in R holds [it.x,it.y] in R;
mode BinOp of D,R -> BinOp of D means
:: 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;
end;
reserve F,G for BinOp of D,RD;
definition
let D;
let R be Equivalence_Relation of D;
mode UnOp of R is UnOp of D,R;
mode BinOp of R is BinOp of D,R;
end;
definition
let D;
let R be Equivalence_Relation of D;
let u be UnOp of D;
assume
u is UnOp of D,R;
func u /\/ R -> UnOp of Class R means
:: FILTER_1:def 3
for x,y st x in Class R & y in x holds it.x = Class(R,u.y);
end;
definition
let D;
let R be Equivalence_Relation of D;
let b be BinOp of D;
assume
b is BinOp of D,R;
func b /\/ R -> BinOp of Class R means
:: FILTER_1:def 4
for x,y, x1,y1 st x in Class R
& y in Class R & x1 in x & y1 in y holds it.(x,y) = Class(R,b.(x1,y1));
end;
theorem :: FILTER_1:3
(F /\/ RD).(Class(RD,a), Class(RD,b)) = Class(RD, F.(a,b));
scheme :: FILTER_1:sch 1
SchAux1 { D()->non empty set, R()->Equivalence_Relation of D(), P[set] }:
for x being Element of Class R() holds P[x]
provided
for x being Element of D() holds P[EqClass(R(),x)];
scheme :: FILTER_1:sch 2
SchAux2 { D()->non empty set, R()->Equivalence_Relation of D(), P[set,set] }
: for x,y being Element of Class R() holds P[x,y]
provided
for x,y being Element of D() holds P[EqClass(R(),x),EqClass(R(),y)];
scheme :: FILTER_1:sch 3
SchAux3 { D()->non empty set, R()->Equivalence_Relation of D(), P[set,set,
set] }: for x,y,z being Element of Class R() holds P[x,y,z]
provided
for x,y,z being Element of D() holds P[EqClass(R(),x),EqClass(R(),y)
,EqClass(R(),z)];
theorem :: FILTER_1:4
F is commutative implies F/\/RD is commutative;
theorem :: FILTER_1:5
F is associative implies F/\/RD is associative;
theorem :: FILTER_1:6
d is_a_left_unity_wrt F implies EqClass(RD,d) is_a_left_unity_wrt F/\/RD;
theorem :: FILTER_1:7
d is_a_right_unity_wrt F implies EqClass(RD,d) is_a_right_unity_wrt F/\/RD;
theorem :: FILTER_1:8
d is_a_unity_wrt F implies EqClass(RD,d) is_a_unity_wrt F/\/RD;
theorem :: FILTER_1:9
F is_left_distributive_wrt G implies F/\/RD is_left_distributive_wrt G/\/RD;
theorem :: FILTER_1:10
F is_right_distributive_wrt G implies F/\/RD is_right_distributive_wrt G/\/RD
;
theorem :: FILTER_1:11
F is_distributive_wrt G implies F/\/RD is_distributive_wrt G/\/RD;
theorem :: FILTER_1:12
F absorbs G implies F/\/RD absorbs G/\/RD;
theorem :: FILTER_1:13
the L_join of I is BinOp of the carrier of I, equivalence_wrt FI;
theorem :: FILTER_1:14
the L_meet of I is BinOp of the carrier of I, equivalence_wrt FI;
definition
let L be Lattice, F be Filter of L;
assume
L is I_Lattice;
func L /\/ F -> strict Lattice means
:: FILTER_1:def 5
for R being
Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds it =
LattStr (#Class R, (the L_join of L)/\/R, (the L_meet of L)/\/R#);
end;
definition
let L be Lattice, F be Filter of L, a be Element of L;
assume
L is I_Lattice;
func a /\/ F -> Element of L /\/ F means
:: FILTER_1:def 6
for R being
Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds it =
Class(R, a);
end;
theorem :: FILTER_1:15
(i/\/FI) "\/" (j/\/FI) = (i"\/"j)/\/FI & (i/\/FI) "/\" (j/\/FI)
= (i"/\"j)/\/FI;
theorem :: FILTER_1:16
i/\/FI [= j/\/FI iff i => j in FI;
theorem :: FILTER_1:17
(i"/\"j) => k = i => (j => k);
theorem :: FILTER_1:18
I is lower-bounded implies I/\/FI is 0_Lattice & Bottom (I/\/FI)
= (Bottom I)/\/FI;
theorem :: FILTER_1:19
I/\/FI is 1_Lattice & Top (I/\/FI) = (Top I)/\/FI;
registration
let I,FI;
cluster I/\/FI -> implicative;
end;
theorem :: FILTER_1:20
B/\/FB is B_Lattice;
definition
let D1,D2 be set;
let f1 be BinOp of D1;
let f2 be BinOp of D2;
redefine func |:f1,f2:| -> BinOp of [:D1,D2:];
end;
theorem :: FILTER_1:21
|:f1,f2:|.([a1,a2],[b1,b2]) = [f1.(a1,b1),f2.(a2,b2)];
scheme :: FILTER_1:sch 4
AuxCart1 { D1() -> non empty set, D2() -> non empty set, P[set] }: for d
being Element of [:D1(),D2():] holds P[d]
provided
for d1 being Element of D1(), d2 being Element of D2() holds P[[d1, d2]];
scheme :: FILTER_1:sch 5
AuxCart2 { D1() -> non empty set, D2() -> non empty set, P[set,set] }: for d
,d9 being Element of [:D1(),D2():] holds P[d,d9]
provided
for d1,d19 being Element of D1(), d2,d29 being Element of D2() holds
P[[d1,d2],[d19,d29]];
scheme :: FILTER_1:sch 6
AuxCart3 { D1() -> non empty set, D2() -> non empty set, P[set,set,set] }:
for a,b,c being Element of [:D1(),D2():] holds P[a,b,c]
provided
for a1,b1,c1 being Element of D1(), a2,b2,c2 being Element of D2()
holds P[[a1,a2],[b1,b2],[c1,c2]];
theorem :: FILTER_1:22
f1 is commutative & f2 is commutative iff |:f1,f2:| is commutative;
theorem :: FILTER_1:23
f1 is associative & f2 is associative iff |:f1,f2:| is associative;
theorem :: FILTER_1:24
a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 iff [a1,a2
] is_a_left_unity_wrt |:f1,f2:|;
theorem :: FILTER_1:25
a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 iff [a1,
a2] is_a_right_unity_wrt |:f1,f2:|;
theorem :: FILTER_1:26
a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 iff [a1,a2] is_a_unity_wrt
|:f1,f2:|;
theorem :: FILTER_1:27
f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2
iff |:f1,f2:| is_left_distributive_wrt |:g1,g2:|;
theorem :: FILTER_1:28
f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt
g2 iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:|;
theorem :: FILTER_1:29
f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 iff |:f1,
f2:| is_distributive_wrt |:g1,g2:|;
theorem :: FILTER_1:30
f1 absorbs g1 & f2 absorbs g2 iff |:f1,f2:| absorbs |:g1,g2:|;
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:|#);
end;
registration
let L1,L2 be non empty LattStr;
cluster [:L1,L2:] -> non empty;
end;
definition
let L be Lattice;
func LattRel L -> Relation equals
:: FILTER_1:def 8
{ [p,q] where p is Element of L, q is
Element of L: p [= q };
end;
theorem :: FILTER_1:31
[p,q] in LattRel L iff p [= q;
theorem :: FILTER_1:32
dom LattRel L = the carrier of L & rng LattRel L = the carrier
of L & field LattRel L = the carrier of L;
definition
let L1,L2 be Lattice;
pred L1,L2 are_isomorphic means
:: FILTER_1:def 9
LattRel L1, LattRel L2 are_isomorphic;
reflexivity;
symmetry;
end;
registration
let L1,L2 be Lattice;
cluster [:L1,L2:] -> Lattice-like;
end;
theorem :: FILTER_1:33
for L1,L2,L3 being Lattice st L1,L2 are_isomorphic & L2,L3
are_isomorphic holds L1,L3 are_isomorphic;
theorem :: FILTER_1:34
for L1,L2 being non empty LattStr st [:L1,L2:] is Lattice holds L1 is
Lattice & L2 is Lattice;
definition
let L1,L2 be Lattice;
let a be Element of L1, b be Element of L2;
redefine func [a,b] -> Element of [:L1,L2:];
end;
theorem :: FILTER_1:35
[p1,p2] "\/" [q1,q2] = [p1"\/"q1,p2"\/"q2] & [p1,p2] "/\" [q1,q2] = [
p1"/\"q1,p2"/\"q2];
theorem :: FILTER_1:36
[p1,p2] [= [q1,q2] iff p1 [= q1 & p2 [= q2;
theorem :: FILTER_1:37
L1 is modular & L2 is modular iff [:L1,L2:] is modular;
theorem :: FILTER_1:38
L1 is D_Lattice & L2 is D_Lattice iff [:L1,L2:] is D_Lattice;
theorem :: FILTER_1:39
L1 is lower-bounded & L2 is lower-bounded iff [:L1,L2:] is lower-bounded;
theorem :: FILTER_1:40
L1 is upper-bounded & L2 is upper-bounded iff [:L1,L2:] is upper-bounded;
theorem :: FILTER_1:41
L1 is bounded & L2 is bounded iff [:L1,L2:] is bounded;
theorem :: FILTER_1:42
L1 is 0_Lattice & L2 is 0_Lattice implies Bottom [:L1,L2:] = [
Bottom L1, Bottom L2];
theorem :: FILTER_1:43
L1 is 1_Lattice & L2 is 1_Lattice implies Top [:L1,L2:] = [Top L1,Top L2];
theorem :: FILTER_1:44
L1 is 01_Lattice & L2 is 01_Lattice implies (p1
is_a_complement_of q1 & p2 is_a_complement_of q2 iff [p1,p2] is_a_complement_of
[q1,q2]);
theorem :: FILTER_1:45
L1 is C_Lattice & L2 is C_Lattice iff [:L1,L2:] is C_Lattice;
theorem :: FILTER_1:46
L1 is B_Lattice & L2 is B_Lattice iff [:L1,L2:] is B_Lattice;
theorem :: FILTER_1:47
L1 is implicative & L2 is implicative iff [:L1,L2:] is implicative;
theorem :: FILTER_1:48
[:L1,L2:].: = [:L1.:,L2.: :];
theorem :: FILTER_1:49
[:L1,L2:], [:L2,L1:] are_isomorphic;
reserve B for B_Lattice,
a,b,c,d for Element of B;
theorem :: FILTER_1:50
a <=> b = (a"/\"b)"\/"(a`"/\"b`);
theorem :: FILTER_1:51
(a => b)` = a "/\" b` & (a <=> b)` = (a "/\" b`) "\/" (a` "/\" b
) & (a <=> b)` = a <=> b` & (a <=> b)` = a` <=> b;
theorem :: FILTER_1:52
a <=> b = a <=> c implies b = c;
theorem :: FILTER_1:53
a <=> (a <=> b) = b;
theorem :: FILTER_1:54
(i"\/"j) => i = j => i & i => (i"/\"j) = i => j;
theorem :: FILTER_1:55
i => j [= i => (j"\/"k) & i => j [= (i"/\"k) => j & i => j [= i
=> (k"\/"j) & i => j [= (k"/\"i) => j;
theorem :: FILTER_1:56
(i => k)"/\"(j => k) [= (i"\/"j) => k;
theorem :: FILTER_1:57
(i => j)"/\"(i => k) [= i => (j"/\"k);
theorem :: FILTER_1:58
i1 <=> i2 in FI & j1 <=> j2 in FI implies (i1"\/"j1) <=> (i2"\/"
j2) in FI & (i1"/\"j1) <=> (i2"/\"j2) in FI;
theorem :: FILTER_1:59
i in Class(equivalence_wrt FI,k) & j in Class(equivalence_wrt FI
,k) implies i"\/"j in Class(equivalence_wrt FI,k) & i"/\" j in Class(
equivalence_wrt FI,k);
theorem :: FILTER_1:60
c"\/"(c <=>d) in Class(equivalence_wrt <.d.),c) & for b st b in
Class(equivalence_wrt <.d.),c) holds b [= c"\/"(c <=>d);
theorem :: FILTER_1:61
B, [:B/\/<.a.),latt <.a.):] are_isomorphic;