Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

### On the Characterization of Modular and Distributive Lattices

by

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;
```