:: Representation Theorem For Finite Distributive Lattices
:: by Marek Dudzicz
::
:: Received January 6, 2000
:: Copyright (c) 2000-2026 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;
requirements NUMERALS, REAL, SUBSET, BOOLE;
definitions TARSKI, WAYBEL_0, WAYBEL_1, LATTICE3, RELAT_2, COHSP_1;
equalities WAYBEL_0;
expansions TARSKI, WAYBEL_0, WAYBEL_1, LATTICE3, COHSP_1;
theorems WAYBEL_0, WAYBEL_1, WAYBEL_2, YELLOW_0, YELLOW_1, YELLOW_4, TARSKI,
FUNCT_1, FUNCT_2, ORDERS_2, WAYBEL_4, CARD_1, CARD_2, NAT_1, YELLOW_5,
WAYBEL13, WAYBEL_6, RELSET_1, XBOOLE_0, XBOOLE_1, XXREAL_0, ORDINAL1,
PARTFUN1;
schemes NAT_1, PBOOLE;
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 :: redefines c= (TARSKI, definition)
for x be Element of L st x in A holds x in B;
compatibility;
end;
registration
let L be LATTICE;
cluster non empty for Chain of L;
existence
proof
{Bottom L} is Chain of L by ORDERS_2:8;
hence thesis;
end;
end;
definition
let L be LATTICE;
let x,y be Element of L such that
A1: x <= y;
mode Chain of x,y -> non empty Chain of L means
:Def2:
x in it & y in it & for z be Element of L st z in it holds x <= z & z <= y;
existence
proof
reconsider A={x,y} as non empty Chain of L by A1,ORDERS_2:9;
A2: for z be Element of L st z in A holds x <= z & z <= y
proof
let z be Element of L;
assume
A3: z in A;
per cases by A3,TARSKI:def 2;
suppose
z=x;
hence thesis by A1;
end;
suppose
z=y;
hence thesis by A1;
end;
end;
y in A & x in A by TARSKI:def 2;
hence thesis by A2;
end;
end;
theorem Th1:
for L be LATTICE for x,y be Element of L holds x <= y implies {x,
y} is Chain of x,y
proof
let L be LATTICE;
let x,y be Element of L;
A1: x in {x,y} & y in {x,y} by TARSKI:def 2;
assume
A2: x <= y;
A3: for z be Element of L st z in {x,y} holds x <= z & z <= y
proof
let z be Element of L;
assume
A4: z in {x,y};
per cases by A4,TARSKI:def 2;
suppose
z=x;
hence thesis by A2;
end;
suppose
z=y;
hence thesis by A2;
end;
end;
{x,y} is Chain of L by A2,ORDERS_2:9;
hence thesis by A2,A1,A3,Def2;
end;
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
:Def3:
(ex A be Chain of Bottom L,x
st it= card A) & for A be Chain of Bottom L,x holds card A <= it;
existence
proof
defpred P[Nat] means ex A be Chain of Bottom L,x st $1=card A;
A1: {Bottom L,x} is Chain of Bottom L,x by Th1,YELLOW_0:44;
ex k st P[k] & for n st P[n] holds n <= k
proof
P[card{Bottom L,x}] by A1;
then
A2: ex k be Nat st P[k];
A3: for k be Nat st P[k] holds k <= card the carrier of L by NAT_1:43;
consider k being Nat such that
A4: P[k] & for n being Nat st P[n] holds n <= k from NAT_1:sch 6 (A3
,A2);
reconsider k as Element of NAT by ORDINAL1:def 12;
take k;
thus thesis by A4;
end;
then consider k such that
A5: ( P[k])& for n st P[n] holds n <= k;
take k;
thus thesis by A5;
end;
uniqueness
proof
let a,b be Element of NAT;
assume ( ex A be Chain of Bottom L,x st a= card A)&( ( for A be Chain of
Bottom L,x holds card A <= a)& ex B be Chain of Bottom L,x st b= card B ) & for
A be Chain of Bottom L,x holds card A <= b;
then a<=b & b<=a;
hence thesis by XXREAL_0:1;
end;
end;
theorem Th2:
for L be finite LATTICE for a,b be Element of L holds a < b
implies height(a) < height(b)
proof
let L be finite LATTICE;
let a,b be Element of L;
( ex A be Chain of Bottom L,a st height(a) = card A)& for C be Chain of
Bottom L,a holds card C <= height(a) by Def3;
then consider A be Chain of Bottom L,a such that
A1: height(a) = card A and
for C be Chain of Bottom L,a holds card C <= height(a);
set C=A \/ {b};
b in {b} by TARSKI:def 1;
then
A2: b in C by XBOOLE_0:def 3;
A3: Bottom L<=a by YELLOW_0:44;
then Bottom L in A by Def2;
then
A4: Bottom L in C by XBOOLE_0:def 3;
assume
A5: a < b;
not b in A
proof
assume b in A;
then b <= a by A3,Def2;
hence contradiction by A5,ORDERS_2:6;
end;
then
A6: card C = (card A)+1 by CARD_2:41;
the InternalRel of L is_strongly_connected_in C
proof
let x,y be object;
x in C & y in C implies [x,y] in the InternalRel of L or [y,x] in the
InternalRel of L
proof
assume
A7: x in C & y in C;
per cases by A7,XBOOLE_0:def 3;
suppose
A8: x in A & y in A;
then reconsider x,y as Element of L;
x <= y or y <= x by A8,ORDERS_2:11;
hence thesis by ORDERS_2:def 5;
end;
suppose
A9: x in A & y in {b};
then reconsider x as Element of L;
Bottom L<=a by YELLOW_0:44;
then x <= a by A9,Def2;
then x < b by A5,ORDERS_2:7;
then
A10: x <= b by ORDERS_2:def 6;
y=b by A9,TARSKI:def 1;
hence thesis by A10,ORDERS_2:def 5;
end;
suppose
A11: x in {b} & y in A;
then reconsider y as Element of L;
Bottom L<=a by YELLOW_0:44;
then y <= a by A11,Def2;
then y < b by A5,ORDERS_2:7;
then
A12: y <= b by ORDERS_2:def 6;
x=b by A11,TARSKI:def 1;
hence thesis by A12,ORDERS_2:def 5;
end;
suppose
A13: x in {b} & y in {b};
then reconsider x,y as Element of L;
x=b by A13,TARSKI:def 1;
then x <= y by A13,TARSKI:def 1;
hence thesis by ORDERS_2:def 5;
end;
end;
hence thesis;
end;
then
A14: C is strongly_connected Subset of L by ORDERS_2:def 7;
A15: for z be Element of L st z in C holds Bottom L <= z & z <= b
proof
let z be Element of L;
assume
A16: z in C;
per cases by A16,XBOOLE_0:def 3;
suppose
A17: z in A;
thus Bottom L<=z by YELLOW_0:44;
z<=a by A3,A17,Def2;
then z<b by A5,ORDERS_2:7;
hence thesis by ORDERS_2:def 6;
end;
suppose
z in {b};
hence thesis by TARSKI:def 1,YELLOW_0:44;
end;
end;
Bottom L <= b by YELLOW_0:44;
then C is Chain of Bottom L,b by A4,A2,A15,A14,Def2;
then height(a) + 1 <= height(b) by A1,A6,Def3;
hence thesis by NAT_1:13;
end;
theorem Th3:
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) )
proof
let L be finite LATTICE;
let C be Chain of L;
let x,y be Element of L;
assume
A1: x in C & y in C;
height(x) < height(y) implies x < y
proof
assume
A2: height(x) < height(y);
per cases by A1,ORDERS_2:11;
suppose
x <= y;
hence thesis by A2,ORDERS_2:def 6;
end;
suppose
y <= x;
then x=y or y < x by ORDERS_2:def 6;
hence thesis by A2,Th2;
end;
end;
hence x < y iff height(x) < height(y) by Th2;
end;
theorem Th4:
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) )
proof
let L be finite LATTICE;
let C be Chain of L;
let x,y be Element of L;
assume
A1: x in C & y in C;
thus x = y implies height(x) = height(y);
height(x) = height(y) implies x=y
proof
assume that
A2: height(x) = height(y) and
A3: x<>y;
A4: x<=y or y<=x by A1,ORDERS_2:11;
height(x)<>height(y)
proof
per cases by A3,A4,ORDERS_2:def 6;
suppose
x < y;
hence thesis by A1,Th3;
end;
suppose
y < x;
hence thesis by A1,Th3;
end;
end;
hence contradiction by A2;
end;
hence thesis;
end;
theorem Th5:
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) )
proof
let L be finite LATTICE;
let C be Chain of L;
let x,y be Element of L;
assume
A1: x in C & y in C;
A2: height(x) <= height(y) implies x<=y
proof
assume height(x) <= height(y);
then height(x) < height(y) or height(x) = height(y) by XXREAL_0:1;
then x<y or height(x) = height(y) by A1,Th3;
hence thesis by A1,Th4,ORDERS_2:def 6;
end;
x <= y implies height(x) <= height(y)
proof
assume x<=y;
then x<y or x=y by ORDERS_2:def 6;
hence thesis by A1,Th3;
end;
hence x <= y iff height(x) <= height(y) by A2;
end;
theorem
for L be finite LATTICE for x be Element of L holds height (x) = 1 iff
x = Bottom L
proof
let L be finite LATTICE;
let x be Element of L;
A1: x = Bottom L implies height (x) = 1
proof
A2: for B be Chain of Bottom L,Bottom L holds B = {Bottom L}
proof
let B be Chain of Bottom L,Bottom L;
A3: B c= {Bottom L}
proof
let r be set;
r in B implies r in {Bottom L}
proof
assume r in B;
then reconsider r as Element of B;
Bottom L <= r & r <= Bottom L by Def2;
then Bottom L = r by ORDERS_2:2;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
{Bottom L} c= B
proof
let r be set;
r in {Bottom L} implies r in B
proof
assume r in {Bottom L};
then r = Bottom L by TARSKI:def 1;
hence thesis by Def2;
end;
hence thesis;
end;
hence thesis by A3,XBOOLE_0:def 10;
end;
assume
A4: x = Bottom L;
( ex A be Chain of Bottom L,Bottom L st height(Bottom L)= card A)&
card { Bottom L} = 1 by Def3,CARD_1:30;
hence thesis by A4,A2;
end;
height (x) = 1 implies x = Bottom L
proof
A5: for z be Element of L st z in {Bottom L,x} holds Bottom L <= z & z <= x
proof
let z be Element of L;
assume
A6: z in {Bottom L,x};
per cases by A6,TARSKI:def 2;
suppose
z=Bottom L;
hence thesis by YELLOW_0:44;
end;
suppose
z=x;
hence thesis by YELLOW_0:44;
end;
end;
A7: x in {Bottom L,x} & Bottom L in {Bottom L,x} by TARSKI:def 2;
A8: Bottom L<=x by YELLOW_0:44;
then {Bottom L,x} is Chain of L by ORDERS_2:9;
then
A9: {Bottom L,x} is Chain of Bottom L,x by A8,A7,A5,Def2;
assume that
A10: height (x) = 1 and
A11: x <> Bottom L;
card {Bottom L,x} = 2 by A11,CARD_2:57;
hence contradiction by A10,A9,Def3;
end;
hence thesis by A1;
end;
theorem Th7:
for L be non empty finite LATTICE for x be Element of L holds height (x) >= 1
proof
let L be non empty finite LATTICE;
let x be Element of L;
A1: {Bottom L,x} is Chain of Bottom L,x by Th1,YELLOW_0:44;
then
A2: card {Bottom L,x} <= height (x) by Def3;
per cases;
suppose
x<>Bottom L;
then card {Bottom L,x} = 2 by CARD_2:57;
hence thesis by A2,XXREAL_0:2;
end;
suppose
A3: x=Bottom L;
A4: {Bottom L}c={Bottom L,Bottom L}
proof
let d be Element of L;
assume d in{Bottom L};
then d =Bottom L by TARSKI:def 1;
hence thesis by TARSKI:def 2;
end;
{Bottom L,Bottom L}c={Bottom L}
proof
let d be Element of L;
assume d in {Bottom L,Bottom L};
then d =Bottom L or d =Bottom L by TARSKI:def 2;
hence thesis by TARSKI:def 1;
end;
then
A5: {Bottom L,Bottom L}={Bottom L} by A4,XBOOLE_0:def 10;
card {Bottom L,Bottom L} <= height (Bottom L) by A1,A3,Def3;
hence thesis by A3,A5,CARD_1:30;
end;
end;
scheme
LattInd { L() -> finite LATTICE, P[set]}: for x be Element of L() holds P[x]
provided
A1: for x be Element of L() st for b be Element of L() st b < x holds P[
b] holds P[x]
proof
defpred Q[Nat] means for x be Element of L() st height(x) <= $1
holds P[x];
A2: for n be Nat st Q[n] holds Q[n+1]
proof
let n be Nat;
assume
A3: Q[n];
for x be Element of L() st height(x) <= n+1 holds P[x]
proof
let x be Element of L();
assume
A4: height(x) <= n+1;
per cases by A3,A4,NAT_1:8;
suppose
A5: height(x) = n+1;
for y be Element of L() st y < x holds P[y]
proof
let y be Element of L();
assume y < x;
then height(y) < height(x) by Th2;
then height(y) <= n by A5,NAT_1:13;
hence thesis by A3;
end;
hence thesis by A1;
end;
suppose
P[x];
hence thesis;
end;
end;
hence thesis;
end;
let x be Element of L();
A6: ( for x be Element of L() st height(x) <= height(x) holds P[x] )
implies for x be Element of L() holds P[x]
proof
assume that
A7: for x be Element of L() st height(x) <= height(x) holds P[x] and
A8: not(for x be Element of L() holds P[x]);
consider x be Element of L() such that
A9: not P[x] by A8;
height(x) <= height(x) implies P[x] by A7;
hence contradiction by A9;
end;
A10: Q[ 0 ] by Th7;
for n be Nat holds Q[n] from NAT_1:sch 2(A10,A2);
hence thesis by A6;
end;
begin :: Join irreducible elements in a finite distributive lattice
registration
cluster distributive finite for LATTICE;
existence
proof
set D = {{}};
set R = the Order of D;
reconsider A = RelStr (#D,R#) as with_infima with_suprema Poset;
take A;
thus thesis;
end;
end;
definition
let L be LATTICE;
let x,y be Element of L;
pred x <(1) y means
x < y & not (ex z be Element of L st x < z & z < y);
end;
theorem Th8:
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
proof
let L be finite LATTICE;
let X be non empty Subset of L;
defpred P[Nat] means ex x be Element of L st x in X & $1=height(x);
ex k st P[k] & for n st P[n] holds n <= k
proof
A1: for k be Nat st P[k] holds k <= card the carrier of L
proof
let k be Nat;
assume P[k];
then consider x be Element of L such that
x in X and
A2: k=height(x);
ex B be Chain of Bottom L,x st k=card B by A2,Def3;
hence thesis by NAT_1:43;
end;
A3: ex k be Nat st P[k]
proof
consider x be object such that
A4: x in X by XBOOLE_0:def 1;
reconsider x as Element of L by A4;
ex B be Chain of Bottom L,x st height(x)= card B by Def3;
hence thesis by A4;
end;
consider k being Nat such that
A5: P[k] and
A6: for n being Nat st P[n] holds n <= k from NAT_1:sch 6 (A1,A3);
for n being Element of NAT st P[n] holds n <= k by A6;
hence thesis by A5;
end;
then consider k such that
A7: ( P[k])& for n st P[n] holds n <= k;
consider x be Element of L such that
A8: x in X and
A9: k=height(x) & for n st ex y be Element of L st y in X & n=height(y)
holds n <= k by A7;
for y be Element of L st y in X holds not x < y
proof
let y be Element of L;
assume that
A10: y in X and
A11: x < y;
height(x)<height(y) by A11,Th2;
hence contradiction by A9,A10;
end;
hence thesis by A8;
end;
definition
let L be finite LATTICE;
let A be non empty Chain of L;
func max(A) -> Element of L means
:Def5:
(for x be Element of L st x in A holds x <= it) & it in A;
existence
proof
defpred P[Nat] means ex x be Element of L st x in A & $1=height(x);
ex k st P[k] & for n st P[n] holds n <= k
proof
A1: for k be Nat st P[k] holds k <= card the carrier of L
proof
let k be Nat;
assume P[k];
then consider x be Element of L such that
x in A and
A2: k=height(x);
ex B be Chain of Bottom L,x st k=card B by A2,Def3;
hence thesis by NAT_1:43;
end;
A3: ex k be Nat st P[k]
proof
consider x be object such that
A4: x in A by XBOOLE_0:def 1;
reconsider x as Element of L by A4;
ex B be Chain of Bottom L,x st height(x)= card B by Def3;
hence thesis by A4;
end;
consider k being Nat such that
A5: P[k] and
A6: for n being Nat st P[n] holds n <= k from NAT_1:sch 6 (A1,A3);
for n being Element of NAT st P[n] holds n <= k by A6;
hence thesis by A5;
end;
then consider k such that
A7: ( P[k])& for n st P[n] holds n <= k;
consider x be Element of L such that
A8: x in A and
A9: k=height(x) & for n st ex z be Element of L st z in A & n=height(
z) holds n <=k by A7;
take x;
thus for w be Element of L st w in A holds w <= x
proof
let w be Element of L;
assume
A10: w in A;
then height(w)<=height(x) by A9;
hence thesis by A8,A10,Th5;
end;
thus thesis by A8;
end;
uniqueness
proof
let s,t be Element of L;
assume ( for x be Element of L st x in A holds x <= s)&( s in A & for y
be Element of L st y in A holds y <= t ) & t in A;
then t <= s & s <= t;
hence thesis by ORDERS_2:2;
end;
end;
theorem Th9:
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
proof
let L be finite LATTICE;
let y be Element of L;
( ex A be Chain of Bottom L,y st height(y)= card A)& for A be Chain of
Bottom L,y holds card A <= height(y) by Def3;
then consider A be Chain of Bottom L,y such that
A1: height(y)= card A & for A be Chain of Bottom L,y holds card A <= height(y);
set B=A\{y};
A2: the InternalRel of L is_strongly_connected_in B
proof
let p,q be object;
p in B & q in B implies [p,q] in the InternalRel of L or [q,p] in the
InternalRel of L
proof
assume
A3: p in B & q in B;
then
A4: p in A & q in A by XBOOLE_0:def 5;
reconsider p,q as Element of L by A3;
p <= q or q <= p by A4,ORDERS_2:11;
hence thesis by ORDERS_2:def 5;
end;
hence thesis;
end;
assume
A5: y <> Bottom L;
B is non empty
proof
Bottom L<=y by YELLOW_0:44;
then
A6: Bottom L in A by Def2;
assume
A7: B is empty;
not Bottom L in {y} by A5,TARSKI:def 1;
hence contradiction by A7,A6,XBOOLE_0:def 5;
end;
then reconsider B as non empty Chain of L by A2,ORDERS_2:def 7;
take x=max(B);
A8: not ex z be Element of L st x < z & z < y
proof
given z be Element of L such that
A9: x < z and
A10: z < y;
A11: Bottom L<=y by YELLOW_0:44;
then y in A by Def2;
then
A12: y in A \/ {z} by XBOOLE_0:def 3;
set C=A \/ {z};
{y} c= A
proof
let h be Element of L;
assume h in {y};
then
A13: h=y by TARSKI:def 1;
Bottom L<=y by YELLOW_0:44;
hence thesis by A13,Def2;
end;
then
A14: A=(A\{y})\/{y} by XBOOLE_1:45;
the InternalRel of L is_strongly_connected_in C
proof
let x1,y1 be object;
x1 in C & y1 in C implies [x1,y1] in the InternalRel of L or [y1,x1
] in the InternalRel of L
proof
assume
A15: x1 in C & y1 in C;
per cases by A15,XBOOLE_0:def 3;
suppose
A16: x1 in A & y1 in A;
then reconsider x1,y1 as Element of L;
x1 <= y1 or y1 <= x1 by A16,ORDERS_2:11;
hence thesis by ORDERS_2:def 5;
end;
suppose
A17: x1 in A & y1 in {z};
then
A18: y1=z by TARSKI:def 1;
reconsider x1,y1 as Element of L by A17;
x1 in A\{y} or x1 in {y} by A14,A17,XBOOLE_0:def 3;
then x1 <= x or x1 = y by Def5,TARSKI:def 1;
then x1 < y1 or x1 = y by A9,A18,ORDERS_2:7;
then x1 <= y1 or y1 < x1 by A10,A17,ORDERS_2:def 6,TARSKI:def 1;
then x1 <= y1 or y1 <= x1 by ORDERS_2:def 6;
hence thesis by ORDERS_2:def 5;
end;
suppose
A19: y1 in A & x1 in {z};
then
A20: x1=z by TARSKI:def 1;
reconsider x1,y1 as Element of L by A19;
y1 in A\{y} or y1 in {y} by A14,A19,XBOOLE_0:def 3;
then y1 <= x or y1 = y by Def5,TARSKI:def 1;
then y1 < x1 or y1 = y by A9,A20,ORDERS_2:7;
then y1 <= x1 or x1 <= y1 by A10,A20,ORDERS_2:def 6;
hence thesis by ORDERS_2:def 5;
end;
suppose
A21: x1 in {z} & y1 in {z};
then reconsider x1,y1 as Element of L;
x1=z by A21,TARSKI:def 1;
then x1<=y1 by A21,TARSKI:def 1;
hence thesis by ORDERS_2:def 5;
end;
end;
hence thesis;
end;
then
A22: C is strongly_connected Subset of L by ORDERS_2:def 7;
A23: z <= y by A10,ORDERS_2:def 6;
A24: for v be Element of L st v in A \/ {z} holds Bottom L <= v & v <= y
proof
let v be Element of L;
assume
A25: v in A \/ {z};
per cases by A25,XBOOLE_0:def 3;
suppose
A26: v in A;
thus Bottom L<=v by YELLOW_0:44;
thus thesis by A11,A26,Def2;
end;
suppose
v in {z};
hence thesis by A23,TARSKI:def 1,YELLOW_0:44;
end;
end;
not z in A
proof
assume
A27: z in A;
not z in {y} by A10,TARSKI:def 1;
then z in B by A27,XBOOLE_0:def 5;
then z <= x by Def5;
hence contradiction by A9,ORDERS_2:7;
end;
then
A28: card (A \/ {z})=card A + 1 by CARD_2:41;
Bottom L in A by A11,Def2;
then Bottom L in A \/ {z} by XBOOLE_0:def 3;
then A \/ {z} is Chain of Bottom L,y by A22,A11,A12,A24,Def2;
then card A + 1 <= card A by A1,A28;
hence contradiction by NAT_1:13;
end;
A29: x in B by Def5;
then not x in {y} by XBOOLE_0:def 5;
then
A30: not x=y by TARSKI:def 1;
Bottom L<=y & x in A by A29,XBOOLE_0:def 5,YELLOW_0:44;
then x<=y by Def2;
then x < y by A30,ORDERS_2:def 6;
hence thesis by A8;
end;
definition
let L be LATTICE;
func Join-IRR L -> Subset of L equals
{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};
coherence
proof
{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} c= the carrier of L
proof
let x be object;
assume x in {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};
then
ex a being Element of L st x=a & a <> Bottom L & for b,c be Element
of L holds a= b"\/"c implies a=b or a=c;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th10:
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
proof
let L be LATTICE;
let x be Element of L;
thus x in Join-IRR L implies x <> Bottom L & for b,c be Element of L holds x
= b"\/"c implies x=b or x=c
proof
assume x in Join-IRR L;
then
ex a being Element of L st x = a & a<>Bottom L & for b,c be Element of
L holds a= b"\/"c implies a=b or a=c;
hence thesis;
end;
thus thesis;
end;
theorem Th11:
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
proof
let L be finite distributive LATTICE;
let x be Element of L;
assume
A1: x in Join-IRR L;
then x<>Bottom L by Th10;
then consider z be Element of L such that
A2: z <(1) x by Th9;
A3: z < x by A2;
for y be Element of L st y < x holds y <= z
proof
let y be Element of L;
consider Y be set such that
A4: Y={g where g is Element of L : g < x & not (g <= z)};
A5: Y is empty
proof
A6: Y c= the carrier of L
proof
let f be object;
assume f in Y;
then ex g be Element of L st g=f & g<x & not g<=z by A4;
hence thesis;
end;
assume Y is non empty;
then consider a be Element of L such that
A7: a in Y and
A8: for b be Element of L st b in Y holds not a < b by A6,Th8;
A9: for t be Element of L holds t in Y iff t < x & not t <= z
proof
let t be Element of L;
t in Y implies t < x & not t <= z
proof
assume t in Y;
then ex g be Element of L st g=t & g < x & not g <= z by A4;
hence thesis;
end;
hence thesis by A4;
end;
then
A10: not a<=z by A7;
A11: z<=x by A3,ORDERS_2:def 6;
a<x by A9,A7;
then
A12: a"\/"z<>x by A1,A3,Th10;
a<x by A9,A7;
then a<=x by ORDERS_2:def 6;
then a"\/"z <= x by A11,YELLOW_5:9;
then
A13: a"\/"z<x by A12,ORDERS_2:def 6;
a"/\"a <= a"\/"z by YELLOW_5:5;
then
A14: a <= a"\/"z by YELLOW_5:2;
a<>a"\/"z
proof
assume a=a"\/"z;
z"/\"z<=a"\/"z by YELLOW_5:5;
then z<=a"\/"z by YELLOW_5:2;
then z<a"\/"z by A10,A14,ORDERS_2:def 6;
hence contradiction by A2,A13;
end;
then
A15: (a"\/"z)>a by A14,ORDERS_2:def 6;
not a"\/"z <= z by A10,YELLOW_5:3;
then a"\/"z in Y by A9,A13;
hence contradiction by A8,A15;
end;
assume y < x & not y <= z;
then y in Y by A4;
hence contradiction by A5;
end;
hence thesis by A3;
end;
Lm1: for L be finite distributive LATTICE for a being Element of L st for b be
Element of L st b < a holds sup(downarrow b /\ Join-IRR L) =b holds sup(
downarrow a /\ Join-IRR L) =a
proof
let L be finite distributive LATTICE;
let a be Element of L;
assume
A1: for b be Element of L st b < a holds sup(downarrow b /\ Join-IRR L) =b;
thus sup(downarrow a /\ Join-IRR L) = a
proof
per cases;
suppose
A2: a = Bottom L;
A3: {Bottom L} /\ Join-IRR L= {}
proof
set x = the Element of {Bottom L} /\ Join-IRR L;
assume
A4: {Bottom L} /\ Join-IRR L <> {};
then x in {Bottom L} by XBOOLE_0:def 4;
then
A5: x = Bottom L by TARSKI:def 1;
x in Join-IRR L by A4,XBOOLE_0:def 4;
hence contradiction by A5,Th10;
end;
downarrow a = {Bottom L} by A2,WAYBEL_4:23;
hence thesis by A2,A3,YELLOW_0:def 11;
end;
suppose
(not a in Join-IRR L) & a <> Bottom L;
then consider y,z be Element of L such that
A6: a= y"\/"z and
A7: a <> y and
A8: a <> z;
A9: y <= a by A6,YELLOW_0:22;
then
A10: y < a by A7,ORDERS_2:def 6;
A11: downarrow a /\ Join-IRR L c= (downarrow y /\ Join-IRR L) \/ (
downarrow z /\ Join-IRR L)
proof
let x be Element of L;
set x1=x,y1=y,a1=a,z1=z;
assume
A12: x in downarrow a /\ Join-IRR L;
then
A13: x in Join-IRR L by XBOOLE_0:def 4;
x in downarrow a by A12,XBOOLE_0:def 4;
then
A14: x1 <= a1 by WAYBEL_0:17;
x1 "/\" a1 = (x1"/\"y1) "\/" (x1"/\"z1) by A6,WAYBEL_1:def 3;
then x1 = (x1"/\"y1) "\/" (x1"/\"z1) by A14,YELLOW_0:25;
then x1 = x1"/\"y1 or x1 = x1"/\"z1 by A13,Th10;
then x1 <= y1 or x1 <= z1 by YELLOW_0:25;
then x1 in downarrow y1 or x1 in downarrow z1 by WAYBEL_0:17;
then x1 in downarrow y1 /\ Join-IRR L or x1 in downarrow z1 /\
Join-IRR L by A13,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
A15: ex_sup_of (downarrow y /\ Join-IRR L \/ downarrow z /\ Join-IRR L),
L & ex_sup_of downarrow y /\ Join-IRR L,L by YELLOW_0:17;
A16: ex_sup_of downarrow z /\ Join-IRR L,L by YELLOW_0:17;
A17: z <= a by A6,YELLOW_0:22;
(downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L) c=
downarrow a /\ Join-IRR L
proof
let x be Element of L;
(downarrow y /\ Join-IRR L) c= (downarrow a /\ Join-IRR L) & (
downarrow z /\ Join-IRR L) c= (downarrow a /\ Join-IRR L) by A9,A17,WAYBEL_0:21
,XBOOLE_1:26;
then
A18: (downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L) c=
downarrow a /\ Join-IRR L by XBOOLE_1:8;
assume x in (downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L);
hence thesis by A18;
end;
then downarrow a /\ Join-IRR L = (downarrow y /\ Join-IRR L) \/ (
downarrow z /\ Join-IRR L) by A11,XBOOLE_0:def 10;
then sup (downarrow a /\ Join-IRR L) = sup(downarrow y /\ Join-IRR L)
"\/" sup(downarrow z /\ Join-IRR L) by A15,A16,YELLOW_0:36;
then
A19: sup (downarrow a /\ Join-IRR L) = y "\/" sup(downarrow z /\
Join-IRR L) by A1,A10;
z < a by A8,A17,ORDERS_2:def 6;
hence thesis by A1,A6,A19;
end;
suppose
A20: a in Join-IRR L;
a <= a;
then a in downarrow a by WAYBEL_0:17;
then a in downarrow a /\ Join-IRR L by A20,XBOOLE_0:def 4;
then
A21: a <= sup(downarrow a /\ Join-IRR L) by YELLOW_0:17,YELLOW_4:1;
ex_sup_of downarrow a /\ Join-IRR L,L & ex_sup_of downarrow a,L by
YELLOW_0:17;
then sup(downarrow a /\ Join-IRR L) <= sup(downarrow a) by XBOOLE_1:17
,YELLOW_0:34;
then sup(downarrow a /\ Join-IRR L) <= a by WAYBEL_0:34;
hence thesis by A21,ORDERS_2:2;
end;
end;
end;
theorem Th12:
for L be distributive finite LATTICE for x be Element of L holds
sup (downarrow x /\ Join-IRR L) = x
proof
let L be distributive finite LATTICE;
let x be Element of L;
A1: x <= sup( downarrow x /\ Join-IRR L)
proof
defpred X[Element of L] means sup(downarrow $1 /\ Join-IRR L) = $1;
A2: for x being Element of L st for b be Element of L st b < x holds X[b]
holds X[x] by Lm1;
for x being Element of L holds X[x] from LattInd(A2);
hence thesis;
end;
ex_sup_of downarrow x /\ Join-IRR L,L & ex_sup_of downarrow x,L by
YELLOW_0:17;
then sup(downarrow x /\ Join-IRR L) <= sup(downarrow x) by XBOOLE_1:17
,YELLOW_0:34;
then sup(downarrow x /\ Join-IRR L) <= x by WAYBEL_0:34;
hence thesis by A1,ORDERS_2:2;
end;
begin :: Representation theorem
definition
let P be RelStr;
func LOWER(P) -> non empty set equals
{X where X is Subset of P:X is lower};
coherence
proof
{}P in {X where X is Subset of P:X is lower};
hence thesis;
end;
end;
theorem Th13:
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
proof
let L be distributive finite LATTICE;
set I = InclPoset LOWER(subrelstr Join-IRR L);
deffunc U(Element of L) = downarrow $1 /\ Join-IRR L;
consider r be ManySortedSet of the carrier of L such that
A1: for d be Element of L holds r.d= U(d) from PBOOLE:sch 5;
A2: rng r c= the carrier of I
proof
let t be object;
reconsider tt=t as set by TARSKI:1;
assume t in rng r;
then consider x be object such that
A3: x in dom r and
A4: t = r.x by FUNCT_1:def 3;
reconsider x as Element of L by A3;
A5: t=downarrow x /\ Join-IRR L by A1,A4;
then tt c= Join-IRR L by XBOOLE_1:17;
then reconsider t as Subset of subrelstr Join-IRR L by YELLOW_0:def 15;
A6: t is lower
proof
let c,d be Element of subrelstr Join-IRR L;
assume that
A7: c in t and
A8: d <= c;
A9: d is Element of Join-IRR L by YELLOW_0:def 15;
A10: Join-IRR L is non empty by A5,A7;
then d in Join-IRR L by A9;
then reconsider c1=c,d1=d as Element of L by A5,A7;
c in downarrow x by A5,A7,XBOOLE_0:def 4;
then
A11: c1 <= x by WAYBEL_0:17;
d1 <= c1 by A8,YELLOW_0:59;
then d1 <= x by A11,ORDERS_2:3;
then d1 in downarrow x by WAYBEL_0:17;
hence thesis by A5,A10,A9,XBOOLE_0:def 4;
end;
the carrier of I = LOWER(subrelstr Join-IRR L) by YELLOW_1:1;
hence thesis by A6;
end;
dom r = the carrier of L by PARTFUN1:def 2;
then reconsider r as Function of L,I by A2,FUNCT_2:def 1,RELSET_1:4;
A12: for x,y being Element of L holds (x <= y iff r.x <= r.y)
proof
let x,y be Element of L;
thus x <= y implies r.x <= r.y
proof
assume
A13: x <= y;
downarrow x /\ Join-IRR L c= downarrow y /\ Join-IRR L
proof
let a be Element of L;
assume a in downarrow x /\ Join-IRR L;
then
A14: a in downarrow x & a in Join-IRR L by XBOOLE_0:def 4;
downarrow x c= downarrow y by A13,WAYBEL_0:21;
hence thesis by A14,XBOOLE_0:def 4;
end;
then r.x c= downarrow y /\ Join-IRR L by A1;
then r.x c= r.y by A1;
hence thesis by YELLOW_1:3;
end;
thus r.x <= r.y implies x <= y
proof
r.x= downarrow x /\ Join-IRR L & r.y= downarrow y /\ Join-IRR L by A1;
then reconsider rx = r.x,ry= r.y as Subset of L;
assume r.x <= r.y;
then
A15: rx c= ry by YELLOW_1:3;
ex_sup_of rx,L & ex_sup_of ry,L by YELLOW_0:17;
then sup(rx) <= sup(ry) by A15,YELLOW_0:34;
then sup (downarrow x /\ Join-IRR L) <= sup (ry) by A1;
then sup (downarrow x /\ Join-IRR L) <= sup (downarrow y /\ Join-IRR L)
by A1;
then x <= sup (downarrow y /\ Join-IRR L) by Th12;
hence thesis by Th12;
end;
end;
the carrier of I c= rng r
proof
let x be object;
assume
A16: x in the carrier of I;
thus x in rng r
proof
x in LOWER(subrelstr Join-IRR L) by A16,YELLOW_1:1;
then consider X being Subset of subrelstr Join-IRR L such that
A17: x=X and
A18: X is lower;
the carrier of subrelstr Join-IRR L c= Join-IRR L by YELLOW_0:def 15;
then the carrier of subrelstr Join-IRR L c= the carrier of L by
XBOOLE_1:1;
then reconsider X1=X as Subset of L by XBOOLE_1:1;
ex y being set st y in dom r & x = r.y
proof
take y = sup X1;
dom r = the carrier of L by FUNCT_2:def 1;
hence y in dom r;
A19: downarrow(sup X1) /\ Join-IRR L c= X1
proof
let r be Element of L;
reconsider r1=r as Element of L;
assume
A20: r in downarrow(sup X1) /\ Join-IRR L;
then r in downarrow(sup X1) by XBOOLE_0:def 4;
then
A21: r1 <= sup X1 by WAYBEL_0:17;
per cases;
suppose
r1 in X1;
hence thesis;
end;
suppose
A22: not r1 in X1;
A23: r1 in Join-IRR L by A20,XBOOLE_0:def 4;
then consider z be Element of L such that
A24: z < r1 and
A25: for y be Element of L st y < r1 holds y <= z by Th11;
{r1} "/\" X1 is_<=_than z
proof
let a be Element of L;
A26: r1 in the carrier of subrelstr Join-IRR L by A23,YELLOW_0:def 15;
assume a in {r1} "/\" X1;
then a in {r1"/\"k where k is Element of L:k in X1} by
YELLOW_4:42;
then consider x be Element of L such that
A27: a=r1"/\"x and
A28: x in X1;
reconsider r9=r1,x9=x as Element of subrelstr Join-IRR L by A23
,A28,YELLOW_0:def 15;
A29: ex_inf_of {r1,x},L by YELLOW_0:17;
then
A30: a <= x by A27,YELLOW_0:19;
A31: a <> r1 by A18,A22,A28,A30,A26,YELLOW_0:60;
a <= r1 by A27,A29,YELLOW_0:19;
then a < r1 by A31,ORDERS_2:def 6;
hence thesis by A25;
end;
then
A32: sup ({r1} "/\" X1) <= z by YELLOW_0:32;
r1 = r1 "/\" sup X1 & r1 "/\" sup X1 = sup ({r1} "/\" X1) by A21,
WAYBEL_2:15,YELLOW_0:25;
hence thesis by A24,A32,ORDERS_2:7;
end;
end;
X1 c= downarrow(sup X1) /\ Join-IRR L
proof
let a be Element of L;
assume
A33: a in X1;
set A = a;
ex_sup_of X1,L by YELLOW_0:17;
then
A34: X1 is_<=_than "\/"(X1,L) by YELLOW_0:def 9;
ex y being Element of L st y in {sup X1} & A <= y
proof
take y = sup X1;
thus y in {sup X1} by TARSKI:def 1;
thus thesis by A33,A34;
end;
then
A35: A in downarrow {sup X1} by WAYBEL_0:def 15;
X is Subset of Join-IRR L by YELLOW_0:def 15;
hence a in downarrow(sup X1) /\ Join-IRR L by A33,A35,XBOOLE_0:def 4;
end;
then X1 = downarrow(sup X1) /\ Join-IRR L by A19,XBOOLE_0:def 10;
hence x=r.y by A1,A17;
end;
hence thesis by FUNCT_1:def 3;
end;
end;
then
A36: rng r = the carrier of I by XBOOLE_0:def 10;
r is one-to-one
proof
let x,y be Element of L;
r.y= downarrow y /\ Join-IRR L by A1;
then reconsider ry= r.y as Subset of L;
assume r.x = r.y;
then sup (downarrow x /\ Join-IRR L) = sup (ry) by A1;
then sup (downarrow x /\ Join-IRR L) = sup (downarrow y /\ Join-IRR L) by
A1;
then x = sup (downarrow y /\ Join-IRR L) by Th12;
hence thesis by Th12;
end;
then r is isomorphic by A36,A12,WAYBEL_0:66;
hence thesis by A1;
end;
theorem Th14:
for L be distributive finite LATTICE holds L, InclPoset LOWER(
subrelstr Join-IRR L) are_isomorphic
proof
let 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
by Th13;
hence thesis;
end;
definition
mode Ring_of_sets -> set means
:Def8:
it includes_lattice_of it;
existence
proof
set X = the set;
take R = bool X;
let a,b be set;
assume that
A1: a in R and
A2: b in R;
a /\ b c= X by A1,XBOOLE_1:108;
hence a /\ b in R;
a \/ b c= X by A1,A2,XBOOLE_1:8;
hence thesis;
end;
end;
registration
cluster non empty for Ring_of_sets;
existence
proof
take A={{}};
A includes_lattice_of A
proof
let a,b be set;
assume that
A1: a in A and
A2: b in A;
a={} by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
hence thesis by Def8;
end;
end;
Lm2: for L1,L2 be non empty RelStr for f be Function of L1,L2 holds f is
infs-preserving implies f is meet-preserving;
Lm3: for L1,L2 be non empty RelStr for f be Function of L1,L2 holds f is
sups-preserving implies f is join-preserving;
registration
let X be non empty Ring_of_sets;
cluster InclPoset X -> with_suprema with_infima distributive;
coherence
proof
A1: X includes_lattice_of X by Def8;
A2: InclPoset X is distributive
proof
let x,y,z be Element of InclPoset X;
x in the carrier of InclPoset X;
then
A3: x in X by YELLOW_1:1;
z in the carrier of InclPoset X;
then
A4: z in X by YELLOW_1:1;
then
A5: x /\ z in X by A1,A3;
then
A6: x "/\" z = x /\ z by YELLOW_1:9;
y in the carrier of InclPoset X;
then
A7: y in X by YELLOW_1:1;
then
A8: y \/ z in X by A1,A4;
then reconsider r = y \/ z as Element of InclPoset X by YELLOW_1:1;
A9: x /\ y in X by A1,A3,A7;
then reconsider r1 = x /\ y, r2 = x /\ z as Element of InclPoset X by A5,
YELLOW_1:1;
r1 in the carrier of InclPoset X;
then
A10: r1 in X by YELLOW_1:1;
r in the carrier of InclPoset X;
then r in X by YELLOW_1:1;
then x /\ r in X by A1,A3;
then x "/\" r = x /\ r by YELLOW_1:9;
then
A11: x /\ (y \/ z) = x /\ y \/ x /\ z & x /\ (y \/ z) = x "/\" (y "\/" z
) by A8,XBOOLE_1:23,YELLOW_1:8;
r2 in the carrier of InclPoset X;
then r2 in X by YELLOW_1:1;
then
A12: r1 \/ r2 in X by A1,A10;
x "/\" y = x /\ y by A9,YELLOW_1:9;
hence thesis by A11,A6,A12,YELLOW_1:8;
end;
( for x,y be set st x in X & y in X holds x /\ y in X)& for x,y be set
st x in X & y in X holds x \/ y in X by A1;
hence thesis by A2,YELLOW_1:11,12;
end;
end;
theorem Th15:
for L be finite LATTICE holds LOWER(subrelstr Join-IRR L) is Ring_of_sets
proof
let L be finite LATTICE;
set X = LOWER(subrelstr Join-IRR L);
X includes_lattice_of X
proof
let a,b be set;
assume that
A1: a in X and
A2: b in X;
A3: a \/ b in X
proof
consider Z1 be Subset of subrelstr Join-IRR L such that
A4: b=Z1 and
A5: Z1 is lower by A2;
consider Z be Subset of subrelstr Join-IRR L such that
A6: a=Z and
A7: Z is lower by A1;
Z \/ Z1 is lower by A7,A5,WAYBEL_0:27;
hence thesis by A6,A4;
end;
a /\ b in X
proof
consider Z1 be Subset of subrelstr Join-IRR L such that
A8: b=Z1 and
A9: Z1 is lower by A2;
consider Z be Subset of subrelstr Join-IRR L such that
A10: a=Z and
A11: Z is lower by A1;
Z /\ Z1 is lower by A11,A9,WAYBEL_0:27;
hence thesis by A10,A8;
end;
hence thesis by A3;
end;
hence thesis by Def8;
end;
theorem
for L be finite LATTICE holds L is distributive iff ex X be non empty
Ring_of_sets st L, InclPoset X are_isomorphic
proof
let L be finite LATTICE;
thus L is distributive implies ex X be non empty Ring_of_sets st L,
InclPoset X are_isomorphic
proof
consider X be set such that
A1: X = LOWER(subrelstr Join-IRR L);
A2: X is Ring_of_sets by A1,Th15;
assume L is distributive;
then L,InclPoset X are_isomorphic by A1,Th14;
hence thesis by A1,A2;
end;
given X be non empty Ring_of_sets such that
A3: L, InclPoset X are_isomorphic;
consider f be Function of L, InclPoset X such that
A4: f is isomorphic by A3;
A5: f is one-to-one by A4,WAYBEL_0:66;
f is infs-preserving & f is join-preserving by A4,Lm3,WAYBEL13:20;
hence thesis by A5,Lm2,WAYBEL_6:3;
end;