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;