:: Introduction to Lattice Theory :: by Stanis{\l}aw \.Zukowski :: :: Received April 14, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition attrc1 is strict ; struct /\-SemiLattStr -> 1-sorted ; aggr/\-SemiLattStr(# carrier, L_meet #) -> /\-SemiLattStr ; sel L_meet c1 -> BinOp of the carrier of c1; end; definition attrc1 is strict ; struct \/-SemiLattStr -> 1-sorted ; aggr\/-SemiLattStr(# carrier, L_join #) -> \/-SemiLattStr ; sel L_join c1 -> BinOp of the carrier of c1; end; definition attrc1 is strict ; struct LattStr -> /\-SemiLattStr , \/-SemiLattStr ; aggrLattStr(# carrier, L_join, L_meet #) -> LattStr ; end; registration let D be non empty set ; let u be BinOp of D; cluster \/-SemiLattStr(# D,u #) -> non empty ; coherence not \/-SemiLattStr(# D,u #) is empty ; cluster /\-SemiLattStr(# D,u #) -> non empty ; coherence not /\-SemiLattStr(# D,u #) is empty ; end; registration let D be non empty set ; let u, n be BinOp of D; cluster LattStr(# D,u,n #) -> non empty ; coherence not LattStr(# D,u,n #) is empty ; end; registration cluster1 -element strict for \/-SemiLattStr ; existence ex b1 being \/-SemiLattStr st ( b1 is 1 -element & b1 is strict ) proofend; cluster1 -element strict for /\-SemiLattStr ; existence ex b1 being /\-SemiLattStr st ( b1 is 1 -element & b1 is strict ) proofend; cluster1 -element strict for LattStr ; existence ex b1 being LattStr st ( b1 is 1 -element & b1 is strict ) proofend; end; definition let G be non empty \/-SemiLattStr ; let p, q be Element of G; funcp "\/" q -> Element of G equals :: LATTICES:def 1 the L_join of G . (p,q); coherence the L_join of G . (p,q) is Element of G ; end; :: deftheorem defines "\/" LATTICES:def_1_:_ for G being non empty \/-SemiLattStr for p, q being Element of G holds p "\/" q = the L_join of G . (p,q); definition let G be non empty /\-SemiLattStr ; let p, q be Element of G; funcp "/\" q -> Element of G equals :: LATTICES:def 2 the L_meet of G . (p,q); coherence the L_meet of G . (p,q) is Element of G ; end; :: deftheorem defines "/\" LATTICES:def_2_:_ for G being non empty /\-SemiLattStr for p, q being Element of G holds p "/\" q = the L_meet of G . (p,q); definition let G be non empty \/-SemiLattStr ; let p, q be Element of G; predp [= q means :Def3: :: LATTICES:def 3 p "\/" q = q; end; :: deftheorem Def3 defines [= LATTICES:def_3_:_ for G being non empty \/-SemiLattStr for p, q being Element of G holds ( p [= q iff p "\/" q = q ); Lm1: for uu, nn being BinOp of (bool {}) for x, y being Element of LattStr(# (bool {}),uu,nn #) holds x = y proofend; Lm2: for n being BinOp of (bool {}) for x, y being Element of \/-SemiLattStr(# (bool {}),n #) holds x = y proofend; Lm3: for n being BinOp of (bool {}) for x, y being Element of /\-SemiLattStr(# (bool {}),n #) holds x = y proofend; definition let IT be non empty \/-SemiLattStr ; attrIT is join-commutative means :Def4: :: LATTICES:def 4 for a, b being Element of IT holds a "\/" b = b "\/" a; attrIT is join-associative means :Def5: :: LATTICES:def 5 for a, b, c being Element of IT holds a "\/" (b "\/" c) = (a "\/" b) "\/" c; end; :: deftheorem Def4 defines join-commutative LATTICES:def_4_:_ for IT being non empty \/-SemiLattStr holds ( IT is join-commutative iff for a, b being Element of IT holds a "\/" b = b "\/" a ); :: deftheorem Def5 defines join-associative LATTICES:def_5_:_ for IT being non empty \/-SemiLattStr holds ( IT is join-associative iff for a, b, c being Element of IT holds a "\/" (b "\/" c) = (a "\/" b) "\/" c ); definition let IT be non empty /\-SemiLattStr ; attrIT is meet-commutative means :Def6: :: LATTICES:def 6 for a, b being Element of IT holds a "/\" b = b "/\" a; attrIT is meet-associative means :Def7: :: LATTICES:def 7 for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c; end; :: deftheorem Def6 defines meet-commutative LATTICES:def_6_:_ for IT being non empty /\-SemiLattStr holds ( IT is meet-commutative iff for a, b being Element of IT holds a "/\" b = b "/\" a ); :: deftheorem Def7 defines meet-associative LATTICES:def_7_:_ for IT being non empty /\-SemiLattStr holds ( IT is meet-associative iff for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c ); definition let IT be non empty LattStr ; attrIT is meet-absorbing means :Def8: :: LATTICES:def 8 for a, b being Element of IT holds (a "/\" b) "\/" b = b; attrIT is join-absorbing means :Def9: :: LATTICES:def 9 for a, b being Element of IT holds a "/\" (a "\/" b) = a; end; :: deftheorem Def8 defines meet-absorbing LATTICES:def_8_:_ for IT being non empty LattStr holds ( IT is meet-absorbing iff for a, b being Element of IT holds (a "/\" b) "\/" b = b ); :: deftheorem Def9 defines join-absorbing LATTICES:def_9_:_ for IT being non empty LattStr holds ( IT is join-absorbing iff for a, b being Element of IT holds a "/\" (a "\/" b) = a ); definition let IT be non empty LattStr ; attrIT is Lattice-like means :Def10: :: LATTICES:def 10 ( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing ); end; :: deftheorem Def10 defines Lattice-like LATTICES:def_10_:_ for IT being non empty LattStr holds ( IT is Lattice-like iff ( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing ) ); registration cluster non empty Lattice-like -> non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing for LattStr ; coherence for b1 being non empty LattStr st b1 is Lattice-like holds ( b1 is join-commutative & b1 is join-associative & b1 is meet-absorbing & b1 is meet-commutative & b1 is meet-associative & b1 is join-absorbing ) by Def10; cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing -> non empty Lattice-like for LattStr ; coherence for b1 being non empty LattStr st b1 is join-commutative & b1 is join-associative & b1 is meet-absorbing & b1 is meet-commutative & b1 is meet-associative & b1 is join-absorbing holds b1 is Lattice-like by Def10; end; registration cluster non empty strict join-commutative join-associative for \/-SemiLattStr ; existence ex b1 being non empty \/-SemiLattStr st ( b1 is strict & b1 is join-commutative & b1 is join-associative ) proofend; cluster non empty strict meet-commutative meet-associative for /\-SemiLattStr ; existence ex b1 being non empty /\-SemiLattStr st ( b1 is strict & b1 is meet-commutative & b1 is meet-associative ) proofend; cluster non empty strict Lattice-like for LattStr ; existence ex b1 being non empty LattStr st ( b1 is strict & b1 is Lattice-like ) proofend; end; definition mode Lattice is non empty Lattice-like LattStr ; end; definition let L be non empty join-commutative \/-SemiLattStr ; let a, b be Element of L; :: original:"\/" redefine funca "\/" b -> Element of L; commutativity for a, b being Element of L holds a "\/" b = b "\/" a by Def4; end; definition let L be non empty meet-commutative /\-SemiLattStr ; let a, b be Element of L; :: original:"/\" redefine funca "/\" b -> Element of L; commutativity for a, b being Element of L holds a "/\" b = b "/\" a by Def6; end; definition let IT be non empty LattStr ; attrIT is distributive means :Def11: :: LATTICES:def 11 for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c); end; :: deftheorem Def11 defines distributive LATTICES:def_11_:_ for IT being non empty LattStr holds ( IT is distributive iff for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ); definition let IT be non empty LattStr ; attrIT is modular means :Def12: :: LATTICES:def 12 for a, b, c being Element of IT st a [= c holds a "\/" (b "/\" c) = (a "\/" b) "/\" c; end; :: deftheorem Def12 defines modular LATTICES:def_12_:_ for IT being non empty LattStr holds ( IT is modular iff for a, b, c being Element of IT st a [= c holds a "\/" (b "/\" c) = (a "\/" b) "/\" c ); definition let IT be non empty /\-SemiLattStr ; attrIT is lower-bounded means :Def13: :: LATTICES:def 13 ex c being Element of IT st for a being Element of IT holds ( c "/\" a = c & a "/\" c = c ); end; :: deftheorem Def13 defines lower-bounded LATTICES:def_13_:_ for IT being non empty /\-SemiLattStr holds ( IT is lower-bounded iff ex c being Element of IT st for a being Element of IT holds ( c "/\" a = c & a "/\" c = c ) ); definition let IT be non empty \/-SemiLattStr ; attrIT is upper-bounded means :Def14: :: LATTICES:def 14 ex c being Element of IT st for a being Element of IT holds ( c "\/" a = c & a "\/" c = c ); end; :: deftheorem Def14 defines upper-bounded LATTICES:def_14_:_ for IT being non empty \/-SemiLattStr holds ( IT is upper-bounded iff ex c being Element of IT st for a being Element of IT holds ( c "\/" a = c & a "\/" c = c ) ); Lm4: for n, u being BinOp of (bool {}) holds LattStr(# (bool {}),n,u #) is Lattice proofend; registration cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded for LattStr ; existence ex b1 being Lattice st ( b1 is strict & b1 is distributive & b1 is lower-bounded & b1 is upper-bounded & b1 is modular ) proofend; 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; Lm5: for n, u being BinOp of (bool {}) holds LattStr(# (bool {}),n,u #) is 0_Lattice proofend; Lm6: for n, u being BinOp of (bool {}) holds LattStr(# (bool {}),n,u #) is 1_Lattice proofend; definition let IT be non empty LattStr ; attrIT is bounded means :Def15: :: LATTICES:def 15 ( IT is lower-bounded & IT is upper-bounded ); end; :: deftheorem Def15 defines bounded LATTICES:def_15_:_ for IT being non empty LattStr holds ( IT is bounded iff ( IT is lower-bounded & IT is upper-bounded ) ); registration cluster non empty lower-bounded upper-bounded -> non empty bounded for LattStr ; coherence for b1 being non empty LattStr st b1 is lower-bounded & b1 is upper-bounded holds b1 is bounded by Def15; cluster non empty bounded -> non empty lower-bounded upper-bounded for LattStr ; coherence for b1 being non empty LattStr st b1 is bounded holds ( b1 is lower-bounded & b1 is upper-bounded ) by Def15; end; registration cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like bounded for LattStr ; existence ex b1 being Lattice st ( b1 is bounded & b1 is strict ) proofend; end; definition mode 01_Lattice is bounded Lattice; end; definition let L be non empty /\-SemiLattStr ; assume A1: L is lower-bounded ; func Bottom L -> Element of L means :Def16: :: LATTICES:def 16 for a being Element of L holds ( it "/\" a = it & a "/\" it = it ); existence ex b1 being Element of L st for a being Element of L holds ( b1 "/\" a = b1 & a "/\" b1 = b1 ) by A1, Def13; uniqueness for b1, b2 being Element of L st ( for a being Element of L holds ( b1 "/\" a = b1 & a "/\" b1 = b1 ) ) & ( for a being Element of L holds ( b2 "/\" a = b2 & a "/\" b2 = b2 ) ) holds b1 = b2 proofend; end; :: deftheorem Def16 defines Bottom LATTICES:def_16_:_ for L being non empty /\-SemiLattStr st L is lower-bounded holds for b2 being Element of L holds ( b2 = Bottom L iff for a being Element of L holds ( b2 "/\" a = b2 & a "/\" b2 = b2 ) ); definition let L be non empty \/-SemiLattStr ; assume A1: L is upper-bounded ; func Top L -> Element of L means :Def17: :: LATTICES:def 17 for a being Element of L holds ( it "\/" a = it & a "\/" it = it ); existence ex b1 being Element of L st for a being Element of L holds ( b1 "\/" a = b1 & a "\/" b1 = b1 ) by A1, Def14; uniqueness for b1, b2 being Element of L st ( for a being Element of L holds ( b1 "\/" a = b1 & a "\/" b1 = b1 ) ) & ( for a being Element of L holds ( b2 "\/" a = b2 & a "\/" b2 = b2 ) ) holds b1 = b2 proofend; end; :: deftheorem Def17 defines Top LATTICES:def_17_:_ for L being non empty \/-SemiLattStr st L is upper-bounded holds for b2 being Element of L holds ( b2 = Top L iff for a being Element of L holds ( b2 "\/" a = b2 & a "\/" b2 = b2 ) ); definition let L be non empty LattStr ; let a, b be Element of L; preda is_a_complement_of b means :Def18: :: LATTICES:def 18 ( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L ); end; :: deftheorem Def18 defines is_a_complement_of LATTICES:def_18_:_ for L being non empty LattStr for a, b being Element of L holds ( a is_a_complement_of b iff ( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L ) ); definition let IT be non empty LattStr ; attrIT is complemented means :Def19: :: LATTICES:def 19 for b being Element of IT ex a being Element of IT st a is_a_complement_of b; end; :: deftheorem Def19 defines complemented LATTICES:def_19_:_ for IT being non empty LattStr holds ( IT is complemented iff for b being Element of IT ex a being Element of IT st a is_a_complement_of b ); registration cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like bounded complemented for LattStr ; existence ex b1 being Lattice st ( b1 is bounded & b1 is complemented & b1 is strict ) proofend; end; definition mode C_Lattice is complemented 01_Lattice; end; definition let IT be non empty LattStr ; attrIT is Boolean means :Def20: :: LATTICES:def 20 ( IT is bounded & IT is complemented & IT is distributive ); end; :: deftheorem Def20 defines Boolean LATTICES:def_20_:_ for IT being non empty LattStr holds ( IT is Boolean iff ( IT is bounded & IT is complemented & IT is distributive ) ); registration cluster non empty Boolean -> non empty distributive bounded complemented for LattStr ; coherence for b1 being non empty LattStr st b1 is Boolean holds ( b1 is bounded & b1 is complemented & b1 is distributive ) by Def20; cluster non empty distributive bounded complemented -> non empty Boolean for LattStr ; coherence for b1 being non empty LattStr st b1 is bounded & b1 is complemented & b1 is distributive holds b1 is Boolean by Def20; end; registration cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Boolean for LattStr ; existence ex b1 being Lattice st ( b1 is Boolean & b1 is strict ) proofend; end; definition mode B_Lattice is Boolean Lattice; end; registration let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ; let a be Element of L; reducea "\/" a to a; reducibility a "\/" a = a proofend; end; registration let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ; let a be Element of L; reducea "/\" a to a; reducibility a "/\" a = a proofend; end; theorem :: LATTICES:1 canceled; theorem :: LATTICES:2 canceled; theorem Th3: :: 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) ) proofend; theorem Th4: :: LATTICES:4 for L being non empty meet-absorbing join-absorbing LattStr for a, b being Element of L holds ( a [= b iff a "/\" b = a ) proofend; theorem Th5: :: LATTICES:5 for L being non empty join-associative meet-commutative meet-absorbing join-absorbing LattStr for a, b being Element of L holds a [= a "\/" b proofend; theorem Th6: :: LATTICES:6 for L being non empty meet-commutative meet-absorbing LattStr for a, b being Element of L holds a "/\" b [= a proofend; definition let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ; let a, b be Element of L; :: original:[= redefine preda [= b; reflexivity for a being Element of L holds (L,b1,b1) proofend; end; theorem :: LATTICES:7 for L being non empty join-associative \/-SemiLattStr for a, b, c being Element of L st a [= b & b [= c holds a [= c proofend; theorem Th8: :: LATTICES:8 for L being non empty join-commutative \/-SemiLattStr for a, b being Element of L st a [= b & b [= a holds a = b proofend; theorem Th9: :: LATTICES:9 for L being non empty meet-associative meet-absorbing join-absorbing LattStr for a, b, c being Element of L st a [= b holds a "/\" c [= b "/\" c proofend; theorem :: LATTICES:10 for L being Lattice st ( for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) ) holds L is distributive proofend; theorem Th11: :: LATTICES:11 for L being D_Lattice for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) proofend; theorem Th12: :: LATTICES:12 for L being D_Lattice for c, a, b being Element of L st c "/\" a = c "/\" b & c "\/" a = c "\/" b holds a = b proofend; theorem :: LATTICES:13 for L being D_Lattice for a, b, c being Element of L holds ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) = ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) proofend; registration cluster non empty Lattice-like distributive -> modular for LattStr ; coherence for b1 being Lattice st b1 is distributive holds b1 is modular proofend; end; registration let L be 0_Lattice; let a be Element of L; reduce(Bottom L) "\/" a to a; reducibility (Bottom L) "\/" a = a proofend; reduce(Bottom L) "/\" a to Bottom L; reducibility (Bottom L) "/\" a = Bottom L by Def16; end; theorem :: LATTICES:14 for L being 0_Lattice for a being Element of L holds (Bottom L) "\/" a = a ; theorem :: LATTICES:15 for L being 0_Lattice for a being Element of L holds (Bottom L) "/\" a = Bottom L ; theorem Th16: :: LATTICES:16 for L being 0_Lattice for a being Element of L holds Bottom L [= a proofend; registration let L be 1_Lattice; let a be Element of L; reduce(Top L) "/\" a to a; reducibility (Top L) "/\" a = a proofend; reduce(Top L) "\/" a to Top L; reducibility (Top L) "\/" a = Top L by Def17; end; theorem :: LATTICES:17 for L being 1_Lattice for a being Element of L holds (Top L) "/\" a = a ; theorem :: LATTICES:18 for L being 1_Lattice for a being Element of L holds (Top L) "\/" a = Top L ; theorem :: LATTICES:19 for L being 1_Lattice for a being Element of L holds a [= Top L proofend; definition let L be non empty LattStr ; let x be Element of L; assume A1: L is complemented D_Lattice ; funcx ` -> Element of L means :Def21: :: LATTICES:def 21 it is_a_complement_of x; existence ex b1 being Element of L st b1 is_a_complement_of x by A1, Def19; uniqueness for b1, b2 being Element of L st b1 is_a_complement_of x & b2 is_a_complement_of x holds b1 = b2 proofend; end; :: deftheorem Def21 defines ` LATTICES:def_21_:_ for L being non empty LattStr for x being Element of L st L is complemented D_Lattice holds for b3 being Element of L holds ( b3 = x ` iff b3 is_a_complement_of x ); theorem Th20: :: LATTICES:20 for L being B_Lattice for a being Element of L holds (a `) "/\" a = Bottom L proofend; theorem Th21: :: LATTICES:21 for L being B_Lattice for a being Element of L holds (a `) "\/" a = Top L proofend; registration let L be B_Lattice; let a be Element of L; reduce(a `) ` to a; reducibility (a `) ` = a proofend; end; theorem :: LATTICES:22 for L being B_Lattice for a being Element of L holds (a `) ` = a ; theorem Th23: :: LATTICES:23 for L being B_Lattice for a, b being Element of L holds (a "/\" b) ` = (a `) "\/" (b `) proofend; theorem :: LATTICES:24 for L being B_Lattice for a, b being Element of L holds (a "\/" b) ` = (a `) "/\" (b `) proofend; theorem Th25: :: LATTICES:25 for L being B_Lattice for b, a being Element of L holds ( b "/\" a = Bottom L iff b [= a ` ) proofend; theorem :: LATTICES:26 for L being B_Lattice for a, b being Element of L st a [= b holds b ` [= a ` proofend; begin :: missing, 2009.07.28, A.T. definition let L be Lattice; let S be Subset of L; attrS is initial means :Def22: :: LATTICES:def 22 for p, q being Element of L st p [= q & q in S holds p in S; attrS is final means :Def23: :: LATTICES:def 23 for p, q being Element of L st p [= q & p in S holds q in S; attrS 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; attrS 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; :: deftheorem Def22 defines initial LATTICES:def_22_:_ for L being Lattice for S being Subset of L holds ( S is initial iff for p, q being Element of L st p [= q & q in S holds p in S ); :: deftheorem Def23 defines final LATTICES:def_23_:_ for L being Lattice for S being Subset of L holds ( S is final iff for p, q being Element of L st p [= q & p in S holds q in S ); :: deftheorem defines meet-closed LATTICES:def_24_:_ for L being Lattice for S being Subset of L holds ( S is meet-closed iff for p, q being Element of L st p in S & q in S holds p "/\" q in S ); :: deftheorem defines join-closed LATTICES:def_25_:_ for L being Lattice for S being Subset of L holds ( S is join-closed iff for p, q being Element of L st p in S & q in S holds p "\/" q in S ); registration let L be Lattice; cluster [#] L -> non empty initial final ; coherence ( [#] L is initial & [#] L is final & not [#] L is empty ) proofend; end; registration let L be Lattice; cluster non empty initial final for M2( bool the carrier of L); existence ex b1 being Subset of L st ( b1 is initial & b1 is final & not b1 is empty ) proofend; cluster empty -> initial final for M2( bool the carrier of L); coherence for b1 being Subset of L st b1 is empty holds ( b1 is initial & b1 is final ) proofend; cluster initial -> meet-closed for M2( bool the carrier of L); coherence for b1 being Subset of L st b1 is initial holds b1 is meet-closed proofend; cluster final -> join-closed for M2( bool the carrier of L); coherence for b1 being Subset of L st b1 is final holds b1 is join-closed proofend; end; theorem :: LATTICES:27 for L being Lattice for S being non empty initial final Subset of L holds S = [#] L proofend;