:: Introduction to Lattice Theory :: by Stanis{\l}aw \.Zukowski :: :: Received April 14, 1989 :: Copyright (c) 1990-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 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, NUMERALS; 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 Lattice, 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 Lattice; cluster [#]L -> initial final non empty; end; registration let L be Lattice; cluster initial final non empty for Subset of L; cluster empty -> initial final for Subset of L; cluster initial -> meet-closed for Subset of L; 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;