Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### On the Characterization of Modular and Distributive Lattices

**by****Adam Naumowicz**- Received April 3, 1998
- MML identifier: YELLOW11

- [ Mizar article, MML identifier index ]

environ vocabulary ORDINAL1, BOOLE, RELAT_2, LATTICE3, ORDERS_1, LATTICES, WAYBEL_0, YELLOW_1, CAT_1, FILTER_2, WELLORD1, PRE_TOPC, YELLOW_0, FUNCT_1, SEQM_3, RELAT_1, ORDINAL2, MEASURE5, QUANTAL1, FINSET_1, BHSP_3, YELLOW11; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, STRUCT_0, ORDERS_1, LATTICE3, ORDERS_3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_1, LATTICE5, FINSET_1, GROUP_1, WAYBEL_0, ORDINAL1; constructors LATTICE3, GROUP_1, ORDERS_3, WAYBEL_1, ENUMSET1; clusters STRUCT_0, LATTICE3, YELLOW_0, ORDERS_1, FINSET_1, YELLOW_1, RELSET_1, XBOOLE_0; requirements NUMERALS, REAL, SUBSET, BOOLE; begin reserve x for set; :: Preliminaries theorem :: YELLOW11:1 3 = {0,1,2}; theorem :: YELLOW11:2 2\1={1}; theorem :: YELLOW11:3 3\1 = {1,2}; theorem :: YELLOW11:4 3\2 = {2}; begin:: Main part theorem :: YELLOW11:5 for L being antisymmetric reflexive with_infima with_suprema RelStr for a,b being Element of L holds a"/\"b = b iff a"\/"b = a; theorem :: YELLOW11:6 for L being LATTICE for a,b,c being Element of L holds (a"/\"b)"\/"(a"/\"c) <= a"/\"(b"\/"c); theorem :: YELLOW11:7 for L being LATTICE for a,b,c being Element of L holds a"\/"(b"/\"c) <= (a"\/"b)"/\"(a"\/"c); theorem :: YELLOW11:8 for L being LATTICE for a,b,c being Element of L holds a <= c implies a"\/"(b"/\"c) <= (a"\/"b) "/\"c; definition func N_5 -> RelStr equals :: YELLOW11:def 1 InclPoset {0, 3 \ 1, 2, 3 \ 2, 3}; end; definition cluster N_5 -> strict reflexive transitive antisymmetric; cluster N_5 -> with_infima with_suprema; end; definition func M_3 -> RelStr equals :: YELLOW11:def 2 InclPoset{ 0, 1, 2 \ 1, 3 \ 2, 3 }; end; definition cluster M_3 -> strict reflexive transitive antisymmetric; cluster M_3 -> with_infima with_suprema; end; theorem :: 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)); theorem :: 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); begin:: Modular lattices definition let L be non empty RelStr; attr L is modular means :: YELLOW11:def 3 for a,b,c being Element of L st a <= c holds a"\/"(b"/\"c) = (a"\/"b)"/\"c; end; definition cluster distributive -> modular (non empty antisymmetric reflexive with_infima RelStr); end; theorem :: YELLOW11:11 for L being LATTICE holds L is modular iff not ex K being full Sublattice of L st N_5,K are_isomorphic; theorem :: YELLOW11:12 for L being LATTICE st L is modular holds L is distributive iff not ex K being full Sublattice of L st M_3,K are_isomorphic; begin:: Intervals of a lattice definition let L be non empty RelStr; let a,b be Element of L; func [#a,b#] -> Subset of L means :: YELLOW11:def 4 for c being Element of L holds c in it iff a <= c & c <= b; end; definition let L be non empty RelStr; let IT be Subset of L; attr IT is interval means :: YELLOW11:def 5 ex a,b being Element of L st IT = [#a,b#]; end; definition let L be non empty reflexive transitive RelStr; cluster non empty interval -> directed (Subset of L); cluster non empty interval -> filtered (Subset of L); end; definition let L be non empty RelStr; let a,b be Element of L; cluster [#a,b#] -> interval; end; theorem :: YELLOW11:13 for L being non empty reflexive transitive RelStr, a,b being Element of L holds [#a,b#] = uparrow a /\ downarrow b; definition let L be with_infima Poset; let a,b be Element of L; cluster subrelstr[#a,b#] -> meet-inheriting; end; definition let L be with_suprema Poset; let a,b be Element of L; cluster subrelstr[#a,b#] -> join-inheriting; end; theorem :: YELLOW11:14 for L being LATTICE, a,b being Element of L holds L is modular implies subrelstr[#b,a"\/"b#],subrelstr[#a"/\" b,a#] are_isomorphic; definition cluster finite non empty LATTICE; end; definition cluster finite -> lower-bounded Semilattice; end; definition cluster finite -> complete LATTICE; end;

Back to top