:: Representation Theorem For Finite Distributive Lattices
:: by Marek Dudzicz
::
:: Received January 6, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users


definition
let L be 1-sorted ;
let A, B be Subset of L;
:: original: c=
redefine pred A c= B means :: LATTICE7:def 1
 for x being Element of L st x in A holds
x in B;
compatibility
( A c= B iff for x being Element of L st x in A holds
x in B ) ;
end;

:: deftheorem defines c= LATTICE7:def 1 :
for L being 1-sorted
for A, B being Subset of L holds
( A c= B iff for x being Element of L st x in A holds
x in B );

registration
let L be LATTICE;
cluster non empty strongly_connected for Element of bool the carrier of L;
existence
not for b1 being Chain of L holds b1 is empty
proof end;
end;

definition
let L be LATTICE;
let x, y be Element of L;
assume A1: x <= y ;
mode Chain of x,y -> non empty Chain of L means :Def2: :: LATTICE7:def 2
( x in it & y in it & ( for z being Element of L st z in it holds
( x <= z & z <= y ) ) );
existence
ex b1 being non empty Chain of L st
( x in b1 & y in b1 & ( for z being Element of L st z in b1 holds
( x <= z & z <= y ) ) )
proof end;
end;

:: deftheorem Def2 defines Chain LATTICE7:def 2 :
for L being LATTICE
for x, y being Element of L st x <= y holds
for b4 being non empty Chain of L holds
( b4 is Chain of x,y iff ( x in b4 & y in b4 & ( for z being Element of L st z in b4 holds
( x <= z & z <= y ) ) ) );

theorem Th1: :: LATTICE7:1
for L being LATTICE
for x, y being Element of L st x <= y holds
{x,y} is Chain of x,y
proof end;

definition
let L be finite LATTICE;
let x be Element of L;
func height x -> Element of NAT means :Def3: :: LATTICE7:def 3
( ex A being Chain of Bottom L,x st it = card A & ( for A being Chain of Bottom L,x holds card A <= it ) );
existence
ex b1 being Element of NAT st
( ex A being Chain of Bottom L,x st b1 = card A & ( for A being Chain of Bottom L,x holds card A <= b1 ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st ex A being Chain of Bottom L,x st b1 = card A & ( for A being Chain of Bottom L,x holds card A <= b1 ) & ex A being Chain of Bottom L,x st b2 = card A & ( for A being Chain of Bottom L,x holds card A <= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines height LATTICE7:def 3 :
for L being finite LATTICE
for x being Element of L
for b3 being Element of NAT holds
( b3 = height x iff ( ex A being Chain of Bottom L,x st b3 = card A & ( for A being Chain of Bottom L,x holds card A <= b3 ) ) );

theorem Th2: :: LATTICE7:2
for L being finite LATTICE
for a, b being Element of L st a < b holds
height a < height b
proof end;

theorem Th3: :: LATTICE7:3
for L being finite LATTICE
for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x < y iff height x < height y )
proof end;

theorem Th4: :: LATTICE7:4
for L being finite LATTICE
for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x = y iff height x = height y )
proof end;

theorem Th5: :: LATTICE7:5
for L being finite LATTICE
for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x <= y iff height x <= height y )
proof end;

theorem :: LATTICE7:6
for L being finite LATTICE
for x being Element of L holds
( height x = 1 iff x = Bottom L )
proof end;

theorem Th7: :: LATTICE7:7
for L being non empty finite LATTICE
for x being Element of L holds height x >= 1
proof end;

scheme :: LATTICE7:sch 1
LattInd{ F1() -> finite LATTICE, P1[ set ] } :
for x being Element of F1() holds P1[x]
provided
A1: for x being Element of F1() st ( for b being Element of F1() st b < x holds
P1[b] ) holds
P1[x]
proof end;

registration
cluster non empty finite V123() reflexive transitive antisymmetric distributive with_suprema with_infima for RelStr ;
existence
ex b1 being LATTICE st
( b1 is distributive & b1 is finite )
proof end;
end;

definition
let L be LATTICE;
let x, y be Element of L;
pred x <(1) y means :: LATTICE7:def 4
( x < y & ( for z being Element of L holds
( not x < z or not z < y ) ) );
end;

