:: On the Characterization of Modular and Distributive Lattices
:: by Adam Naumowicz
::
:: Received April 3, 1998
:: Copyright (c) 1998-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, CARD_1, XBOOLE_0, TARSKI, RELAT_2, LATTICE3, ORDERS_2,
SUBSET_1, LATTICES, EQREL_1, XXREAL_0, WAYBEL_0, YELLOW_1, STRUCT_0,
CAT_1, LATTICE5, WELLORD1, FUNCT_1, SEQM_3, YELLOW_0, RELAT_1, ORDINAL2,
MEASURE5, FINSET_1, ORDERS_1, REWRITE1, YELLOW11, ZFMISC_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, SUBSET_1, FUNCT_1, RELSET_1,
FUNCT_2, ORDINAL1, CARD_1, NUMBERS, ORDERS_1, DOMAIN_1, FINSET_1,
STRUCT_0, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_1,
LATTICE5, WAYBEL_0;
constructors DOMAIN_1, XXREAL_0, LATTICE3, ORDERS_3, WAYBEL_1, RELSET_1,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, ORDERS_2, LATTICE3,
YELLOW_0, YELLOW_1, ORDINAL1;
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;
registration
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;
registration
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,c,d,e are_mutually_distinct &
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,c,d,e are_mutually_distinct &
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;
registration
cluster distributive -> modular for 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;
registration
let L be non empty reflexive transitive RelStr;
cluster non empty interval -> directed for (Subset of L);
cluster non empty interval -> filtered for (Subset of L);
end;
registration
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;
registration
let L be with_infima Poset;
let a,b be Element of L;
cluster subrelstr[#a,b#] -> meet-inheriting;
end;
registration
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;
registration
cluster finite non empty for LATTICE;
end;
registration
cluster finite -> lower-bounded for Semilattice;
end;
registration
cluster finite -> complete for LATTICE;
end;