:: Representation Theorem For Finite Distributive Lattices
:: by Marek Dudzicz
::
:: Received January 6, 2000
:: Copyright (c) 2000-2017 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, STRUCT_0, SUBSET_1, TARSKI, WAYBEL_0, XBOOLE_0, TREES_2,
LATTICES, XXREAL_0, FINSET_1, TREES_1, CARD_1, NAT_1, ARYTM_3, ORDERS_2,
RELAT_2, ORDERS_1, LATTICE3, EQREL_1, ORDINAL2, YELLOW_0, FUNCT_1,
YELLOW_1, CAT_1, PBOOLE, RELAT_1, WELLORD1, COHSP_1, ZFMISC_1, LATTICE7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2,
DOMAIN_1, CARD_1, ORDINAL1, NUMBERS, STRUCT_0, ORDERS_1, PBOOLE,
XCMPLX_0, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_4, WAYBEL_1,
WAYBEL_0, NAT_1, RELAT_2, COHSP_1, XXREAL_0;
constructors DOMAIN_1, NAT_1, MEMBERED, COHSP_1, WAYBEL_1, YELLOW_4, RELSET_1,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0,
YELLOW_1, WAYBEL_2, WAYBEL11, YELLOW11, XXREAL_0, RELSET_1, ORDINAL1,
XCMPLX_0, NAT_1;
requirements NUMERALS, REAL, SUBSET, BOOLE;
begin :: Induction in a finite lattice
definition
let L be 1-sorted;
let A,B be Subset of L;
redefine pred A c= B means
:: LATTICE7:def 1
for x be Element of L st x in A holds x in B;
end;
registration
let L be LATTICE;
cluster non empty for Chain of L;
end;
definition
let L be LATTICE;
let x,y be Element of L such that
x <= y;
mode Chain of x,y -> non empty Chain of L means
:: LATTICE7:def 2
x in it & y in it & for z be Element of L st z in it holds x <= z & z <= y;
end;
theorem :: LATTICE7:1
for L be LATTICE for x,y be Element of L holds x <= y implies {x,
y} is Chain of x,y;
reserve n,k for Element of NAT;
definition
let L be finite LATTICE;
let x be Element of L;
func height(x) -> Element of NAT means
:: LATTICE7:def 3
(ex A be Chain of Bottom L,x
st it= card A) & for A be Chain of Bottom L,x holds card A <= it;
end;
theorem :: LATTICE7:2
for L be finite LATTICE for a,b be Element of L holds a < b
implies height(a) < height(b);
theorem :: LATTICE7:3
for L be finite LATTICE for C be Chain of L for x,y be Element of
L holds x in C & y in C implies ( x < y iff height(x) < height(y) );
theorem :: LATTICE7:4
for L be finite LATTICE for C be Chain of L for x,y be Element of
L holds x in C & y in C implies ( x = y iff height(x) = height(y) );
theorem :: LATTICE7:5
for L be finite LATTICE for C be Chain of L for x,y be Element of
L holds x in C & y in C implies ( x <= y iff height(x) <= height(y) );
theorem :: LATTICE7:6
for L be finite LATTICE for x be Element of L holds height (x) = 1 iff
x = Bottom L;
theorem :: LATTICE7:7
for L be non empty finite LATTICE for x be Element of L holds height (x) >= 1
;
scheme :: LATTICE7:sch 1
LattInd { L() -> finite LATTICE, P[set]}: for x be Element of L() holds P[x]
provided
for x be Element of L() st for b be Element of L() st b < x holds P[
b] holds P[x];
begin :: Join irreducible elements in a finite distributive lattice
registration
cluster distributive finite for LATTICE;
end;
definition
let L be LATTICE;
let x,y be Element of L;
pred x <(1) y means
:: LATTICE7:def 4
x < y & not (ex z be Element of L st x < z & z < y);
end;
theorem :: LATTICE7:8
for L be finite LATTICE for X be non empty Subset of L holds ex x
be Element of L st x in X & for y be Element of L st y in X holds not x < y;
definition
let L be finite LATTICE;
let A be non empty Chain of L;
func max(A) -> Element of L means
:: LATTICE7:def 5
(for x be Element of L st x in A holds x <= it) & it in A;
end;
theorem :: LATTICE7:9
for L be finite LATTICE for y be Element of L st y <> Bottom L
holds ex x be Element of L st x <(1) y;
definition
let L be LATTICE;
func Join-IRR L -> Subset of L equals
:: LATTICE7:def 6
{a where a is Element of L: a<>Bottom
L & for b,c be Element of L holds a= b"\/"c implies a=b or a=c};
end;
theorem :: LATTICE7:10
for L be LATTICE for x be Element of L holds x in Join-IRR L iff
x<>Bottom L & for b,c be Element of L holds x= b"\/"c implies x=b or x=c;
theorem :: LATTICE7:11
for L be finite distributive LATTICE for x be Element of L holds
x in Join-IRR L implies ex z be Element of L st z < x & for y be Element of L
st y < x holds y <= z;
theorem :: LATTICE7:12
for L be distributive finite LATTICE for x be Element of L holds
sup (downarrow x /\ Join-IRR L) = x;
begin :: Representation theorem
definition
let P be RelStr;
func LOWER(P) -> non empty set equals
:: LATTICE7:def 7
{X where X is Subset of P:X is lower};
end;
theorem :: LATTICE7:13
for L be distributive finite LATTICE ex r be Function of L,
InclPoset LOWER(subrelstr Join-IRR L) st r is isomorphic & for a being Element
of L holds r.a= downarrow a /\ Join-IRR L;
theorem :: LATTICE7:14
for L be distributive finite LATTICE holds L, InclPoset LOWER(
subrelstr Join-IRR L) are_isomorphic;
definition
mode Ring_of_sets -> set means
:: LATTICE7:def 8
it includes_lattice_of it;
end;
registration
cluster non empty for Ring_of_sets;
end;
registration
let X be non empty Ring_of_sets;
cluster InclPoset X -> with_suprema with_infima distributive;
end;
theorem :: LATTICE7:15
for L be finite LATTICE holds LOWER(subrelstr Join-IRR L) is Ring_of_sets;
theorem :: LATTICE7:16
for L be finite LATTICE holds L is distributive iff ex X be non empty
Ring_of_sets st L, InclPoset X are_isomorphic;