:: Introduction to Lattice Theory
:: by Stanis{\l}aw \.Zukowski
::
:: Received April 14, 1989
:: Copyright (c) 1990-2021 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 STRUCT_0, BINOP_1, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1,
FUNCT_1, PBOOLE, XXREAL_2, CAT_1, LATTICES, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, CARD_1, STRUCT_0, BINOP_1;
constructors BINOP_1, STRUCT_0;
registrations XBOOLE_0, SUBSET_1, CARD_1, STRUCT_0;
requirements SUBSET, BOOLE;
begin
definition
struct(1-sorted) /\-SemiLattStr (# carrier -> set, L_meet -> BinOp of the
carrier #);
end;
definition
struct (1-sorted) \/-SemiLattStr (# carrier -> set, L_join -> BinOp of the
carrier #);
end;
definition
struct (/\-SemiLattStr,\/-SemiLattStr) LattStr (# carrier -> set, L_join,
L_meet -> BinOp of the carrier #);
end;
registration
let D be non empty set, u be BinOp of D;
cluster \/-SemiLattStr (# D, u #) -> non empty;
cluster /\-SemiLattStr (# D, u #) -> non empty;
end;
registration
let D be non empty set, u,n be BinOp of D;
cluster LattStr (# D, u, n #) -> non empty;
end;
registration
cluster 1-element strict for \/-SemiLattStr;
cluster 1-element strict for /\-SemiLattStr;
cluster 1-element strict for LattStr;
end;
definition
let G be non empty \/-SemiLattStr, p, q be Element of G;
func p"\/"q -> Element of G equals
:: LATTICES:def 1
(the L_join of G).(p,q);
end;
definition
let G be non empty /\-SemiLattStr, p, q be Element of G;
func p"/\"q -> Element of G equals
:: LATTICES:def 2
(the L_meet of G).(p,q);
end;
definition
let G be non empty \/-SemiLattStr, p, q be Element of G;
pred p [= q means
:: LATTICES:def 3
p"\/"q = q;
end;
definition
let IT be non empty \/-SemiLattStr;
attr IT is join-commutative means
:: LATTICES:def 4
for a,b being Element of IT holds a "\/"b = b"\/"a;
attr IT is join-associative means
:: LATTICES:def 5
for a,b,c being Element of IT holds a"\/"(b"\/"c) = (a"\/"b)"\/"c;
end;
definition
let IT be non empty /\-SemiLattStr;
attr IT is meet-commutative means
:: LATTICES:def 6
for a,b being Element of IT holds a "/\"b = b"/\"a;
attr IT is meet-associative means
:: LATTICES:def 7
for a,b,c being Element of IT holds a"/\"(b"/\"c) = (a"/\"b)"/\"c;
end;
definition
let IT be non empty LattStr;
attr IT is meet-absorbing means
:: LATTICES:def 8
for a,b being Element of IT holds (a "/\"b)"\/"b = b;
attr IT is join-absorbing means
:: LATTICES:def 9
for a,b being Element of IT holds a "/\"(a"\/"b)=a;
end;
definition
let IT be non empty LattStr;
attr IT is Lattice-like means
:: LATTICES:def 10
IT is join-commutative
join-associative meet-absorbing meet-commutative meet-associative
join-absorbing;
end;
registration
cluster Lattice-like -> join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing for non empty LattStr;
cluster join-commutative join-associative meet-absorbing meet-commutative
meet-associative join-absorbing -> Lattice-like for non empty LattStr;
end;
registration
cluster strict join-commutative join-associative for
non empty \/-SemiLattStr;
cluster strict meet-commutative meet-associative for
non empty /\-SemiLattStr;
cluster strict Lattice-like for non empty LattStr;
end;
definition
mode Lattice is Lattice-like non empty LattStr;
end;
definition
let L be join-commutative non empty \/-SemiLattStr, a, b be Element of L;
redefine func a"\/"b;
commutativity;
end;
definition
let L be meet-commutative non empty /\-SemiLattStr, a, b be Element of L;
redefine func a"/\"b;
commutativity;
end;
definition
let IT be non empty LattStr;
attr IT is distributive means
:: LATTICES:def 11
for a,b,c being Element of IT holds a "/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c);
end;
definition
let IT be non empty LattStr;
attr IT is modular means
:: LATTICES:def 12
for a,b,c being Element of IT st a [= c holds a"\/"(b"/\"c) = (a"\/"b)"/\"c;
end;
definition
let IT be non empty /\-SemiLattStr;
attr IT is lower-bounded means
:: LATTICES:def 13
ex c being Element of IT st for a
being Element of IT holds c"/\"a = c & a"/\"c = c;
end;
definition
let IT be non empty \/-SemiLattStr;
attr IT is upper-bounded means
:: LATTICES:def 14
ex c being Element of IT st for a
being Element of IT holds c"\/"a = c & a"\/"c = c;
end;
registration
cluster strict distributive lower-bounded upper-bounded modular for Lattice;
end;
definition
mode D_Lattice is distributive Lattice;
mode M_Lattice is modular Lattice;
mode 0_Lattice is lower-bounded Lattice;
mode 1_Lattice is upper-bounded Lattice;
end;
definition
let IT be non empty LattStr;
attr IT is bounded means
:: LATTICES:def 15
IT is lower-bounded upper-bounded;
end;
registration
cluster lower-bounded upper-bounded -> bounded for non empty LattStr;
cluster bounded -> lower-bounded upper-bounded for non empty LattStr;
end;
registration
cluster bounded strict for Lattice;
end;
definition
mode 01_Lattice is bounded Lattice;
end;
definition
let L be non empty /\-SemiLattStr;
assume
L is lower-bounded;
func Bottom L -> Element of L means
:: LATTICES:def 16
for a being Element of L holds it "/\" a = it & a "/\" it = it;
end;
definition
let L be non empty \/-SemiLattStr;
assume
L is upper-bounded;
func Top L -> Element of L means
:: LATTICES:def 17
for a being Element of L holds it "\/" a = it & a "\/" it = it;
end;
definition
let L be non empty LattStr, a, b be Element of L;
pred a is_a_complement_of b means
:: LATTICES:def 18
a"\/"b = Top L & b"\/"a = Top L & a"/\"b = Bottom L & b"/\"a = Bottom L;
end;
definition
let IT be non empty LattStr;
attr IT is complemented means
:: LATTICES:def 19
for b being Element of IT ex a being Element of IT st a is_a_complement_of b;
end;
registration
cluster bounded complemented strict for Lattice;
end;
definition
mode C_Lattice is complemented 01_Lattice;
end;
definition
let IT be non empty LattStr;
attr IT is Boolean means
:: LATTICES:def 20
IT is bounded complemented distributive;
end;
registration
cluster Boolean -> bounded complemented distributive for non empty LattStr;
cluster bounded complemented distributive -> Boolean for non empty LattStr;
end;
registration
cluster Boolean strict for Lattice;
end;
definition
mode B_Lattice is Boolean Lattice;
end;
registration
let L be meet-absorbing join-absorbing meet-commutative non empty LattStr,
a be Element of L;
reduce a "\/" a to a;
end;
registration
let L be meet-absorbing join-absorbing meet-commutative non empty LattStr,
a be Element of L;
reduce a "/\" a to a;
end;
::$CT 2
theorem :: LATTICES:3
for L being Lattice holds (for a,b,c being Element of L holds a
"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c)) iff for a,b,c being Element of L holds a
"\/"(b"/\"c) = (a"\/"b)"/\"(a"\/"c);
theorem :: LATTICES:4
for L being meet-absorbing join-absorbing non empty LattStr,
a, b being Element of L holds a [= b iff a"/\"b = a;
theorem :: LATTICES:5
for L being meet-absorbing join-absorbing join-associative
meet-commutative non empty LattStr, a, b being Element of L holds a [= a"\/"b;
theorem :: LATTICES:6
for L being meet-absorbing meet-commutative non empty LattStr,
a, b being Element of L holds a"/\"b [= a;
definition
let L be meet-absorbing join-absorbing meet-commutative non empty LattStr,
a, b be Element of L;
redefine pred a [= b;
reflexivity;
end;
theorem :: LATTICES:7
for L being join-associative non empty \/-SemiLattStr, a, b, c being
Element of L holds a [= b & b [= c implies a [= c;
theorem :: LATTICES:8
for L being join-commutative non empty \/-SemiLattStr, a, b
being Element of L holds a [= b & b [= a implies a=b;
theorem :: LATTICES:9
for L being meet-absorbing join-absorbing meet-associative non
empty LattStr, a, b, c being Element of L holds a [= b implies a"/\"c [= b"/\"
c;
theorem :: LATTICES:10
for L being Lattice holds (for a,b,c being Element of L holds (a"/\"b)
"\/"(b"/\"c)"\/"(c"/\"a) = (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a)) implies L is
distributive;
reserve L for D_Lattice;
reserve a, b, c for Element of L;
theorem :: LATTICES:11
a"\/"(b"/\"c) = (a"\/"b)"/\"(a"\/"c);
theorem :: LATTICES:12
c"/\"a = c"/\"b & c"\/"a = c"\/"b implies a=b;
theorem :: LATTICES:13
(a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) = (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a);
registration
cluster distributive -> modular for Lattice;
end;
registration
let L be 0_Lattice, a be Element of L;
reduce Bottom L "\/" a to a;
reduce Bottom L "/\" a to Bottom L;
end;
theorem :: LATTICES:14
for L being 0_Lattice, a being Element of L holds Bottom L "\/" a = a;
theorem :: LATTICES:15
for L being 0_Lattice, a being Element of L holds Bottom L "/\" a = Bottom L;
theorem :: LATTICES:16
for L being 0_Lattice, a being Element of L holds Bottom L [= a;
registration
let L be 1_Lattice, a be Element of L;
reduce Top L"/\"a to a;
reduce Top L"\/"a to Top L;
end;
theorem :: LATTICES:17
for L being 1_Lattice, a being Element of L holds Top L"/\"a = a;
theorem :: LATTICES:18
for L being 1_Lattice, a being Element of L holds Top L"\/"a = Top L;
theorem :: LATTICES:19
for L being 1_Lattice, a being Element of L holds a [= Top L;
definition
let L be non empty LattStr, x be Element of L;
assume
L is complemented D_Lattice;
func x` -> Element of L means
:: LATTICES:def 21
it is_a_complement_of x;
end;
reserve L for B_Lattice;
reserve a, b for Element of L;
theorem :: LATTICES:20
a`"/\"a = Bottom L;
theorem :: LATTICES:21
a`"\/"a = Top L;
registration let L,a;
reduce a`` to a;
end;
theorem :: LATTICES:22
a`` = a;
theorem :: LATTICES:23
( a"/\"b )` = a`"\/" b`;
theorem :: LATTICES:24
( a"\/"b )` = a`"/\" b`;
theorem :: LATTICES:25
b"/\"a = Bottom L iff b [= a`;
theorem :: LATTICES:26
a [= b implies b` [= a`;
begin :: Addenda
:: missing, 2009.07.28, A.T.
definition let L be non empty LattStr, S be Subset of L;
attr S is initial means
:: LATTICES:def 22
for p,q being Element of L st p [= q & q in S holds p in S;
attr S is final means
:: LATTICES:def 23
for p,q being Element of L st p [= q & p in S holds q in S;
attr S is meet-closed means
:: LATTICES:def 24
for p,q being Element of L st p in S & q in S holds p "/\" q in S;
attr S is join-closed means
:: LATTICES:def 25
for p,q being Element of L st p in S & q in S holds p "\/" q in S;
end;
registration let L be non empty LattStr;
cluster [#]L -> initial final non empty;
end;
registration let L be non empty LattStr;
cluster initial final non empty for Subset of L;
cluster empty -> initial final for Subset of L;
end;
registration let L be Lattice;
cluster initial final non empty for Subset of L;
end;
registration
let L be meet-absorbing meet-commutative non empty LattStr;
cluster initial -> meet-closed for Subset of L;
end;
registration
let L be meet-absorbing join-absorbing join-associative
meet-commutative non empty LattStr;
cluster final -> join-closed for Subset of L;
end;
theorem :: LATTICES:27
for L being Lattice, S being initial final non empty Subset of L
holds S = [#]L;