:: deftheorem defines <(1) LATTICE7:def 4 :
for L being LATTICE
for x, y being Element of L holds
( x <(1) y iff ( x < y & ( for z being Element of L holds
( not x < z or not z < y ) ) ) );

theorem Th8: :: LATTICE7:8
for L being finite LATTICE
for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) )
proof end;

definition
let L be finite LATTICE;
let A be non empty Chain of L;
func max A -> Element of L means :Def5: :: LATTICE7:def 5
( ( for x being Element of L st x in A holds
x <= it ) & it in A );
existence
ex b1 being Element of L st
( ( for x being Element of L st x in A holds
x <= b1 ) & b1 in A )
proof end;
uniqueness
for b1, b2 being Element of L st ( for x being Element of L st x in A holds
x <= b1 ) & b1 in A & ( for x being Element of L st x in A holds
x <= b2 ) & b2 in A holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines max LATTICE7:def 5 :
for L being finite LATTICE
for A being non empty Chain of L
for b3 being Element of L holds
( b3 = max A iff ( ( for x being Element of L st x in A holds
x <= b3 ) & b3 in A ) );

theorem Th9: :: LATTICE7:9
for L being finite LATTICE
for y being Element of L st y <> Bottom L holds
ex x being Element of L st x <(1) y
proof end;

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 being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) ) } ;
coherence
{ a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) ) } is Subset of L
proof end;
end;

:: deftheorem defines Join-IRR LATTICE7:def 6 :
for L being LATTICE holds Join-IRR L = { a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) ) } ;

theorem Th10: :: LATTICE7:10
for L being LATTICE
for x being Element of L holds
( x in Join-IRR L iff ( x <> Bottom L & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) ) )
proof end;

theorem Th11: :: LATTICE7:11
for L being finite distributive LATTICE
for x being Element of L st x in Join-IRR L holds
ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) )
proof end;

Lm1: for L being finite distributive LATTICE
for a being Element of L st ( for b being Element of L st b < a holds
sup ((downarrow b) /\ (Join-IRR L)) = b ) holds
sup ((downarrow a) /\ (Join-IRR L)) = a
proof end;

theorem Th12: :: LATTICE7:12
for L being finite distributive LATTICE
for x being Element of L holds sup ((downarrow x) /\ (Join-IRR L)) = x
proof end;

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 } ;
coherence
{ X where X is Subset of P : X is lower } is non empty set
proof end;
end;

:: deftheorem defines LOWER LATTICE7:def 7 :
for P being RelStr holds LOWER P = { X where X is Subset of P : X is lower } ;

theorem Th13: :: LATTICE7:13
for L being finite distributive LATTICE ex r being 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) ) )
proof end;

theorem Th14: :: LATTICE7:14
for L being finite distributive LATTICE holds L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic
proof end;

definition
mode Ring_of_sets -> set means :Def8: :: LATTICE7:def 8
it includes_lattice_of it;
existence
ex b1 being set st b1 includes_lattice_of b1
proof end;
end;

:: deftheorem Def8 defines Ring_of_sets LATTICE7:def 8 :
for b1 being set holds
( b1 is Ring_of_sets iff b1 includes_lattice_of b1 );

registration
cluster non empty for Ring_of_sets ;
existence
not for b1 being Ring_of_sets holds b1 is empty
proof end;
end;

Lm2: for L1, L2 being non empty RelStr
for f being Function of L1,L2 st f is infs-preserving holds
f is meet-preserving
;

Lm3: for L1, L2 being non empty RelStr
for f being Function of L1,L2 st f is sups-preserving holds
f is join-preserving
;

registration
let X be non empty Ring_of_sets ;
cluster InclPoset X -> distributive with_suprema with_infima ;
coherence
( InclPoset X is with_suprema & InclPoset X is with_infima & InclPoset X is distributive )
proof end;
end;

theorem Th15: :: LATTICE7:15
for L being finite LATTICE holds LOWER (subrelstr (Join-IRR L)) is Ring_of_sets
proof end;

theorem :: LATTICE7:16
for L being finite LATTICE holds
( L is distributive iff ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic )
proof end;