:: Representation Theorem For Finite Distributive Lattices :: by Marek Dudzicz :: :: Received January 6, 2000 :: Copyright (c) 2000-2012 Association of Mizar Users begin definition let L be 1-sorted ; let A, B be Subset of L; :: original:c= redefine predA 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 ) proofend; 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 proofend; end; definition let L be LATTICE; let x, y be Element of L; assume B1: 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 ) ) ) proofend; 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 proofend; 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 ) ) proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; theorem :: LATTICE7:6 for L being finite LATTICE for x being Element of L holds ( height x = 1 iff x = Bottom L ) proofend; theorem Th7: :: LATTICE7:7 for L being non empty finite LATTICE for x being Element of L holds height x >= 1 proofend; 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] proofend; begin registration cluster non empty finite V117() reflexive transitive antisymmetric distributive with_suprema with_infima for RelStr ; existence ex b1 being LATTICE st ( b1 is distributive & b1 is finite ) proofend; end; definition let L be LATTICE; let x, y be Element of L; predx <(1) y means :Def4: :: LATTICE7:def 4 ( x < y & ( for z being Element of L holds ( not x < z or not z < y ) ) ); end; :: deftheorem Def4 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 ) ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) ) ) ) proofend; 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 ) ) proofend; 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 proofend; theorem Th12: :: LATTICE7:12 for L being finite distributive LATTICE for x being Element of L holds sup ((downarrow x) /\ (Join-IRR L)) = x proofend; begin 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 proofend; 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) ) ) proofend; theorem Th14: :: LATTICE7:14 for L being finite distributive LATTICE holds L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; end; theorem Th15: :: LATTICE7:15 for L being finite LATTICE holds LOWER (subrelstr (Join-IRR L)) is Ring_of_sets proofend; 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 ) proofend;