Copyright (c) 2000 Association of Mizar Users
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;
definitions TARSKI, WAYBEL_0, WAYBEL_1, LATTICE3, RELAT_2, COHSP_1, XBOOLE_0;
theorems WAYBEL_0, WAYBEL_1, WAYBEL_2, YELLOW_0, YELLOW_1, YELLOW_4, LATTICE3,
TARSKI, FUNCT_1, FUNCT_2, ORDERS_1, WAYBEL_4, CARD_1, CARD_2, NAT_1,
AXIOMS, YELLOW_5, REAL_1, PBOOLE, COHSP_1, WAYBEL13, WAYBEL_6, RELSET_1,
XBOOLE_0, XBOOLE_1;
schemes NAT_1, PRALG_2;
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
for x be Element of L st x in A holds x in B;
compatibility
proof
thus A c= B iff (for x be Element of L st x in A holds x in B)
proof
thus A c= B implies (for x be Element of L st x in A holds x in B);
(for x be Element of L st x in A holds x in B) implies A c= B
proof
assume A1: for x be Element of L st x in A holds x in B;
thus A c= B
proof
let x be set;
assume x in A;
hence x in B by A1;
end;
end;
hence thesis;
end;
end;
end;
definition
let L be LATTICE;
cluster non empty Chain of L;
existence
proof
{Bottom L} is Chain of L by ORDERS_1:35;
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_1:36;
A2: y in A by TARSKI:def 2;
A3: x in A by TARSKI:def 2;
for z be Element of L st z in A holds x <= z & z <= y
proof
let z be Element of L;
assume A4: z in A;
per cases by A4,TARSKI:def 2;
suppose z=x;
hence thesis by A1;
suppose z=y;
hence thesis by A1;
end;
hence thesis by A2,A3;
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;
assume A1: x <= y;
then A2: {x,y} is Chain of L by ORDERS_1:36;
A3: x in {x,y} by TARSKI:def 2;
A4: y in {x,y} by TARSKI:def 2;
for z be Element of L st z in {x,y} holds x <= z & z <= y
proof
let z be Element of L;
assume A5: z in {x,y};
per cases by A5,TARSKI:def 2;
suppose z=x;
hence thesis by A1;
suppose z=y;
hence thesis by A1;
end;
hence thesis by A1,A2,A3,A4,Def2;
end;
reserve n,k for Nat;
definition
let L be finite LATTICE;
let x be Element of L;
func height(x) -> 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;
Bottom L <= x by YELLOW_0:44;
then A1: {Bottom L,x} is Chain of Bottom L,x by Th1;
ex k st P[k] & for n st P[n] holds n <= k
proof
A2: for k st P[k] holds k <= card the carrier of L by CARD_1:80;
A3: ex k st P[k]
proof
P[card{Bottom L,x}] by A1;
hence thesis;
end;
thus thesis from Max (A2,A3);
end;
then consider k such that A4: P[k] & for n st P[n] holds n <= k;
take k;
thus P[k] by A4;
let A be Chain of Bottom L,x;
thus thesis by A4;
end;
uniqueness
proof
let a,b be Nat such that
A5: (ex A be Chain of Bottom L,x st a= card A) and
A6: (for A be Chain of Bottom L,x holds card A <= a) and
A7: (ex B be Chain of Bottom L,x st b= card B) and
A8: (for A be Chain of Bottom L,x holds card A <= b);
consider A be Chain of Bottom L,x such that A9: a= card A &
(for A be Chain of Bottom L,x holds card A <= a) by A5,A6;
consider B be Chain of Bottom L,x such that A10: b= card B &
(for A be Chain of Bottom L,x holds card A <= b) by A7,A8;
A11: a<=b by A9,A10;
b<=a by A9,A10;
hence thesis by A11,AXIOMS:21;
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;
assume
A1: a < b;
(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
A2: height(a) = card A and
(for C be Chain of Bottom L,a holds card C <= height(a));
(ex B be Chain of Bottom L,b st height(b) = card B) &
for D be Chain of Bottom L,b holds card D <= height(b) by Def3;
then consider B be Chain of Bottom L,b such that
height(b) = card B and
A3: (for B be Chain of Bottom L,b holds card B <= height(b));
A4: Bottom L<=a by YELLOW_0:44;
A5: not b in A
proof
assume b in A;
then Bottom L <= b & b <= a by A4,Def2;
hence contradiction by A1,ORDERS_1:30;
end;
set C=A \/ {b};
Bottom L in A by A4,Def2;
then A6: Bottom L in C by XBOOLE_0:def 2;
A7: b in C
proof
b in {b} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
end;
A8: for z be Element of L st z in C holds Bottom L <= z & z <= b
proof
let z be Element of L;
assume A9: z in C;
per cases by A9,XBOOLE_0:def 2;
suppose A10: z in A;
thus Bottom L<=z by YELLOW_0:44;
z<=a by A4,A10,Def2;
then z<b by A1,ORDERS_1:32;
hence thesis by ORDERS_1:def 10;
suppose z in {b};
hence thesis by TARSKI:def 1,YELLOW_0:44;
end;
A11: C is strongly_connected Subset of L
proof
the InternalRel of L is_strongly_connected_in C
proof
let x,y be set;
x in C & y in C implies [x,y] in the InternalRel of L
or [y,x] in the InternalRel of L
proof
assume A12: x in C & y in C;
per cases by A12,XBOOLE_0:def 2;
suppose A13: x in A & y in A;
then reconsider x,y as Element of L;
x <= y or y <= x by A13,ORDERS_1:38;
hence thesis by ORDERS_1:def 9;
suppose A14: x in A & y in {b};
then A15: y=b by TARSKI:def 1;
reconsider x as Element of L by A14;
Bottom L<=a by YELLOW_0:44;
then x <= a by A14,Def2;
then x < b by A1,ORDERS_1:32;
then x <= b by ORDERS_1:def 10;
hence thesis by A15,ORDERS_1:def 9;
suppose A16: x in {b} & y in A;
then A17: x=b by TARSKI:def 1;
reconsider y as Element of L by A16;
Bottom L<=a by YELLOW_0:44;
then y <= a by A16,Def2;
then y < b by A1,ORDERS_1:32;
then y <= b by ORDERS_1:def 10;
hence thesis by A17,ORDERS_1:def 9;
suppose A18: x in {b} & y in {b};
then reconsider x,y as Element of L;
x=b & y=b by A18,TARSKI:def 1;
then x <= y;
hence thesis by ORDERS_1:def 9;
end;
hence thesis;
end;
hence thesis by ORDERS_1:def 11;
end;
Bottom L <= b by YELLOW_0:44;
then A19: C is Chain of Bottom L,b by A6,A7,A8,A11,Def2;
card C = (card A)+1 by A5,CARD_2:54;
then height(a) + 1 <= height(b) by A2,A3,A19;
hence thesis by NAT_1:38;
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;
thus x < y iff height(x) < height(y)
proof
thus x < y implies height(x) < height(y) by Th2;
height(x) < height(y) implies x < y
proof
assume A2: height(x) < height(y);
per cases by A1,ORDERS_1:38;
suppose x <= y;
hence thesis by A2,ORDERS_1:def 10;
suppose y <= x;
then x=y or y < x by ORDERS_1:def 10;
hence thesis by A2,Th2;
end;
hence thesis;
end;
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 A2: height(x) = height(y) & x<>y;
then A3:(x<=y or y<=x) & x<>y by A1,ORDERS_1:38;
height(x)<>height(y)
proof
per cases by A3,ORDERS_1:def 10;
suppose x < y;
hence thesis by A1,Th3;
suppose y < x;
hence thesis by A1,Th3;
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;
thus x <= y iff height(x) <= height(y)
proof
A2: x <= y implies height(x) <= height(y)
proof
assume x<=y;
then x<y or x=y by ORDERS_1:def 10;
hence thesis by A1,Th3;
end;
height(x) <= height(y) implies x<=y
proof
assume height(x) <= height(y);
then height(x) < height(y) or height(x) = height(y) by REAL_1:def 5;
then x<y or height(x) = height(y) by A1,Th3;
hence thesis by A1,Th4,ORDERS_1:def 10;
end;
hence thesis by A2;
end;
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: height (x) = 1 implies x = Bottom L
proof
assume A2: height (x) = 1 & x <> Bottom L;
(ex A be Chain of Bottom L,x st height (x)= card A) &
for A be Chain of Bottom L,x holds card A <= height (x) by Def3;
then consider A be Chain of Bottom L,x such that A3: height (x)= card A
& for A be Chain of Bottom L,x holds card A <= height (x);
A4: {Bottom L,x} is Chain of Bottom L,x
proof
A5: Bottom L<=x by YELLOW_0:44;
then A6: {Bottom L,x} is Chain of L by ORDERS_1:36;
A7: x in {Bottom L,x} by TARSKI:def 2;
A8: Bottom L in {Bottom L,x} by TARSKI:def 2;
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 A9: z in {Bottom L,x};
per cases by A9,TARSKI:def 2;
suppose z=Bottom L;
hence thesis by YELLOW_0:44;
suppose z=x;
hence thesis by YELLOW_0:44;
end;
hence thesis by A5,A6,A7,A8,Def2;
end;
card {Bottom L,x} = 2 by A2,CARD_2:76;
hence contradiction by A2,A3,A4;
end;
x = Bottom L implies height (x) = 1
proof
assume A10: x = Bottom L;
(ex A be Chain of Bottom L,Bottom L st height(Bottom L)= card A) &
for A be Chain of Bottom L,Bottom L holds card A <= height(Bottom
L) by Def3;
then consider A be Chain of Bottom L,Bottom L such that A11: height(
Bottom
L)= card A &
for A be Chain of Bottom L,Bottom L holds card A <= height(Bottom
L);
A12: for B be Chain of Bottom L,Bottom L holds B = {Bottom L}
proof
let B be Chain of Bottom L,Bottom L;
A13: 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_1:25;
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 A13,XBOOLE_0:def 10;
end;
card {Bottom L} = 1 by CARD_1:79;
hence thesis by A10,A11,A12;
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;
(ex A be Chain of Bottom L,x st height (x)= card A) &
for A be Chain of Bottom L,x holds card A <= height (x) by Def3;
then consider A be Chain of Bottom L,x such that height (x)= card A
and A1: (for B be Chain of Bottom L,x holds card B <= height (x));
Bottom L<=x by YELLOW_0:44;
then A2: {Bottom L,x} is Chain of Bottom L,x by Th1;
then A3: card {Bottom L,x} <= height (x) by A1;
per cases;
suppose x<>Bottom L;
then card {Bottom L,x} = 2 by CARD_2:76;
hence thesis by A3,AXIOMS:22;
suppose A4: x=Bottom L;
then A5: card {Bottom L,Bottom L} <= height (Bottom L) by A1,A2;
{Bottom L,Bottom L}={Bottom L}
proof
A6: {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;
{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;
hence thesis by A6,XBOOLE_0:def 10;
end;
hence thesis by A4,A5,CARD_1:79;
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
let x be Element of L();
defpred Q[Nat] means
for x be Element of L() st height(x) <= $1
holds P[x];
A2: for n be Nat holds Q[n]
proof
A3: Q[0]
proof
for x be Element of L() st height(x) <= 0 holds P[x]
proof
let x be Element of L();
assume (height(x) <= 0) & not P[x];
then height(x) < 0 + 1 by NAT_1:38;
hence contradiction by Th7;
end;
hence thesis;
end;
A4: for n be Nat st Q[n] holds Q[n+1]
proof
let n be Nat;
assume A5: Q[n];
for x be Element of L() st height(x) <= n+1 holds P[x]
proof
let x be Element of L();
assume height(x) <= n+1;
then A6: height(x) = n+1 or height(x) <= n by NAT_1:26;
per cases by A5,A6;
suppose A7: 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 A7,NAT_1:38;
hence thesis by A5;
end;
hence thesis by A1;
suppose P[x];
hence thesis;
end;
hence thesis;
end;
thus thesis from Ind (A3,A4);
end;
( 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 A8: (for x be Element of L() st height(x) <= height(x) holds P[x])
& not (for x be Element of L() holds P[x]);
then consider x be Element of L() such that A9: not P[x];
height(x) <= height(x) implies P[x] by A8;
hence contradiction by A9;
end;
hence thesis by A2;
end;
begin :: Join irreducible elements in a finite distributive lattice
definition
cluster distributive finite LATTICE;
existence
proof
consider s being set;
set D = {s};
consider R being 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 :Def4:
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 st P[k] holds k <= card the carrier of L
proof
let k;
assume P[k];
then consider x be Element of L such that A2: x in X & k=height(x);
consider B be Chain of Bottom L,x such that A3: k=card B by A2,Def3;
thus thesis by A3,CARD_1:80;
end;
A4: ex k st P[k]
proof
consider x be set such that A5: x in X by XBOOLE_0:def 1;
reconsider x as Element of L by A5;
(ex B be Chain of Bottom L,x st height(x)= card B) &
for B be Chain of Bottom L,x holds card B <= height(x) by Def3;
then consider B be Chain of Bottom L,x such that A6: height(x)= card B &
for B be Chain of Bottom L,x holds card B <= height(x);
thus thesis by A5,A6;
end;
thus thesis from Max (A1,A4);
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 & 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 A9: y in X & x < y;
then height(x)<height(y) by Th2;
hence contradiction by A8,A9;
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 st P[k] holds k <= card the carrier of L
proof
let k;
assume P[k];
then consider x be Element of L such that A2: x in A & k=height(x);
consider B be Chain of Bottom L,x such that A3: k=card B by A2,Def3;
thus thesis by A3,CARD_1:80;
end;
A4: ex k st P[k]
proof
consider x be set such that A5: x in A by XBOOLE_0:def 1;
reconsider x as Element of L by A5;
(ex B be Chain of Bottom L,x st height(x)= card B) &
for B be Chain of Bottom L,x holds card B <= height(x) by Def3;
then consider B be Chain of Bottom L,x such that A6: height(x)= card B &
for B be Chain of Bottom L,x holds card B <= height(x);
thus thesis by A5,A6;
end;
thus thesis from Max (A1,A4);
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 & k=height(x) and
A9: 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 A8,A9;
hence thesis by A8,A10,Th5;
end;
thus x in A by A8;
end;
uniqueness
proof
let s,t be Element of L such that
A11: for x be Element of L st x in A holds x <= s and A12: s in A and
A13: for y be Element of L st y in A holds y <= t and A14: t in A;
consider A be non empty Chain of L such that
A15: (for x be Element of L st x in A holds x <= s) & s in A and
A16: (for y be Element of L st y in A holds y <= t) & t in A by A11,A12,A13
,A14;
A17: t <= s by A15,A16;
s <= t by A15,A16;
hence s=t by A17,ORDERS_1:25;
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;
assume A1: y <> Bottom 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 A2: height(y)= card A &
for A be Chain of Bottom L,y holds card A <= height(y);
set B=A\{y};
A3:B is strongly_connected Subset of L
proof
the InternalRel of L is_strongly_connected_in B
proof
let p,q be set;
p in B & q in B implies [p,q] in the InternalRel of L
or [q,p] in the InternalRel of L
proof
assume A4:p in B & q in B;
then A5: p in A & not (p in {y}) & q in A & not (q in {y}) by XBOOLE_0
:def 4;
reconsider p,q as Element of L by A4;
p <= q or q <= p by A5,ORDERS_1:38;
hence thesis by ORDERS_1:def 9;
end;
hence thesis;
end;
hence thesis by ORDERS_1:def 11;
end;
B is non empty
proof
assume A6: B is empty;
Bottom L<=y by YELLOW_0:44;
then A7: Bottom L in A by Def2;
not (Bottom L in {y}) by A1,TARSKI:def 1;
hence contradiction by A6,A7,XBOOLE_0:def 4;
end;
then reconsider B as non empty Chain of L by A3;
take x=max(B);
A8: x < y
proof
A9: x in B by Def5;
A10: Bottom L<=y by YELLOW_0:44;
x in A & not x in {y} by A9,XBOOLE_0:def 4;
then Bottom L<=x & x<=y & not x=y by A10,Def2,TARSKI:def 1;
hence thesis by ORDERS_1:def 10;
end;
not ex z be Element of L st x < z & z < y
proof
given z be Element of L such that A11: x < z & z < y;
A12: not z in A
proof
assume A13: z in A;
not (z in {y}) by A11,TARSKI:def 1;
then z in B by A13,XBOOLE_0:def 4;
then z <= x & x < z by A11,Def5;
hence contradiction by ORDERS_1:32;
end;
set C=A \/ {z};
A14: C is strongly_connected Subset of L
proof
A15: A=(A\{y})\/{y}
proof
{y} c= A
proof
let h be Element of L;
assume h in {y};
then A16: h=y by TARSKI:def 1;
Bottom L<=y by YELLOW_0:44;
hence thesis by A16,Def2;
end;
hence thesis by XBOOLE_1:45;
end;
the InternalRel of L is_strongly_connected_in C
proof
let x1,y1 be set;
x1 in C & y1 in C implies [x1,y1] in the InternalRel of L
or [y1,x1] in the InternalRel of L
proof
assume A17: x1 in C & y1 in C;
per cases by A17,XBOOLE_0:def 2;
suppose A18: x1 in A & y1 in A;
then reconsider x1,y1 as Element of L;
x1 <= y1 or y1 <= x1 by A18,ORDERS_1:38;
hence thesis by ORDERS_1:def 9;
suppose A19: x1 in A & y1 in {z};
then A20: y1=z by TARSKI:def 1;
reconsider x1,y1 as Element of L by A19;
x1 in A\{y} or x1 in {y} by A15,A19,XBOOLE_0:def 2;
then x1 <= x or x1 = y by Def5,TARSKI:def 1;
then x1 < y1 or x1 = y by A11,A20,ORDERS_1:32;
then x1 <= y1 or y1 < x1
by A11,A19,ORDERS_1:def 10,TARSKI:def 1;
then x1 <= y1 or y1 <= x1 by ORDERS_1:def 10;
hence thesis by ORDERS_1:def 9;
suppose A21: y1 in A & x1 in {z};
then A22: x1=z by TARSKI:def 1;
reconsider x1,y1 as Element of L by A21;
y1 in A\{y} or y1 in {y} by A15,A21,XBOOLE_0:def 2;
then y1 <= x or y1 = y by Def5,TARSKI:def 1;
then y1 < x1 or y1 = y by A11,A22,ORDERS_1:32;
then y1 <= x1 or x1 <= y1 by A11,A22,ORDERS_1:def 10;
hence thesis by ORDERS_1:def 9;
suppose A23: x1 in {z} & y1 in {z};
then reconsider x1,y1 as Element of L;
x1=z & y1=z by A23,TARSKI:def 1;
then x1<=y1;
hence thesis by ORDERS_1:def 9;
end;
hence thesis;
end;
hence thesis by ORDERS_1:def 11;
end;
A24: Bottom L<=y by YELLOW_0:44;
then A25: Bottom L in A by Def2;
A26: y in A by A24,Def2;
A27: Bottom L in A \/ {z} by A25,XBOOLE_0:def 2;
A28: y in A \/ {z} by A26,XBOOLE_0:def 2;
A29: Bottom L <= z & z <= y by A11,ORDERS_1:def 10,YELLOW_0:44;
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 A30:v in A \/ {z};
per cases by A30,XBOOLE_0:def 2;
suppose A31: v in A;
thus Bottom L<=v by YELLOW_0:44;
thus thesis by A24,A31,Def2;
suppose v in {z};
hence thesis by A29,TARSKI:def 1;
end;
then A32: A \/ {z} is Chain of Bottom L,y by A14,A24,A27,A28,Def2;
card (A \/ {z})=card A + 1 by A12,CARD_2:54;
then card A + 1 <= card A by A2,A32;
hence contradiction by NAT_1:38;
end;
hence thesis by A8,Def4;
end;
definition
let L be LATTICE;
func Join-IRR L -> Subset of L equals :Def6:
{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 set;
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;
A1: Join-IRR L = {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} by Def6;
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 by A1;
hence thesis;
end;
thus x <> Bottom
L & (for b,c be Element of L holds x= b"\/"c implies x=b or x=c)
implies x in Join-IRR L by A1;
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 & for b,c be Element of L holds x= b"\/"c implies x=b or x=c by Th10;
then consider z be Element of L such that A2: z <(1) x by Th9;
A3: z < x & not (ex v be Element of L st z < v & v < x) by A2,Def4;
for y be Element of L st y < x holds y <= z
proof
let y be Element of L;
assume A4: (y < x) & not (y <= z);
consider Y be set such that
A5: Y={g where g is Element of L : g < x & not (g <= z)};
A6: Y is empty
proof
assume A7: Y is non empty;
A8: 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 consider g be Element of L
such that A9: g=t & g < x & not (g <= z) by A5;
thus thesis by A9;
end;
hence thesis by A5;
end;
Y is Subset of L
proof
Y c= the carrier of L
proof
let f be set;
assume f in Y;
then consider g be Element of L such that A10: g=f & g<x & not(g<=z
)
by A5;
thus thesis by A10;
end;
hence thesis;
thus thesis;
end;
then consider a be Element of L such that
A11: a in Y and
A12: for b be Element of L st b in Y holds not (a < b) by A7,Th8;
A13: a<x & not(a<=z) by A8,A11;
A14: a"\/"z<x
proof
a<x by A8,A11;
then A15: a<=x by ORDERS_1:def 10;
z<=x by A3,ORDERS_1:def 10;
then A16: a"\/"z <= x by A15,YELLOW_5:9;
a"\/"z<>x by A1,A3,A13,Th10;
hence thesis by A16,ORDERS_1:def 10;
end;
not(a"\/"z <= z) by A13,YELLOW_5:3;
then A17: a"\/"z in Y by A8,A14;
(a"\/"z)>a
proof
a"/\"a <= a"\/"z by YELLOW_5:5;
then A18: a <= a"\/"z by YELLOW_5:2;
a<>a"\/"z
proof
assume a=a"\/"z;
z<a"\/"z
proof
z"/\"z<=a"\/"z by YELLOW_5:5;
then z<=a"\/"z by YELLOW_5:2;
hence thesis by A13,A18,ORDERS_1:def 10;
end;
hence contradiction by A2,A14,Def4;
end;
hence thesis by A18,ORDERS_1:def 10;
end;
hence contradiction by A12,A17;
end;
y in Y by A4,A5;
hence contradiction by A6;
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;
then A3: downarrow a = {Bottom L} by WAYBEL_4:23;
{Bottom L} /\ Join-IRR L= {}
proof
assume
A4: {Bottom L} /\ Join-IRR L <> {};
consider x be Element of {Bottom L} /\ Join-IRR L;
x in {Bottom L} & x in Join-IRR L by A4,XBOOLE_0:def 3;
then x = Bottom L & x<>Bottom L & (for b,c be Element of L holds
x= b"\/"c implies x=b or x=c) by Th10,TARSKI:def 1;
hence contradiction;
end;
hence thesis by A2,A3,YELLOW_0:def 11;
suppose (not a in Join-IRR L) & a <> Bottom L;
then consider y,z be Element of L such that
A5: a= y"\/"z and
A6: a <> y and
A7: (a <> z) by Th10;
A8: y <= a by A5,YELLOW_0:22;
then A9: y < a by A6,ORDERS_1:def 10;
A10: z <= a by A5,YELLOW_0:22;
then A11: z < a by A7,ORDERS_1:def 10;
A12: downarrow a /\ Join-IRR L =
(downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L)
proof
thus downarrow a /\ Join-IRR L c=
(downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L)
proof
let x be Element of L;
assume
x in downarrow a /\ Join-IRR L;
then A13: x in downarrow a & x in Join-IRR L by XBOOLE_0:def 3;
set x1=x,y1=y,a1=a,z1=z;
A14: x1 "/\" a1 = (x1"/\"y1) "\/" (x1"/\"z1) by A5,WAYBEL_1:def 3;
x1 <= a1 by A13,WAYBEL_0:17;
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 3;
hence thesis by XBOOLE_0:def 2;
end;
thus (downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L) c=
downarrow a /\ Join-IRR L
proof
let x be Element of L;
assume
A15: x in (downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L);
downarrow y c= downarrow a by A8,WAYBEL_0:21;
then A16: (downarrow y /\ Join-IRR L) c= (downarrow a /\ Join-IRR L)
by XBOOLE_1:26;
downarrow z c= downarrow a by A10,WAYBEL_0:21;
then (downarrow z /\ Join-IRR L) c= (downarrow a /\ Join-IRR L)
by XBOOLE_1:26;
then (downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L) c=
downarrow a /\ Join-IRR L by A16,XBOOLE_1:8;
hence thesis by A15;
end;
end;
A17: ex_sup_of (downarrow y /\ Join-IRR L \/ downarrow z /\ Join-IRR L),L
by YELLOW_0:17;
A18: ex_sup_of downarrow y /\ Join-IRR L,L by YELLOW_0:17;
ex_sup_of downarrow z /\ Join-IRR L,L by YELLOW_0:17;
then sup (downarrow a /\ Join-IRR L) =
sup(downarrow y /\ Join-IRR L) "\/" sup(downarrow z /\ Join-IRR L)
by A12,A17,A18,YELLOW_0:36;
then sup (downarrow a /\ Join-IRR L) = y "\/" sup(downarrow z /\
Join-IRR L)
by A1,A9;
hence thesis by A1,A5,A11;
suppose
A19: a in Join-IRR L;
A20: downarrow a /\ Join-IRR L c= downarrow a by XBOOLE_1:17;
A21: ex_sup_of downarrow a /\ Join-IRR L,L by YELLOW_0:17;
ex_sup_of downarrow a,L by YELLOW_0:17;
then sup(downarrow a /\ Join-IRR L) <= sup(downarrow a) by A20,A21,
YELLOW_0:34;
then A22: sup(downarrow a /\ Join-IRR L) <= a by WAYBEL_0:34;
a <= sup(downarrow a /\ Join-IRR L)
proof
a <= a;
then a in downarrow a by WAYBEL_0:17;
then a in downarrow a /\ Join-IRR L by A19,XBOOLE_0:def 3;
hence thesis by A21,YELLOW_4:1;
end;
hence sup(downarrow a /\ Join-IRR L) = a by A22,ORDERS_1:25;
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: downarrow x /\ Join-IRR L c= downarrow x by XBOOLE_1:17;
A2: ex_sup_of downarrow x /\ Join-IRR L,L by YELLOW_0:17;
ex_sup_of downarrow x,L by YELLOW_0:17;
then sup(downarrow x /\ Join-IRR L) <= sup(downarrow x) by A1,A2,YELLOW_0:34;
then A3: sup(downarrow x /\ Join-IRR L) <= x by WAYBEL_0:34;
x <= sup( downarrow x /\ Join-IRR L)
proof
defpred X[Element of L] means sup(downarrow $1 /\ Join-IRR L) = $1;
A4: 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(A4);
hence thesis;
end;
hence sup(downarrow x /\ Join-IRR L)= x by A3,ORDERS_1:25;
end;
begin :: Representation theorem
definition
let P be RelStr;
func LOWER(P) -> non empty set equals :Def7:
{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 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
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 LambdaDMS;
A2: for a being Element of L holds r.a= downarrow a /\ Join-IRR L by A1;
A3: dom r = the carrier of L by PBOOLE:def 3;
rng r c= the carrier of I
proof
let t be set;
assume t in rng r;
then consider x be set such that A4: x in dom r & t = r.x by FUNCT_1:
def 5;
x in the carrier of L by A4,PBOOLE:def 3;
then reconsider x as Element of L;
A5: the carrier of I = LOWER(subrelstr Join-IRR L) by YELLOW_1:1;
A6: t=downarrow x /\ Join-IRR L by A1,A4;
then t c= Join-IRR L by XBOOLE_1:17;
then t c= the carrier of subrelstr Join-IRR L by YELLOW_0:def 15;
then reconsider t as Subset of subrelstr Join-IRR L;
t is lower
proof
let c,d be Element of subrelstr Join-IRR L;
assume A7: c in t & d <= c;
then A8: c in downarrow x & c in Join-IRR L by A6,XBOOLE_0:def 3;
A9: Join-IRR L is non empty by A6,A7;
A10: d is Element of Join-IRR L by YELLOW_0:def 15;
then d in Join-IRR L by A9;
then reconsider c1=c,d1=d as Element of L
by A6,A7;
A11: d1 <= c1 by A7,YELLOW_0:60;
c1 <= x by A8,WAYBEL_0:17;
then d1 <= x by A11,ORDERS_1:26;
then d1 in downarrow x by WAYBEL_0:17;
hence thesis by A6,A9,A10,XBOOLE_0:def 3;
end;
then t in {X where X is Subset of subrelstr Join-IRR L : X is lower};
hence thesis by A5,Def7;
end;
then r is Function of the carrier of L, the carrier of I
by A3,FUNCT_2:def 1,RELSET_1:11;
then reconsider r as map of L,I;
A12: r is one-to-one
proof
let x,y be Element of L;
assume
A13: r.x = r.y;
r.y= downarrow y /\ Join-IRR L by A1;
then reconsider ry= r.y as Subset of L;
sup (downarrow x /\ Join-IRR L) = sup (ry) by A1,A13;
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 x=y by Th12;
end;
A14: rng r = the carrier of I
proof
thus rng r c= the carrier of I;
thus the carrier of I c= rng r
proof
let x be set;
assume
A15: x in the carrier of I;
thus x in rng r
proof
x in LOWER(subrelstr Join-IRR L) by A15,YELLOW_1:1;
then x in {X where X is Subset of subrelstr Join-IRR L : X is lower
}
by Def7;
then consider X being Subset of subrelstr Join-IRR L such that
A16: x=X & X is lower;
X is Subset of L
proof
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 X c= the carrier of L by XBOOLE_1:1;
hence thesis;
end;
then reconsider X1=X as Subset of L;
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;
X1 = downarrow(sup X1) /\ Join-IRR L
proof
thus X1 c= downarrow(sup X1) /\ Join-IRR L
proof
let a be Element of L;
assume
A17: a in X1;
set A = a;
thus a in downarrow(sup X1) /\ Join-IRR L
proof
ex_sup_of X1,L by YELLOW_0:17;
then A18: X1 is_<=_than "\/"(X1,L) by YELLOW_0:def 9;
A in downarrow {sup X1}
proof
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 A <= y by A17,A18,LATTICE3:def 9;
end;
hence thesis by WAYBEL_0:def 15;
end;
then A19: a in downarrow(sup X1) by WAYBEL_0:
def 17;
X is Subset of Join-IRR L by YELLOW_0:def 15;
hence thesis by A17,A19,XBOOLE_0:def 3;
end;
end;
thus downarrow(sup X1) /\ Join-IRR L c= X1
proof
let r be Element of L;
assume A20: r in downarrow(sup X1) /\ Join-IRR L;
then A21: r in downarrow(sup X1) & r in Join-IRR L by XBOOLE_0:
def 3;
reconsider r1=r as Element of L;
A22: r1 <= sup X1 by A21,WAYBEL_0:17;
per cases;
suppose r1 in X1;
hence thesis;
suppose
A23: not (r1 in X1);
A24: r1 in Join-IRR L by A20,XBOOLE_0:def 3;
A25: r1 = r1 "/\" sup X1 by A22,YELLOW_0:25;
A26: r1 "/\" sup X1 = sup ({r1} "/\" X1) by WAYBEL_2:15;
consider z be Element of L such that
A27: z < r1 & for y be Element of L st y < r1 holds y <= z
by A24,Th11;
{r1} "/\" X1 is_<=_than z
proof
let a be Element of L;
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 A28: a=r1"/\"x &
x in X1;
A29: ex_inf_of {r1,x},L by YELLOW_0:17;
then A30: a <= r1 by A28,YELLOW_0:19;
A31: a <= x by A28,A29,YELLOW_0:19;
A32: r1 in the carrier of subrelstr Join-IRR L
by A24,YELLOW_0:def 15;
then reconsider r'=r1,x'=x as Element of subrelstr Join-IRR
L
by A28;
now assume a=r1;
then r' <= x' by A31,A32,YELLOW_0:61;
hence contradiction by A16,A23,A28,WAYBEL_0:def 19;
end;
then a < r1 by A30,ORDERS_1:def 10;
hence thesis by A27;
end;
then sup ({r1} "/\" X1) <= z by YELLOW_0:32;
hence thesis by A25,A26,A27,ORDERS_1:32;
end;
end;
hence x=r.y by A1,A16;
end;
hence thesis by FUNCT_1:def 5;
end;
end;
end;
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
A33: 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 A34: a in downarrow x & a in Join-IRR L by XBOOLE_0:def 3;
downarrow x c= downarrow y by A33,WAYBEL_0:21;
hence thesis by A34,XBOOLE_0:def 3;
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
assume
A35: r.x <= r.y;
A36: r.x= downarrow x /\ Join-IRR L by A1;
r.y= downarrow y /\ Join-IRR L by A1;
then reconsider rx = r.x,ry= r.y as Subset of L by A36;
A37: rx c= ry by A35,YELLOW_1:3;
A38: ex_sup_of rx,L by YELLOW_0:17;
ex_sup_of ry,L by YELLOW_0:17;
then sup(rx) <= sup(ry) by A37,A38,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;
then r is isomorphic by A12,A14,WAYBEL_0:66;
hence thesis by A2;
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;
consider r be map of L, InclPoset LOWER(subrelstr Join-IRR L) such that A1:
r is isomorphic &
for a being Element of L holds r.a= downarrow a /\ Join-IRR L by Th13;
thus thesis by A1,WAYBEL_1:def 8;
end;
definition
mode Ring_of_sets means :Def8: it includes_lattice_of it;
existence
proof
consider X be set;
take R = bool X;
let a,b be set;
assume A1: a in R & b in R;
then a /\ b c= X by XBOOLE_1:108;
hence a /\ b in R;
a \/ b c= X by A1,XBOOLE_1:8;
hence a \/ b in R;
end;
end;
definition
cluster non empty Ring_of_sets;
existence
proof
take A={{}};
A includes_lattice_of A
proof
let a,b be set;
assume a in A & b in A;
then a={} & b={} by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
hence thesis by Def8;
end;
end;
Lm2:
for L1,L2 be non empty RelStr
for f be map of L1,L2 holds
f is infs-preserving implies f is meet-preserving
proof
let L1,L2 be non empty RelStr;
let f be map of L1,L2;
assume f is infs-preserving;
then for x,y being Element of L1 holds f preserves_inf_of {x,y}
by WAYBEL_0:def 32;
hence thesis by WAYBEL_0:def 34;
end;
Lm3:
for L1,L2 be non empty RelStr
for f be map of L1,L2 holds
f is sups-preserving implies f is join-preserving
proof
let L1,L2 be non empty RelStr;
let f be map of L1,L2;
assume f is sups-preserving;
then for x,y being Element of L1 holds f preserves_sup_of {x,y}
by WAYBEL_0:def 33;
hence thesis by WAYBEL_0:def 35;
end;
definition
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 LATTICE
proof
A3: InclPoset X is with_infima
proof
for x,y be set st (x in X & y in X) holds x /\ y in
X by A1,COHSP_1:def 8;
hence thesis by YELLOW_1:12;
end;
InclPoset X is with_suprema
proof
for x,y be set st (x in X & y in X) holds x \/ y in
X by A1,COHSP_1:def 8;
hence thesis by YELLOW_1:11;
end;
hence thesis by A3;
end;
InclPoset X is distributive
proof
let x,y,z be Element of InclPoset X;
A4: x /\ (y \/ z) = x /\ y \/ x /\ z by XBOOLE_1:23;
x in the carrier of InclPoset X;
then A5: x in X by YELLOW_1:1;
y in the carrier of InclPoset X;
then A6: y in X by YELLOW_1:1;
z in the carrier of InclPoset X;
then A7: z in X by YELLOW_1:1;
then A8: y \/ z in X by A1,A6,COHSP_1:def 8;
then y \/ z in the carrier of InclPoset X by YELLOW_1:1;
then reconsider r = y \/ z as Element of InclPoset X;
r in the carrier of InclPoset X;
then r in X by YELLOW_1:1;
then x /\ r in X by A1,A5,COHSP_1:def 8;
then x "/\" r = x /\ r by YELLOW_1:9;
then A9: x /\ (y \/ z) = x "/\" (y "\/" z) by A8,YELLOW_1:8;
A10: x /\ y in X by A1,A5,A6,COHSP_1:def 8;
then A11: x /\ y in the carrier of InclPoset X by YELLOW_1:1;
A12: x "/\" y = x /\ y by A10,YELLOW_1:9;
A13: x /\ z in X by A1,A5,A7,COHSP_1:def 8;
then x /\ z in the carrier of InclPoset X by YELLOW_1:1;
then reconsider r1 = x /\ y, r2 = x /\ z as Element of InclPoset X
by A11;
A14: x "/\" z = x /\ z by A13,YELLOW_1:9;
r2 in the carrier of InclPoset X;
then A15: r2 in X by YELLOW_1:1;
r1 in the carrier of InclPoset X;
then r1 in X by YELLOW_1:1;
then r1 \/ r2 in X by A1,A15,COHSP_1:def 8;
hence thesis by A4,A9,A12,A14,YELLOW_1:8;
end;
hence thesis by A2;
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 A1: a in X & b in X;
A2: a /\ b in X
proof
a in {Z where Z is Subset of subrelstr Join-IRR L:Z is lower}
by A1,Def7;
then consider Z be Subset of subrelstr Join-IRR L
such that A3: a=Z & Z is lower;
b in {Z1 where Z1 is Subset of subrelstr Join-IRR L:Z1 is lower}
by A1,Def7;
then consider Z1 be Subset of subrelstr Join-IRR L
such that A4: b=Z1 & Z1 is lower;
Z /\ Z1 is lower by A3,A4,WAYBEL_0:27;
then Z /\ Z1 in {W where W is Subset of subrelstr Join-IRR L:W is
lower};
hence thesis by A3,A4,Def7;
end;
a \/ b in X
proof
a in {Z where Z is Subset of subrelstr Join-IRR L:Z is lower}
by A1,Def7;
then consider Z be Subset of subrelstr Join-IRR L
such that A5: a=Z & Z is lower;
b in {Z1 where Z1 is Subset of subrelstr Join-IRR L:Z1 is lower}
by A1,Def7;
then consider Z1 be Subset of subrelstr Join-IRR L
such that A6: b=Z1 & Z1 is lower;
Z \/ Z1 is lower by A5,A6,WAYBEL_0:27;
then Z \/ Z1 in {W where W is Subset of subrelstr Join-IRR L:W is
lower};
hence thesis by A5,A6,Def7;
end;
hence thesis by A2;
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
assume A1: L is distributive;
consider X be set such that A2: X = LOWER(subrelstr Join-IRR L);
A3: X is Ring_of_sets by A2,Th15;
L,InclPoset X are_isomorphic by A1,A2,Th14;
hence thesis by A2,A3;
end;
given X be non empty Ring_of_sets such that
A4: L, InclPoset X are_isomorphic;
consider f be map of L, InclPoset X such that A5: f is isomorphic
by A4,WAYBEL_1:def 8;
f is infs-preserving by A5,WAYBEL13:20;
then A6: f is meet-preserving by Lm2;
f is sups-preserving by A5,WAYBEL13:20;
then A7: f is join-preserving by Lm3;
f is one-to-one by A5,WAYBEL_0:66;
hence thesis by A6,A7,WAYBEL_6:3;
end;