:: Representation Theorem For Finite Distributive Lattices :: by Marek Dudzicz :: :: Received January 6, 2000 :: Copyright (c) 2000-2019 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;