The abstract of the Mizar article:

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;