:: On the Characterization of Modular and Distributive Lattices :: by Adam Naumowicz :: :: Received April 3, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users begin :: Preliminaries theorem :: YELLOW11:1 3 = {0,1,2} by CARD_1:51; theorem Th2: :: YELLOW11:2 2 \ 1 = {1} proofend; theorem Th3: :: YELLOW11:3 3 \ 1 = {1,2} proofend; theorem Th4: :: YELLOW11:4 3 \ 2 = {2} proofend; Lm1: 3 \ 2 c= 3 \ 1 proofend; begin theorem Th5: :: YELLOW11:5 for L being reflexive antisymmetric with_suprema with_infima RelStr for a, b being Element of L holds ( a "/\" b = b iff a "\/" b = a ) proofend; theorem Th6: :: YELLOW11:6 for L being LATTICE for a, b, c being Element of L holds (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c) proofend; theorem Th7: :: YELLOW11:7 for L being LATTICE for a, b, c being Element of L holds a "\/" (b "/\" c) <= (a "\/" b) "/\" (a "\/" c) proofend; theorem Th8: :: YELLOW11:8 for L being LATTICE for a, b, c being Element of L st a <= c holds a "\/" (b "/\" c) <= (a "\/" b) "/\" c proofend; definition func N_5 -> RelStr equals :: YELLOW11:def 1 InclPoset {0,(3 \ 1),2,(3 \ 2),3}; correctness coherence InclPoset {0,(3 \ 1),2,(3 \ 2),3} is RelStr ; ; end; :: deftheorem defines N_5 YELLOW11:def_1_:_ N_5 = InclPoset {0,(3 \ 1),2,(3 \ 2),3}; registration cluster N_5 -> strict reflexive transitive antisymmetric ; correctness coherence ( N_5 is strict & N_5 is reflexive & N_5 is transitive & N_5 is antisymmetric ); ; cluster N_5 -> with_suprema with_infima ; correctness coherence ( N_5 is with_infima & N_5 is with_suprema ); proofend; end; definition func M_3 -> RelStr equals :: YELLOW11:def 2 InclPoset {0,1,(2 \ 1),(3 \ 2),3}; correctness coherence InclPoset {0,1,(2 \ 1),(3 \ 2),3} is RelStr ; ; end; :: deftheorem defines M_3 YELLOW11:def_2_:_ M_3 = InclPoset {0,1,(2 \ 1),(3 \ 2),3}; registration cluster M_3 -> strict reflexive transitive antisymmetric ; correctness coherence ( M_3 is strict & M_3 is reflexive & M_3 is transitive & M_3 is antisymmetric ); ; cluster M_3 -> with_suprema with_infima ; correctness coherence ( M_3 is with_infima & M_3 is with_suprema ); proofend; end; theorem Th9: :: YELLOW11:9 for L being LATTICE holds ( ex K being full Sublattice of L st N_5 ,K are_isomorphic iff ex a, b, c, d, e being Element of L st ( a <> b & a <> c & a <> d & a <> e & b <> c & b <> d & b <> e & c <> d & c <> e & d <> e & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) ) proofend; theorem Th10: :: YELLOW11:10 for L being LATTICE holds ( ex K being full Sublattice of L st M_3 ,K are_isomorphic iff ex a, b, c, d, e being Element of L st ( a <> b & a <> c & a <> d & a <> e & b <> c & b <> d & b <> e & c <> d & c <> e & d <> e & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) ) proofend; begin definition let L be non empty RelStr ; attrL is modular means :Def3: :: YELLOW11:def 3 for a, b, c being Element of L st a <= c holds a "\/" (b "/\" c) = (a "\/" b) "/\" c; end; :: deftheorem Def3 defines modular YELLOW11:def_3_:_ for L being non empty RelStr holds ( L is modular iff for a, b, c being Element of L st a <= c holds a "\/" (b "/\" c) = (a "\/" b) "/\" c ); registration cluster non empty reflexive antisymmetric with_infima distributive -> non empty reflexive antisymmetric with_infima modular for RelStr ; coherence for b1 being non empty reflexive antisymmetric with_infima RelStr st b1 is distributive holds b1 is modular proofend; end; Lm2: for L being LATTICE holds ( L is modular iff for a, b, c, d, e being Element of L holds ( not a <> b or not a <> c or not a <> d or not a <> e or not b <> c or not b <> d or not b <> e or not c <> d or not c <> e or not d <> e or not a "/\" b = a or not a "/\" c = a or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) ) proofend; theorem :: YELLOW11:11 for L being LATTICE holds ( L is modular iff for K being full Sublattice of L holds not N_5 ,K are_isomorphic ) proofend; Lm3: for L being LATTICE st L is modular holds ( L is distributive iff for a, b, c, d, e being Element of L holds ( not a <> b or not a <> c or not a <> d or not a <> e or not b <> c or not b <> d or not b <> e or not c <> d or not c <> e or not d <> e or not a "/\" b = a or not a "/\" c = a or not a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) ) proofend; theorem :: YELLOW11:12 for L being LATTICE st L is modular holds ( L is distributive iff for K being full Sublattice of L holds not M_3 ,K are_isomorphic ) proofend; begin definition let L be non empty RelStr ; let a, b be Element of L; func[#a,b#] -> Subset of L means :Def4: :: YELLOW11:def 4 for c being Element of L holds ( c in it iff ( a <= c & c <= b ) ); existence ex b1 being Subset of L st for c being Element of L holds ( c in b1 iff ( a <= c & c <= b ) ) proofend; uniqueness for b1, b2 being Subset of L st ( for c being Element of L holds ( c in b1 iff ( a <= c & c <= b ) ) ) & ( for c being Element of L holds ( c in b2 iff ( a <= c & c <= b ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines [# YELLOW11:def_4_:_ for L being non empty RelStr for a, b being Element of L for b4 being Subset of L holds ( b4 = [#a,b#] iff for c being Element of L holds ( c in b4 iff ( a <= c & c <= b ) ) ); definition let L be non empty RelStr ; let IT be Subset of L; attrIT is interval means :Def5: :: YELLOW11:def 5 ex a, b being Element of L st IT = [#a,b#]; end; :: deftheorem Def5 defines interval YELLOW11:def_5_:_ for L being non empty RelStr for IT being Subset of L holds ( IT is interval iff ex a, b being Element of L st IT = [#a,b#] ); registration let L be non empty reflexive transitive RelStr ; cluster non empty interval -> directed for Element of K32( the carrier of L); coherence for b1 being Subset of L st not b1 is empty & b1 is interval holds b1 is directed proofend; cluster non empty interval -> filtered for Element of K32( the carrier of L); coherence for b1 being Subset of L st not b1 is empty & b1 is interval holds b1 is filtered proofend; end; registration let L be non empty RelStr ; let a, b be Element of L; cluster[#a,b#] -> interval ; coherence [#a,b#] is interval by Def5; end; theorem :: YELLOW11:13 for L being non empty reflexive transitive RelStr for a, b being Element of L holds [#a,b#] = (uparrow a) /\ (downarrow b) proofend; registration let L be with_infima Poset; let a, b be Element of L; cluster subrelstr [#a,b#] -> meet-inheriting ; coherence subrelstr [#a,b#] is meet-inheriting proofend; end; registration let L be with_suprema Poset; let a, b be Element of L; cluster subrelstr [#a,b#] -> join-inheriting ; coherence subrelstr [#a,b#] is join-inheriting proofend; end; theorem :: YELLOW11:14 for L being LATTICE for a, b being Element of L st L is modular holds subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic proofend; registration cluster non empty finite V58() reflexive transitive antisymmetric with_suprema with_infima for RelStr ; existence ex b1 being LATTICE st ( b1 is finite & not b1 is empty ) proofend; end; registration cluster finite reflexive transitive antisymmetric with_infima -> lower-bounded for RelStr ; coherence for b1 being Semilattice st b1 is finite holds b1 is lower-bounded proofend; end; registration cluster finite reflexive transitive antisymmetric with_suprema with_infima -> complete for RelStr ; coherence for b1 being LATTICE st b1 is finite holds b1 is complete proofend; end;