Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

### Representation Theorem for Finite Distributive Lattices

by
Marek Dudzicz

Received January 6, 2000

MML identifier: LATTICE7
[ Mizar article, MML identifier index ]

```environ

vocabulary WAYBEL_0, ORDERS_1, LATTICES, FINSET_1, TREES_1, CARD_1, BOOLE,
RELAT_2, LATTICE3, SQUARE_1, ORDINAL2, YELLOW_0, PRE_TOPC, YELLOW_1,
CAT_1, FUNCT_1, PBOOLE, RELAT_1, WELLORD1, COHSP_1, LATTICE7;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
FUNCT_2, PRE_TOPC, ORDERS_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2,
YELLOW_4, WAYBEL_1, GROUP_1, WAYBEL_0, CARD_1, XREAL_0, NAT_1, RELAT_2,
PBOOLE, COHSP_1;
constructors YELLOW_4, ORDERS_3, WAYBEL_1, YELLOW_3, GROUP_6, NAT_1, COHSP_1,
MEMBERED, PRE_TOPC;
clusters STRUCT_0, LATTICE3, YELLOW_0, ORDERS_1, YELLOW_1, WAYBEL_2, WAYBEL11,
YELLOW11, YELLOW13, SUBSET_1, RELSET_1, ARYTM_3, MEMBERED;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;

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;

definition
let L be LATTICE;
cluster non empty 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 Nat;

definition
let L be finite LATTICE;
let x be Element of L;
func height(x) -> 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 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

definition
cluster distributive finite 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 map 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 means
:: LATTICE7:def 8
it includes_lattice_of it;
end;

definition
cluster non empty Ring_of_sets;
end;

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

```