:: Finite Join and Finite Meet, and Dual Lattices
:: by Andrzej Trybulec
::
:: Received August 10, 1990
:: Copyright (c) 1990-2017 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 XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4, TARSKI, FINSUB_1,
BINOP_1, LATTICES, EQREL_1, STRUCT_0, PBOOLE, SETWISEO, FUNCOP_1,
FILTER_0, FINSET_1, XXREAL_2, LATTICE2;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4,
PARTFUN1, FUNCOP_1, BINOP_1, FINSET_1, STRUCT_0, LATTICES, FINSUB_1,
SETWISEO, FILTER_0;
constructors BINOP_1, FUNCOP_1, FUNCT_4, SETWISEO, GROUP_1, FILTER_0,
RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES,
RELSET_1, FILTER_0;
requirements SUBSET, BOOLE;
begin :: Auxiliary theorems
reserve A for set,
C for non empty set,
B for Subset of A,
x for Element of A,
f,g for Function of A,C;
theorem :: LATTICE2:1
dom (g|B) = B;
theorem :: LATTICE2:2
f|B = g|B iff for x st x in B holds g.x = f.x;
theorem :: LATTICE2:3
for B being set holds f +* g|B is Function of A,C;
theorem :: LATTICE2:4
g|B +* f = f;
theorem :: LATTICE2:5
for f,g being Function holds g c= f implies f +* g = f;
theorem :: LATTICE2:6
f +* f|B = f;
theorem :: LATTICE2:7
(for x st x in B holds g.x = f.x) implies f +* g|B = f;
reserve B for Element of Fin A;
theorem :: LATTICE2:8
g|B +* f = f;
theorem :: LATTICE2:9
dom (g|B) = B;
theorem :: LATTICE2:10
(for x st x in B holds g.x = f.x) implies f +* g|B = f;
definition
let D be non empty set;
let o,o9 be BinOp of D;
pred o absorbs o9 means
:: LATTICE2:def 1
for x,y being Element of D holds o.(x,o9.(x,y )) = x;
end;
notation
let D be non empty set;
let o,o9 be BinOp of D;
antonym o doesn't_absorb o9 for o absorbs o9;
end;
:: Dual Lattice structures
reserve L for non empty LattStr,
a,b,c for Element of L;
theorem :: LATTICE2:11
the L_join of L is commutative associative & the L_meet of L is
commutative associative & the L_join of L absorbs the L_meet of L & the L_meet
of L absorbs the L_join of L implies L is Lattice-like;
definition
let L be LattStr;
func L.: -> strict LattStr equals
:: LATTICE2:def 2
LattStr(#the carrier of L, the L_meet of L
, the L_join of L#);
end;
registration
let L be non empty LattStr;
cluster L.: -> non empty;
end;
theorem :: LATTICE2:12
the carrier of L = the carrier of L.: & the L_join of L = the L_meet
of L.: & the L_meet of L = the L_join of L.:;
theorem :: LATTICE2:13
for L being strict non empty LattStr holds L .: .: = L;
:: General Lattices
reserve L for Lattice;
reserve a,b,c,u,v for Element of L;
theorem :: LATTICE2:14
(for v holds u "\/" v = v) implies u = Bottom L;
theorem :: LATTICE2:15
(for v holds (the L_join of L).(u,v) = v) implies u = Bottom L;
theorem :: LATTICE2:16
(for v holds u "/\" v = v) implies u = Top L;
theorem :: LATTICE2:17
(for v holds (the L_meet of L).(u,v) = v) implies u = Top L;
registration
let L;
cluster the L_join of L -> idempotent;
end;
registration
let L be join-commutative non empty \/-SemiLattStr;
cluster the L_join of L -> commutative;
end;
theorem :: LATTICE2:18
the L_join of L is having_a_unity implies Bottom L =
the_unity_wrt the L_join of L;
registration
let L be join-associative non empty \/-SemiLattStr;
cluster the L_join of L -> associative;
end;
registration
let L;
cluster the L_meet of L -> idempotent;
end;
registration
let L be meet-commutative non empty /\-SemiLattStr;
cluster the L_meet of L -> commutative;
end;
registration
let L be meet-associative non empty /\-SemiLattStr;
cluster the L_meet of L -> associative;
end;
theorem :: LATTICE2:19
the L_meet of L is having_a_unity implies Top L = the_unity_wrt
the L_meet of L;
theorem :: LATTICE2:20
the L_join of L is_distributive_wrt the L_join of L;
theorem :: LATTICE2:21
L is D_Lattice implies the L_join of L is_distributive_wrt the L_meet of L;
theorem :: LATTICE2:22
the L_join of L is_distributive_wrt the L_meet of L implies L is distributive
;
theorem :: LATTICE2:23
L is D_Lattice implies the L_meet of L is_distributive_wrt the L_join of L;
theorem :: LATTICE2:24
the L_meet of L is_distributive_wrt the L_join of L implies L is distributive
;
theorem :: LATTICE2:25
the L_meet of L is_distributive_wrt the L_meet of L;
theorem :: LATTICE2:26
the L_join of L absorbs the L_meet of L;
theorem :: LATTICE2:27
the L_meet of L absorbs the L_join of L;
definition
let A be non empty set, L be Lattice;
let B be Element of Fin A;
let f be Function of A, the carrier of L;
func FinJoin(B, f) -> Element of L equals
:: LATTICE2:def 3
(the L_join of L)$$(B,f);
func FinMeet(B, f) -> Element of L equals
:: LATTICE2:def 4
(the L_meet of L)$$(B,f);
end;
reserve A for non empty set,
x for Element of A,
B for Element of Fin A,
f,g for Function of A, the carrier of L;
theorem :: LATTICE2:28
x in B implies f.x [= FinJoin(B,f);
theorem :: LATTICE2:29
(ex x st x in B & u [= f.x) implies u [= FinJoin(B,f);
theorem :: LATTICE2:30
(for x st x in B holds f.x = u) & B <> {} implies FinJoin(B,f) = u;
theorem :: LATTICE2:31
FinJoin(B,f) [= u implies for x st x in B holds f.x [= u;
theorem :: LATTICE2:32
B <> {} & (for x st x in B holds f.x [= u) implies FinJoin(B,f) [= u;
theorem :: LATTICE2:33
B <> {} & (for x st x in B holds f.x [= g.x) implies FinJoin(B,f) [=
FinJoin(B,g);
theorem :: LATTICE2:34
B <> {} & f|B = g|B implies FinJoin(B,f) = FinJoin(B,g);
theorem :: LATTICE2:35
B <> {} implies v "\/" FinJoin(B,f) = FinJoin(B, (the L_join of L)[;](
v, f ) );
registration
let L be Lattice;
cluster L.: -> Lattice-like;
end;
theorem :: LATTICE2:36
for L being Lattice, B being Element of Fin A for f being Function
of A, the carrier of L, f9 being Function of A, the carrier of L.: st f = f9
holds FinJoin(B,f) = FinMeet(B,f9) & FinMeet(B,f) = FinJoin(B,f9);
theorem :: LATTICE2:37
for a9,b9 being Element of L.: st a = a9 & b = b9 holds a "/\" b
= a9"\/" b9 & a "\/" b = a9"/\" b9;
theorem :: LATTICE2:38
a [= b implies for a9,b9 being Element of L.: st a = a9 & b = b9
holds b9 [= a9;
theorem :: LATTICE2:39
for a9,b9 being Element of L.: st a9 [= b9 & a = a9 & b = b9 holds b [= a;
:: Dualizations
theorem :: LATTICE2:40
x in B implies FinMeet(B,f) [= f.x;
theorem :: LATTICE2:41
(ex x st x in B & f.x [= u) implies FinMeet(B,f)[= u;
theorem :: LATTICE2:42
(for x st x in B holds f.x = u) & B <> {} implies FinMeet(B,f) = u;
theorem :: LATTICE2:43
B <> {} implies v "/\" FinMeet(B,f) = FinMeet(B, (the L_meet of L)[;](
v, f ) );
theorem :: LATTICE2:44
u [= FinMeet(B,f) implies for x st x in B holds u [= f.x;
theorem :: LATTICE2:45
B <> {} & f|B = g|B implies FinMeet(B,f) = FinMeet(B,g);
theorem :: LATTICE2:46
B <> {} & (for x st x in B holds u [= f.x) implies u [= FinMeet( B,f);
theorem :: LATTICE2:47
B <> {} & (for x st x in B holds f.x [= g.x) implies FinMeet(B,f) [=
FinMeet(B,g);
theorem :: LATTICE2:48
for L being Lattice holds L is lower-bounded iff L.: is upper-bounded;
theorem :: LATTICE2:49
for L being Lattice holds L is upper-bounded iff L.: is lower-bounded;
theorem :: LATTICE2:50
L is D_Lattice iff L.: is D_Lattice;
::
:: Lower bounded lattices
::
reserve L for 0_Lattice,
f,g for Function of A, the carrier of L,
u for Element of L;
theorem :: LATTICE2:51
Bottom L is_a_unity_wrt the L_join of L;
registration
let L;
cluster the L_join of L -> having_a_unity;
end;
theorem :: LATTICE2:52
Bottom L = the_unity_wrt the L_join of L;
theorem :: LATTICE2:53
f|B = g|B implies FinJoin(B,f) = FinJoin(B,g);
theorem :: LATTICE2:54
(for x st x in B holds f.x [= u) implies FinJoin(B,f) [= u;
theorem :: LATTICE2:55
(for x st x in B holds f.x [= g.x) implies FinJoin(B,f) [= FinJoin(B,g );
::
:: Upper bounded lattices
::
reserve L for 1_Lattice,
f,g for Function of A, the carrier of L,
u for Element of L;
theorem :: LATTICE2:56
Top L is_a_unity_wrt the L_meet of L;
registration
let L;
cluster the L_meet of L -> having_a_unity;
end;
theorem :: LATTICE2:57
Top L = the_unity_wrt the L_meet of L;
theorem :: LATTICE2:58
f|B = g|B implies FinMeet(B,f) = FinMeet(B,g);
theorem :: LATTICE2:59
(for x st x in B holds u [= f.x) implies u [= FinMeet(B,f);
theorem :: LATTICE2:60
(for x st x in B holds f.x [= g.x) implies FinMeet(B,f) [= FinMeet(B,g );
theorem :: LATTICE2:61
for L being 0_Lattice holds Bottom L = Top (L.:);
theorem :: LATTICE2:62
for L being 1_Lattice holds Top L = Bottom (L.:);
::
:: Distributive lattices with the minimal element
::
definition
mode D0_Lattice is distributive lower-bounded Lattice;
end;
reserve L for D0_Lattice,
f,g for (Function of A, the carrier of L),
u for Element of L;
theorem :: LATTICE2:63
the L_meet of L is_distributive_wrt the L_join of L;
theorem :: LATTICE2:64
(the L_meet of L).(u, FinJoin(B, f)) = FinJoin(B, (the L_meet of L)[;](u,f));
theorem :: LATTICE2:65
(for x st x in B holds g.x = u "/\" f.x) implies u "/\" FinJoin(B,f) =
FinJoin(B,g);
theorem :: LATTICE2:66
u "/\" FinJoin(B,f) = FinJoin(B, (the L_meet of L)[;](u, f));
:: Heyting Lattices
definition
let IT be Lattice;
attr IT is Heyting means
:: LATTICE2:def 5
IT is implicative lower-bounded;
end;
registration
cluster Heyting for Lattice;
end;
registration
cluster Heyting -> implicative lower-bounded for Lattice;
cluster implicative lower-bounded -> Heyting for Lattice;
end;
definition
mode H_Lattice is Heyting Lattice;
end;
registration
cluster Heyting strict for Lattice;
end;
theorem :: LATTICE2:67
for L being 0_Lattice holds L is H_Lattice iff for x,z being Element
of L ex y being Element of L st x "/\" y [= z & for v being Element of L st x
"/\" v [= z holds v [= y;
theorem :: LATTICE2:68
for L being Lattice holds L is finite iff L.: is finite;
registration
cluster finite -> lower-bounded for Lattice;
cluster finite -> upper-bounded for Lattice;
end;
registration
cluster finite -> bounded for Lattice;
end;
registration
cluster distributive finite -> Heyting for Lattice;
end;