:: Noetherian Lattices
:: by Christoph Schwarzweller
::
:: Received June 9, 1999
:: Copyright (c) 1999-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 FINSET_1, LATTICES, LATTICE3, XBOOLE_0, STRUCT_0, ZFMISC_1,
SUBSET_1, XXREAL_0, NUMBERS, FINSEQ_1, RELAT_1, ARYTM_3, CARD_1, FUNCT_1,
TARSKI, ORDERS_2, FILTER_1, EQREL_1, PBOOLE, REWRITE1, WELLORD1,
WAYBEL_6, RELAT_2, ZF_LANG, BINOP_1, LATTICE6, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0,
RELAT_1, FUNCT_1, XCMPLX_0, NAT_1, BINOP_1, FINSET_1, WELLORD1, WAYBEL_6,
STRUCT_0, LATTICES, LATTICE3, ORDERS_2, FINSEQ_1, WELLFND1, YELLOW_0,
LATTICE2;
constructors WELLORD1, BINOP_1, REAL_1, REALSET2, LATTICE2, WAYBEL_0,
WAYBEL_6, WELLFND1, RELSET_1, LATTICE3;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XREAL_0, INT_1, FINSEQ_1,
FINSEQ_6, STRUCT_0, LATTICES, ORDERS_2, LATTICE2, LATTICE3, WAYBEL_0,
KNASTER, YELLOW_1, ORDINAL1, CARD_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, WELLFND1, WELLORD1;
expansions TARSKI, WELLFND1, WELLORD1;
theorems TARSKI, FUNCT_1, LATTICES, LATTICE3, ORDERS_2, VECTSP_8, FINSEQ_1,
WAYBEL_6, NAT_1, INT_1, RELAT_1, YELLOW_0, WELLORD1, XBOOLE_0, XXREAL_0,
STRUCT_0, CARD_1, ZFMISC_1;
schemes NAT_1, WELLFND1;
begin
registration
cluster finite for Lattice;
existence
proof
set L = BooleLatt {};
the carrier of L = bool {} by LATTICE3:def 1;
then L is finite;
hence thesis;
end;
end;
Lm1: for L being finite Lattice for X being Subset of L holds X is empty or ex
a being Element of LattPOSet L st a in X & for b being Element of LattPOSet L
st b in X & b <> a holds not b <= a
proof
defpred P[Nat] means for L being finite Lattice for X being
Subset of LattPOSet L for p being FinSequence st rng p = X & len p = $1 holds X
is empty or ex a being Element of LattPOSet L st a in X & for b being Element
of LattPOSet L st b in X & b <> a holds not(b <= a);
let L be finite Lattice;
let X be Subset of L;
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A2: P[k];
per cases;
suppose
A3: k = 0;
for L being finite Lattice for X being Subset of LattPOSet L for p
being FinSequence st rng p = X & len p = 1 holds ex a being Element of
LattPOSet L st a in X & for b being Element of LattPOSet L st b in X & b <> a
holds not b <= a
proof
let L be finite Lattice;
let X be Subset of LattPOSet L;
let p be FinSequence;
assume that
A4: rng p = X and
A5: len p = 1;
consider a being set such that
A6: p.1 = a;
A7: Seg 1 = dom p by A5,FINSEQ_1:def 3;
then 1 in dom p by FINSEQ_1:2,TARSKI:def 1;
then
A8: a in rng p by A6,FUNCT_1:def 3;
then reconsider a as Element of LattPOSet L by A4;
rng p = { a } by A7,A6,FINSEQ_1:2,FUNCT_1:4;
then
for b being Element of LattPOSet L st b in X & b <> a holds not b
<= a by A4,TARSKI:def 1;
hence thesis by A4,A8;
end;
hence thesis by A3;
end;
suppose
A9: k <> 0;
for L being finite Lattice for X being Subset of LattPOSet L for p
being FinSequence st rng p = X & len p = k + 1 holds ex a being Element of
LattPOSet L st a in X & for b being Element of LattPOSet L st b in X & b <> a
holds not b <= a
proof
let L be finite Lattice;
let X be Subset of LattPOSet L;
let p be FinSequence;
assume that
A10: rng p = X and
A11: len p = k + 1;
set q = p|(Seg k), X9 = rng q;
A12: rng q c= rng p by RELAT_1:70;
for x being object
holds x in X9 implies x in the carrier of LattPOSet L
proof
let x be object;
assume x in X9;
then x in rng p by A12;
hence thesis by A10;
end;
then
A13: X9 is Subset of LattPOSet L by TARSKI:def 3;
A14: k <= len p by A11,NAT_1:11;
then len q = k & q <> {} by A9,CARD_1:27,FINSEQ_1:17;
then consider a being Element of LattPOSet L such that
A15: a in X9 and
A16: for b being Element of LattPOSet L st b in X9 & b <> a holds
not b <= a by A2,A13;
consider b being set such that
A17: p.(k+1) = b;
Seg (k+1) = dom p by A11,FINSEQ_1:def 3;
then k + 1 in dom p by FINSEQ_1:4;
then
A18: b in rng p by A17,FUNCT_1:def 3;
then reconsider b as Element of LattPOSet L by A10;
per cases;
suppose
ex c being Element of LattPOSet L st c in X & c <= b & c <> b;
then consider c being Element of LattPOSet L such that
A19: c in X and
A20: c <= b and
A21: c <> b;
for u being Element of LattPOSet L st u in X & u <> a holds not
u <= a
proof
let u be Element of LattPOSet L;
assume that
A22: u in X and
A23: u <> a;
per cases;
suppose
u in X9;
hence thesis by A16,A23;
end;
suppose
A24: not u in X9;
consider n being object such that
A25: n in dom p and
A26: p.n = u by A10,A22,FUNCT_1:def 3;
reconsider n as Element of NAT by A25;
A27: Seg(k+1) = dom p by A11,FINSEQ_1:def 3;
then
A28: n <= k+1 by A25,FINSEQ_1:1;
A29: 1 <= n by A25,A27,FINSEQ_1:1;
A30: n = k + 1
proof
assume n <> k + 1;
then n < k + 1 by A28,XXREAL_0:1;
then n <= k by NAT_1:13;
then n in Seg(k) by A29,FINSEQ_1:1;
then
A31: n in dom q by A14,FINSEQ_1:17;
then q.n = u by A26,FUNCT_1:47;
hence thesis by A24,A31,FUNCT_1:def 3;
end;
A32: c in X9
proof
consider n being object such that
A33: n in dom p and
A34: p.n = c by A10,A19,FUNCT_1:def 3;
reconsider n as Element of NAT by A33;
A35: Seg(k+1) = dom p by A11,FINSEQ_1:def 3;
then n <= k+1 by A33,FINSEQ_1:1;
then n < k + 1 by A17,A21,A34,XXREAL_0:1;
then
A36: n <= k by NAT_1:13;
1 <= n by A33,A35,FINSEQ_1:1;
then n in Seg(k) by A36,FINSEQ_1:1;
then
A37: n in dom q by A14,FINSEQ_1:17;
then q.n = c by A34,FUNCT_1:47;
hence thesis by A37,FUNCT_1:def 3;
end;
assume
A38: u <= a;
then c <> a by A17,A20,A21,A26,A30,ORDERS_2:2;
hence thesis by A16,A17,A20,A26,A30,A38,A32,ORDERS_2:3;
end;
end;
hence thesis by A10,A12,A15;
end;
suppose
not(ex c being Element of LattPOSet L st c in X & c <= b & c <> b);
then
for u being Element of LattPOSet L st u in X & u <> b holds not
u <= b;
hence thesis by A10,A18;
end;
end;
hence thesis;
end;
end;
A39: P[ 0 ]
proof
let L be finite Lattice;
let X be Subset of LattPOSet L;
let p be FinSequence;
assume that
A40: rng p = X and
A41: len p = 0;
Seg 0 = dom p by A41,FINSEQ_1:def 3;
hence thesis by A40,RELAT_1:42;
end;
A42: for k being Nat holds P[k] from NAT_1:sch 2(A39,A1);
reconsider X as finite Subset of L;
LattPOSet L = RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2;
then reconsider X9 = X as finite Subset of LattPOSet L;
consider p being FinSequence such that
A43: rng p = X9 by FINSEQ_1:52;
dom p = Seg len p by FINSEQ_1:def 3;
hence thesis by A42,A43;
end;
Lm2: for L being finite Lattice for X being Subset of L holds X is empty or ex
a being Element of LattPOSet L st a in X & for b being Element of LattPOSet L
st b in X & b <> a holds not a <= b
proof
defpred P[Nat] means for L being finite Lattice for X being
Subset of LattPOSet L for p being FinSequence st rng p = X & len p = $1 holds X
is empty or ex a being Element of LattPOSet L st a in X & for b being Element
of LattPOSet L st b in X & b <> a holds not(a <= b);
let L be finite Lattice;
let X be Subset of L;
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A2: P[k];
per cases;
suppose
A3: k = 0;
for L being finite Lattice for X being Subset of LattPOSet L for p
being FinSequence st rng p = X & len p = 1 holds ex a being Element of
LattPOSet L st a in X & for b being Element of LattPOSet L st b in X & b <> a
holds not a <= b
proof
let L be finite Lattice;
let X be Subset of LattPOSet L;
let p be FinSequence;
assume that
A4: rng p = X and
A5: len p = 1;
consider a being set such that
A6: p.1 = a;
A7: dom p = { 1 } by A5,FINSEQ_1:2,def 3;
then 1 in dom p by TARSKI:def 1;
then
A8: a in rng p by A6,FUNCT_1:def 3;
then reconsider a as Element of LattPOSet L by A4;
rng p = { a } by A7,A6,FUNCT_1:4;
then
for b being Element of LattPOSet L st b in X & b <> a holds not a
<= b by A4,TARSKI:def 1;
hence thesis by A4,A8;
end;
hence thesis by A3;
end;
suppose
A9: k <> 0;
for L being finite Lattice for X being Subset of LattPOSet L for p
being FinSequence st rng p = X & len p = k + 1 holds ex a being Element of
LattPOSet L st a in X & for b being Element of LattPOSet L st b in X & b <> a
holds not a <= b
proof
let L be finite Lattice;
let X be Subset of LattPOSet L;
let p be FinSequence;
assume that
A10: rng p = X and
A11: len p = k + 1;
set q = p|(Seg k), X9 = rng q;
A12: rng q c= rng p by RELAT_1:70;
for x being object
holds x in X9 implies x in the carrier of LattPOSet L
proof
let x be object;
assume x in X9;
then x in rng p by A12;
hence thesis by A10;
end;
then
A13: X9 is Subset of LattPOSet L by TARSKI:def 3;
A14: k <= len p by A11,NAT_1:11;
then len q = k & q <> {} by A9,CARD_1:27,FINSEQ_1:17;
then consider a being Element of LattPOSet L such that
A15: a in X9 and
A16: for b being Element of LattPOSet L st b in X9 & b <> a holds
not a <= b by A2,A13;
consider b being set such that
A17: p.(k+1) = b;
Seg (k+1) = dom p by A11,FINSEQ_1:def 3;
then k + 1 in dom p by FINSEQ_1:4;
then
A18: b in rng p by A17,FUNCT_1:def 3;
then reconsider b as Element of LattPOSet L by A10;
per cases;
suppose
ex c being Element of LattPOSet L st c in X & b <= c & c <> b;
then consider c being Element of LattPOSet L such that
A19: c in X and
A20: b <= c and
A21: c <> b;
for u being Element of LattPOSet L st u in X & u <> a holds not
a <= u
proof
let u be Element of LattPOSet L;
assume that
A22: u in X and
A23: u <> a;
now
per cases;
case
u in X9;
hence thesis by A16,A23;
end;
case
A24: not u in X9;
consider n being object such that
A25: n in dom p and
A26: p.n = u by A10,A22,FUNCT_1:def 3;
reconsider n as Element of NAT by A25;
A27: Seg(k+1) = dom p by A11,FINSEQ_1:def 3;
then
A28: n <= k+1 by A25,FINSEQ_1:1;
A29: 1 <= n by A25,A27,FINSEQ_1:1;
A30: n = k + 1
proof
assume n <> k + 1;
then n < k + 1 by A28,XXREAL_0:1;
then n <= k by NAT_1:13;
then n in Seg(k) by A29,FINSEQ_1:1;
then
A31: n in dom q by A14,FINSEQ_1:17;
then q.n = u by A26,FUNCT_1:47;
hence thesis by A24,A31,FUNCT_1:def 3;
end;
A32: c in X9
proof
consider n being object such that
A33: n in dom p and
A34: p.n = c by A10,A19,FUNCT_1:def 3;
reconsider n as Element of NAT by A33;
A35: Seg(k+1) = dom p by A11,FINSEQ_1:def 3;
then n <= k+1 by A33,FINSEQ_1:1;
then n < k + 1 by A17,A21,A34,XXREAL_0:1;
then
A36: n <= k by NAT_1:13;
1 <= n by A33,A35,FINSEQ_1:1;
then n in Seg(k) by A36,FINSEQ_1:1;
then
A37: n in dom q by A14,FINSEQ_1:17;
then q.n = c by A34,FUNCT_1:47;
hence thesis by A37,FUNCT_1:def 3;
end;
assume a <= u;
then c <> a by A17,A20,A21,A26,A30,ORDERS_2:2;
hence thesis by A16,A17,A20,A26,A30,A32,ORDERS_2:3;
end;
end;
hence thesis;
end;
hence thesis by A10,A12,A15;
end;
suppose
not(ex c being Element of LattPOSet L st c in X & b <= c & c <> b);
then
for u being Element of LattPOSet L st u in X & u <> b holds not
b <= u;
hence thesis by A10,A18;
end;
end;
hence thesis;
end;
end;
A38: P[ 0 ]
proof
let L be finite Lattice;
let X be Subset of LattPOSet L;
let p be FinSequence;
assume that
A39: rng p = X and
A40: len p = 0;
Seg 0 = dom p by A40,FINSEQ_1:def 3;
hence thesis by A39,RELAT_1:42;
end;
A41: for k being Nat holds P[k] from NAT_1:sch 2(A38,A1);
reconsider X as finite Subset of L;
LattPOSet L = RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2;
then reconsider X9 = X as finite Subset of LattPOSet L;
consider p being FinSequence such that
A42: rng p = X9 by FINSEQ_1:52;
dom p = Seg len p by FINSEQ_1:def 3;
hence thesis by A41,A42;
end;
Lm3: for L being finite Lattice for X being Subset of L holds X is empty or ex
a being Element of LattPOSet L st for b being Element of LattPOSet L st b in X
holds b <= a
proof
defpred P[Nat] means for L being finite Lattice for X being
Subset of LattPOSet L for p being FinSequence st rng p = X & len p = $1 holds X
is empty or ex a being Element of LattPOSet L st for b being Element of
LattPOSet L st b in X holds b <= a;
let L be finite Lattice;
let X be Subset of L;
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A2: P[k];
per cases;
suppose
A3: k = 0;
for L being finite Lattice for X being Subset of LattPOSet L for p
being FinSequence st rng p = X & len p = 1 holds ex a being Element of
LattPOSet L st for b being Element of LattPOSet L st b in X holds b <= a
proof
let L be finite Lattice;
let X be Subset of LattPOSet L;
let p be FinSequence;
assume that
A4: rng p = X and
A5: len p = 1;
consider a being set such that
A6: p.1 = a;
A7: Seg 1 = dom p by A5,FINSEQ_1:def 3;
then 1 in dom p by FINSEQ_1:2,TARSKI:def 1;
then a in rng p by A6,FUNCT_1:def 3;
then reconsider a as Element of LattPOSet L by A4;
rng p = { a } by A7,A6,FINSEQ_1:2,FUNCT_1:4;
then for b being Element of LattPOSet L st b in X holds b <= a by A4,
TARSKI:def 1;
hence thesis;
end;
hence thesis by A3;
end;
suppose
A8: k <> 0;
for L being finite Lattice for X being Subset of LattPOSet L for p
being FinSequence st rng p = X & len p = k + 1 holds ex a being Element of
LattPOSet L st for b being Element of LattPOSet L st b in X holds b <= a
proof
let L be finite Lattice;
let X be Subset of LattPOSet L;
let p be FinSequence;
assume that
A9: rng p = X and
A10: len p = k + 1;
consider b being set such that
A11: p.(k+1) = b;
set q = p|(Seg k), X9 = rng q;
for x being object
holds x in X9 implies x in the carrier of LattPOSet L
proof
let x be object;
A12: rng q c= rng p by RELAT_1:70;
assume x in X9;
then x in rng p by A12;
hence thesis by A9;
end;
then
A13: X9 is Subset of LattPOSet L by TARSKI:def 3;
A14: k <= k + 1 by NAT_1:11;
then len q = k & q <> {} by A8,A10,CARD_1:27,FINSEQ_1:17;
then consider a being Element of LattPOSet L such that
A15: for b being Element of LattPOSet L st b in X9 holds b <= a by A2,A13;
Seg (k+1) = dom p by A10,FINSEQ_1:def 3;
then k + 1 in dom p by FINSEQ_1:4;
then b in rng p by A11,FUNCT_1:def 3;
then reconsider b as Element of LattPOSet L by A9;
A16: (%b)% = %b by LATTICE3:def 3
.= b by LATTICE3:def 4;
set a2 = %a "\/" %b;
%a "\/" a2 = (%a "\/" %a) "\/" %b by LATTICES:def 5
.= %a "\/" %b;
then
A17: %a [= a2 by LATTICES:def 3;
%b "\/" a2 = (%b "\/" %b) "\/" %a by LATTICES:def 5
.= %b "\/" %a;
then
A18: %b [= a2 by LATTICES:def 3;
A19: (%a)% = %a by LATTICE3:def 3
.= a by LATTICE3:def 4;
for c being Element of LattPOSet L st c in X holds c <= a2%
proof
let c be Element of LattPOSet L;
assume
A20: c in X;
per cases;
suppose
c in X9;
then
A21: c <= a by A15;
a <= a2% by A17,A19,LATTICE3:7;
hence thesis by A21,ORDERS_2:3;
end;
suppose
A22: not c in X9;
consider n being object such that
A23: n in dom p and
A24: c = p.n by A9,A20,FUNCT_1:def 3;
reconsider n as Element of NAT by A23;
A25: n in Seg(k + 1) by A10,A23,FINSEQ_1:def 3;
A26: n >= k + 1
proof
assume not n >= k + 1;
then
A27: n <= k by INT_1:7;
1 <= n by A25,FINSEQ_1:1;
then
A28: n in Seg(k) by A27,FINSEQ_1:1;
dom(p|(Seg k)) = dom p /\ Seg(k) by RELAT_1:61
.= Seg(k+1) /\ Seg(k) by A10,FINSEQ_1:def 3
.= Seg(k) by FINSEQ_1:7,NAT_1:11;
then
A29: q.n = c by A24,A28,FUNCT_1:47;
n in dom q by A10,A14,A28,FINSEQ_1:17;
hence thesis by A22,A29,FUNCT_1:def 3;
end;
n <= k + 1 by A25,FINSEQ_1:1;
then c = b by A11,A24,A26,XXREAL_0:1;
hence thesis by A18,A16,LATTICE3:7;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
A30: P[ 0 ]
proof
let L be finite Lattice;
let X be Subset of LattPOSet L;
let p be FinSequence;
assume that
A31: rng p = X and
A32: len p = 0;
Seg len p = {} by A32;
then dom p = {} by FINSEQ_1:def 3;
hence thesis by A31,RELAT_1:42;
end;
A33: for k being Nat holds P[k] from NAT_1:sch 2(A30,A1);
reconsider X as finite Subset of L;
LattPOSet L = RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2;
then reconsider X9 = X as finite Subset of LattPOSet L;
consider p being FinSequence such that
A34: rng p = X9 by FINSEQ_1:52;
dom p = Seg len p by FINSEQ_1:def 3;
hence thesis by A33,A34;
end;
Lm4: for L being finite Lattice holds ex a being Element of LattPOSet L st for
b being Element of LattPOSet L holds b <= a
proof
let L be finite Lattice;
the carrier of L c= the carrier of L;
then reconsider L9 = the carrier of L as Subset of L;
consider a being Element of LattPOSet L such that
A1: for b being Element of LattPOSet L st b in L9 holds b <= a by Lm3;
for b being Element of LattPOSet L holds b <= a
proof
let b be Element of LattPOSet L;
LattPOSet L = RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2;
hence thesis by A1;
end;
hence thesis;
end;
Lm5: for L being finite Lattice holds L is complete
proof
let L be finite Lattice;
for X being Subset of L ex a being Element of L st a is_less_than X &
for b being Element of L st b is_less_than X holds b [= a
proof
defpred P[Nat] means for X9 being finite Subset of LattPOSet L
for p being FinSequence st rng p = X9 & len p = $1 holds ex a being Element of
LattPOSet L st (for x being Element of LattPOSet L st x in X9 holds a <= x) & (
for x9 being Element of LattPOSet L st for x being Element of LattPOSet L st x
in X9 holds x9 <= x holds x9 <= a);
let X be Subset of L;
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A2: P[k];
for X9 being finite Subset of LattPOSet L for p being FinSequence
st rng p = X9 & len p = k + 1 holds ex a being Element of LattPOSet L st (for x
being Element of LattPOSet L st x in X9 holds a <= x) & for x9 being Element of
LattPOSet L st for x being Element of LattPOSet L st x in X9 holds x9 <= x
holds x9 <= a
proof
let X be finite Subset of LattPOSet L;
let p be FinSequence;
assume that
A3: rng p = X and
A4: len p = k + 1;
set q = p|(Seg k), X9 = rng q;
for x being object
holds x in X9 implies x in the carrier of LattPOSet L
proof
let x be object;
A5: rng q c= rng p by RELAT_1:70;
assume x in X9;
then x in rng p by A5;
hence thesis by A3;
end;
then
A6: X9 is Subset of LattPOSet L by TARSKI:def 3;
A7: k <= k + 1 by NAT_1:11;
then len q = k by A4,FINSEQ_1:17;
then consider a being Element of LattPOSet L such that
A8: for x being Element of LattPOSet L st x in X9 holds a <= x and
A9: for x9 being Element of LattPOSet L st for x being Element of
LattPOSet L st x in X9 holds x9 <= x holds x9 <= a by A2,A6;
consider b being set such that
A10: p.(k+1) = b;
Seg (k+1) = dom p by A4,FINSEQ_1:def 3;
then k + 1 in dom p by FINSEQ_1:4;
then
A11: b in rng p by A10,FUNCT_1:def 3;
then reconsider b as Element of LattPOSet L by A3;
A12: (%b)% = %b by LATTICE3:def 3
.= b by LATTICE3:def 4;
set a2 = %a "/\" %b;
a2 "\/" %a = %a by LATTICES:def 8;
then
A13: a2 [= %a by LATTICES:def 3;
a2 "\/" %b = %b by LATTICES:def 8;
then
A14: a2 [= %b by LATTICES:def 3;
A15: (%a)% = %a by LATTICE3:def 3
.= a by LATTICE3:def 4;
A16: for x being Element of LattPOSet L st x in X holds a2% <= x
proof
let c be Element of LattPOSet L;
assume
A17: c in X;
per cases;
suppose
c in X9;
then
A18: a <= c by A8;
a2% <= a by A13,A15,LATTICE3:7;
hence thesis by A18,ORDERS_2:3;
end;
suppose
A19: not c in X9;
consider n being object such that
A20: n in dom p and
A21: c = p.n by A3,A17,FUNCT_1:def 3;
reconsider n as Element of NAT by A20;
A22: n in Seg(k + 1) by A4,A20,FINSEQ_1:def 3;
A23: n >= k + 1
proof
assume not n >= k + 1;
then
A24: n <= k by INT_1:7;
1 <= n by A22,FINSEQ_1:1;
then
A25: n in Seg(k) by A24,FINSEQ_1:1;
dom(p|(Seg k)) = dom p /\ Seg(k) by RELAT_1:61
.= Seg(k+1) /\ Seg(k) by A4,FINSEQ_1:def 3
.= Seg(k) by FINSEQ_1:7,NAT_1:11;
then
A26: q.n = c by A21,A25,FUNCT_1:47;
n in dom q by A4,A7,A25,FINSEQ_1:17;
hence thesis by A19,A26,FUNCT_1:def 3;
end;
n <= k + 1 by A22,FINSEQ_1:1;
then c = b by A10,A21,A23,XXREAL_0:1;
hence thesis by A14,A12,LATTICE3:7;
end;
end;
for x9 being Element of LattPOSet L st for x being Element of
LattPOSet L st x in X holds x9 <= x holds x9 <= a2%
proof
let x9 be Element of LattPOSet L;
A27: (%b)% = %b by LATTICE3:def 3
.= b by LATTICE3:def 4;
A28: (%(x9))% = %(x9) by LATTICE3:def 3
.= x9 by LATTICE3:def 4;
assume
A29: for x being Element of LattPOSet L st x in X holds x9 <= x;
for x being Element of LattPOSet L st x in X9 holds x9 <= x
proof
let x be Element of LattPOSet L;
rng q c= rng p by RELAT_1:70;
hence thesis by A3,A29;
end;
then
A30: x9 <= a by A9;
(%a)% = %a by LATTICE3:def 3
.= a by LATTICE3:def 4;
then
A31: %(x9) [= %a by A30,A28,LATTICE3:7;
x9 <= b by A3,A11,A29;
then
A32: %(x9) [= %b by A27,A28,LATTICE3:7;
%(x9) "/\" a2 = (%(x9) "/\" %a) "/\" %b by LATTICES:def 7
.= %(x9) "/\" %b by A31,LATTICES:4
.= %(x9) by A32,LATTICES:4;
then %(x9) [= a2 by LATTICES:4;
hence thesis by A28,LATTICE3:7;
end;
hence thesis by A16;
end;
hence thesis;
end;
for X9 being finite Subset of LattPOSet L for p being FinSequence st
rng p = X9 & len p = 0 holds ex a being Element of LattPOSet L st (for x being
Element of LattPOSet L st x in X9 holds a <= x) & for x9 being Element of
LattPOSet L st for x being Element of LattPOSet L st x in X9 holds x9 <= x
holds x9 <= a
proof
let X9 be finite Subset of LattPOSet L;
let p be FinSequence;
assume that
A33: rng p = X9 and
A34: len p = 0;
Seg len p = {} by A34;
then
A35: dom p = {} by FINSEQ_1:def 3;
ex a being Element of LattPOSet L st (for x being Element of
LattPOSet L st x in X9 holds a <= x) & for x9 being Element of LattPOSet L st
for x being Element of LattPOSet L st x in X9 holds x9 <= x holds x9 <= a
proof
consider a being Element of LattPOSet L such that
A36: for b being Element of LattPOSet L holds b <= a by Lm4;
A37: for x9 being Element of LattPOSet L st for x being Element of
LattPOSet L st x in X9 holds x9 <= x holds x9 <= a by A36;
for x being Element of LattPOSet L st x in X9 holds a <= x by A33,A35,
RELAT_1:42;
hence thesis by A37;
end;
hence thesis;
end;
then
A38: P[ 0 ];
A39: for k being Nat holds P[k] from NAT_1:sch 2(A38,A1);
reconsider X as finite Subset of L;
LattPOSet L = RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2;
then reconsider X9 = X as finite Subset of LattPOSet L;
consider p being FinSequence such that
A40: rng p = X9 by FINSEQ_1:52;
dom p = Seg len p by FINSEQ_1:def 3;
then consider a being Element of LattPOSet L such that
A41: for x being Element of LattPOSet L st x in X9 holds a <= x and
A42: for x9 being Element of LattPOSet L st for x being Element of
LattPOSet L st x in X9 holds x9 <= x holds x9 <= a by A39,A40;
A43: for b being Element of L st b is_less_than X holds b [= %a
proof
let b be Element of L;
assume
A44: b is_less_than X;
for x being Element of LattPOSet L st x in X9 holds b% <= x
proof
let x be Element of LattPOSet L;
assume x in X9;
then consider x9 being Element of L such that
A45: x9 = x and
A46: x9 in X;
b [= x9 by A44,A46,LATTICE3:def 16;
then b% <= (x9)% by LATTICE3:7;
hence thesis by A45,LATTICE3:def 3;
end;
then
A47: b% <= a by A42;
(%a)% = %a by LATTICE3:def 3
.= a by LATTICE3:def 4;
hence thesis by A47,LATTICE3:7;
end;
for x being Element of L st x in X holds %a [= x
proof
let x be Element of L;
A48: (%a)% = %a by LATTICE3:def 3
.= a by LATTICE3:def 4;
assume x in X;
then consider x9 being Element of LattPOSet L such that
A49: x9 = x & x9 in X9;
a <= x9 & x9 = x% by A41,A49,LATTICE3:def 3;
hence thesis by A48,LATTICE3:7;
end;
then %a is_less_than X by LATTICE3:def 16;
hence thesis by A43;
end;
hence thesis by VECTSP_8:def 6;
end;
registration
cluster finite -> complete for Lattice;
coherence by Lm5;
end;
definition
let L be Lattice;
let D be Subset of L;
func D% -> Subset of LattPOSet L equals
{d% where d is Element of L : d in D
};
coherence
proof
set M9 = {d% where d is Element of L : d in D};
for x being object
holds x in M9 implies x in the carrier of LattPOSet L
proof
let x be object;
assume x in M9;
then ex x9 being Element of L st x = x9% & x9 in D;
hence thesis;
end;
hence thesis by TARSKI:def 3;
end;
end;
definition
let L be Lattice;
let D be Subset of LattPOSet L;
func %D -> Subset of L equals
{%d where d is Element of LattPOSet L : d in D
};
coherence
proof
set M9 = {%d where d is Element of LattPOSet L : d in D};
for x being object
holds x in M9 implies x in the carrier of L
proof
let x be object;
assume x in M9;
then ex x9 being Element of LattPOSet L st x = %x9 & x9 in D;
hence thesis;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
let L be finite Lattice;
cluster LattPOSet L -> well_founded;
coherence
proof
let Y be set;
set R = LattPOSet L;
assume that
A1: Y c= the carrier of R and
A2: Y <> {};
LattPOSet L = RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2;
then reconsider Y as Subset of L by A1;
consider a being Element of LattPOSet L such that
A3: a in Y and
A4: for b being Element of LattPOSet L st b in Y & b <> a holds not b
<= a by A2,Lm1;
A5: not(ex x being Element of R st x <> a & [x,a] in the InternalRel of R
& x in Y)
by ORDERS_2:def 5,A4;
(the InternalRel of R)-Seg(a) /\ Y = {}
proof
set z = the Element of (the InternalRel of R)-Seg(a) /\ Y;
assume
A6: (the InternalRel of R)-Seg(a) /\ Y <> {};
then z in (the InternalRel of R)-Seg(a) by XBOOLE_0:def 4;
then
A7: z <> a & [z,a] in (the InternalRel of R) by WELLORD1:1;
z in Y by A6,XBOOLE_0:def 4;
hence thesis by A1,A5,A7;
end;
then (the InternalRel of R)-Seg(a) misses Y by XBOOLE_0:def 7;
hence thesis by A3;
end;
end;
Lm6: for L being finite Lattice holds (LattPOSet L)~ is well_founded
proof
let L be finite Lattice;
set R = LattPOSet L;
A1: (LattPOSet L)~ = RelStr(#the carrier of R, (the InternalRel of R)~#) by
LATTICE3:def 5;
for Y being set st Y c= the carrier of R~ & Y <> {}
ex a being object st a in Y & (the InternalRel of R~)-Seg(a) misses Y
proof
let Y be set;
assume that
A2: Y c= the carrier of R~ and
A3: Y <> {};
LattPOSet L = RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2;
then reconsider Y as Subset of L by A1,A2;
consider a being Element of R such that
A4: a in Y and
A5: for b being Element of LattPOSet L st b in Y & b <> a holds not a
<= b by A3,Lm2;
reconsider a as Element of R;
reconsider a9 = a as Element of R~ by A1;
A6: for b being Element of (LattPOSet L)~ st b in Y & b <> a holds not b <= a9
proof
let b be Element of (LattPOSet L)~;
reconsider b9 = b as Element of R by A1;
assume b in Y & b <> a;
then
A7: not a <= b9 by A5;
a~ = a9 & (b9)~ = b by LATTICE3:def 6;
hence thesis by A7,LATTICE3:9;
end;
A8: not(ex x being Element of R~ st x <> a & [x,a] in the InternalRel of
R~ & x in Y)
by ORDERS_2:def 5,A6;
(the InternalRel of R~)-Seg(a) /\ Y = {}
proof
set z = the Element of (the InternalRel of R~)-Seg(a) /\ Y;
assume
A9: (the InternalRel of R~)-Seg(a) /\ Y <> {};
then z in (the InternalRel of R~)-Seg(a) by XBOOLE_0:def 4;
then
A10: z <> a & [z,a] in (the InternalRel of R~) by WELLORD1:1;
z in Y by A9,XBOOLE_0:def 4;
hence thesis by A2,A8,A10;
end;
then (the InternalRel of R~)-Seg(a) misses Y by XBOOLE_0:def 7;
hence thesis by A4;
end;
then the InternalRel of R~ is_well_founded_in the carrier of R~;
hence thesis;
end;
definition
let L be Lattice;
attr L is noetherian means
:Def3:
LattPOSet L is well_founded;
attr L is co-noetherian means
:Def4:
(LattPOSet L)~ is well_founded;
end;
registration
cluster noetherian upper-bounded lower-bounded complete for Lattice;
existence
proof
set L = the finite Lattice;
take L;
thus thesis;
end;
end;
registration
cluster co-noetherian upper-bounded lower-bounded complete for Lattice;
existence
proof
set L = the finite Lattice;
take L;
(LattPOSet L)~ is well_founded by Lm6;
hence thesis;
end;
end;
theorem
for L being Lattice holds L is noetherian iff L.: is co-noetherian
proof
let L be Lattice;
set R = LattPOSet L;
set Ri = (LattPOSet L)~;
A1: now
A2: (LattPOSet L)~ = LattPOSet (L.:) by LATTICE3:20;
assume L.: is co-noetherian;
then (Ri)~ is well_founded by A2;
then R is well_founded by LATTICE3:8;
hence L is noetherian;
end;
now
assume L is noetherian;
then R is well_founded;
then
A3: (Ri)~ is well_founded by LATTICE3:8;
(LattPOSet L)~ = LattPOSet (L.:) by LATTICE3:20;
hence L.: is co-noetherian by A3;
end;
hence thesis by A1;
end;
Lm7: for L being finite Lattice holds L is noetherian & L is co-noetherian
by Lm6;
registration
cluster finite -> noetherian for Lattice;
coherence;
cluster finite -> co-noetherian for Lattice;
coherence by Lm7;
end;
definition
let L be Lattice;
let a,b be Element of L;
pred a is-upper-neighbour-of b means
a <> b & b [= a & for c being
Element of L holds b [= c & c [= a implies (c = a or c = b);
end;
notation
let L be Lattice;
let a,b be Element of L;
synonym b is-lower-neighbour-of a for a is-upper-neighbour-of b;
end;
theorem Th2:
for L being Lattice for a being Element of L for b,c being
Element of L st b <> c holds ( b is-upper-neighbour-of a & c
is-upper-neighbour-of a implies a = c "/\" b) & ( b is-lower-neighbour-of a & c
is-lower-neighbour-of a implies a = c "\/" b)
proof
let L be Lattice;
let a be Element of L;
let b,c be Element of L;
assume
A1: b <> c;
A2: now
assume that
A3: b is-lower-neighbour-of a and
A4: c is-lower-neighbour-of a;
A5: b [= a by A3;
A6: c [= a by A4;
A7: not b "\/" c = c
proof
assume b "\/" c = c;
then b [= c by LATTICES:def 3;
then c = a or c = b by A3,A6;
hence contradiction by A1,A4;
end;
a = a "\/" a
.= (b "\/" a) "\/" a by A5,LATTICES:def 3
.= (b "\/" a) "\/" (c "\/" a) by A6,LATTICES:def 3
.= b "\/" (a "\/" (a "\/" c)) by LATTICES:def 5
.= b "\/" ((a "\/" a) "\/" c) by LATTICES:def 5
.= b "\/" (a "\/" c)
.= (b "\/" c) "\/" a by LATTICES:def 5;
then
A8: b "\/" c [= a by LATTICES:def 3;
c [= b "\/" c by LATTICES:5;
hence b "\/" c = a by A4,A8,A7;
end;
now
assume that
A9: b is-upper-neighbour-of a and
A10: c is-upper-neighbour-of a;
A11: a [= b by A9;
A12: a [= c by A10;
A13: not b "/\" c = c
proof
assume b "/\" c = c;
then c [= b by LATTICES:4;
then c = a or c = b by A9,A12;
hence contradiction by A1,A10;
end;
a = a "/\" a
.= (b "/\" a) "/\" a by A11,LATTICES:4
.= (b "/\" a) "/\" (c "/\" a) by A12,LATTICES:4
.= b "/\" (a "/\" (c "/\" a)) by LATTICES:def 7
.= b "/\" ((a "/\" a) "/\" c) by LATTICES:def 7
.= b "/\" (a "/\" c)
.= (b "/\" c) "/\" a by LATTICES:def 7;
then
A14: a [= b "/\" c by LATTICES:4;
b "/\" c [= c by LATTICES:6;
hence b "/\" c = a by A10,A14,A13;
end;
hence thesis by A2;
end;
theorem Th3:
for L being noetherian Lattice for a being Element of L for d
being Element of L st a [= d & a <> d holds ex c being Element of L st c [= d &
c is-upper-neighbour-of a
proof
let L be noetherian Lattice;
let a be Element of L;
let d be Element of L;
defpred P[Element of LattPOSet L] means a [= %($1) & a <> %($1) implies ex c
being Element of L st c [= %($1) & c is-upper-neighbour-of a;
A1: %(d%) = d% by LATTICE3:def 4
.= d by LATTICE3:def 3;
A2: for x being Element of LattPOSet L st for y being Element of LattPOSet L
st y <> x & [y,x] in the InternalRel of LattPOSet L holds P[y] holds P[x]
proof
let x be Element of LattPOSet L;
assume
A3: for y being Element of LattPOSet L st y <> x & [y,x] in the
InternalRel of LattPOSet L holds P[y];
a [= %x & a <> %x implies ex c being Element of L st c [= %x & c
is-upper-neighbour-of a
proof
A4: (%x)% = %x by LATTICE3:def 3
.= x by LATTICE3:def 4;
assume
A5: a [= %x & a <> %x;
per cases;
suppose
%x is-upper-neighbour-of a;
hence thesis;
end;
suppose
not %x is-upper-neighbour-of a;
then consider c being Element of L such that
A6: a [= c and
A7: c [= %x and
A8: ( not c = %x)& not c = a by A5;
c% <= x by A4,A7,LATTICE3:7;
then
A9: [c%,x] in the InternalRel of LattPOSet L by ORDERS_2:def 5;
%(c%) = c% by LATTICE3:def 4
.= c by LATTICE3:def 3;
then ex c9 being Element of L st c9 [= c & c9 is-upper-neighbour-of a
by A3,A6,A8,A9;
hence thesis by A7,LATTICES:7;
end;
end;
hence thesis;
end;
A10: LattPOSet L is well_founded by Def3;
A11: for x being Element of LattPOSet L holds P[x] from WELLFND1:sch 3(A2,
A10);
assume a [= d & a <> d;
hence thesis by A11,A1;
end;
theorem Th4:
for L being co-noetherian Lattice for a being Element of L for d
being Element of L st d [= a & a <> d holds ex c being Element of L st d [= c &
c is-lower-neighbour-of a
proof
let L be co-noetherian Lattice;
let a be Element of L;
let d be Element of L;
defpred P[Element of (LattPOSet L)~] means %(~($1)) [= a & a <> %(~($1))
implies ex c being Element of L st %(~($1)) [= c & c is-lower-neighbour-of a;
A1: %(~((d%)~)) = ~((d%)~) by LATTICE3:def 4
.= (d%)~ by LATTICE3:def 7
.= d% by LATTICE3:def 6
.= d by LATTICE3:def 3;
A2: for x being Element of (LattPOSet L)~ st for y being Element of (
LattPOSet L)~ st y <> x & [y,x] in the InternalRel of (LattPOSet L)~ holds P[y]
holds P[x]
proof
let x be Element of (LattPOSet L)~;
assume
A3: for y being Element of (LattPOSet L)~ st y <> x & [y,x] in the
InternalRel of (LattPOSet L)~ holds P[y];
%(~x) [= a & a <> %(~x) implies ex c being Element of L st %(~x) [= c
& c is-lower-neighbour-of a
proof
A4: (~x)~ = ~x by LATTICE3:def 6
.= x by LATTICE3:def 7;
A5: (%(~x))% = %(~x) by LATTICE3:def 3
.= ~x by LATTICE3:def 4;
assume
A6: %(~x) [= a & a <> %(~x);
per cases;
suppose
%(~x) is-lower-neighbour-of a;
hence thesis;
end;
suppose
not %(~x) is-lower-neighbour-of a;
then consider c being Element of L such that
A7: %(~x) [= c and
A8: c [= a & not c = a & not c = %(~x) by A6;
A9: %(~((c%)~)) = ~((c%)~) by LATTICE3:def 4
.= (c%)~ by LATTICE3:def 7
.= c% by LATTICE3:def 6
.= c by LATTICE3:def 3;
~x <= c% by A5,A7,LATTICE3:7;
then (c%)~ <= x by A4,LATTICE3:9;
then [(c%)~,x] in the InternalRel of (LattPOSet L)~ by ORDERS_2:def 5;
then ex c9 being Element of L st %(~((c%)~)) [= c9 & c9
is-lower-neighbour-of a by A3,A8,A9;
hence thesis by A7,A9,LATTICES:7;
end;
end;
hence thesis;
end;
A10: (LattPOSet L)~ is well_founded by Def4;
A11: for x being Element of (LattPOSet L)~ holds P[x] from WELLFND1:sch 3 (
A2,A10);
assume d [= a & a <> d;
hence thesis by A11,A1;
end;
theorem Th5:
for L being upper-bounded Lattice holds not(ex b being Element of
L st b is-upper-neighbour-of Top L)
proof
let L be upper-bounded Lattice;
given b being Element of L such that
A1: b is-upper-neighbour-of Top L;
A2: b [= Top L by LATTICES:19;
Top L [= b & Top L <> b by A1;
hence thesis by A2,LATTICES:8;
end;
theorem Th6:
for L being noetherian upper-bounded Lattice for a being Element
of L holds a = Top L iff not(ex b being Element of L st b is-upper-neighbour-of
a)
proof
let L be noetherian upper-bounded Lattice;
let a be Element of L;
now
assume
A1: not(ex b being Element of L st b is-upper-neighbour-of a);
for b being Element of L holds a "\/" b = a & b "\/" a = a
proof
let b be Element of L;
consider c being Element of L such that
A2: c = a "\/" b;
A3: a [= c by A2,LATTICES:5;
per cases;
suppose
a <> c;
then ex d being Element of L st d [= c & d is-upper-neighbour-of a by
A3,Th3;
hence thesis by A1;
end;
suppose
a = c;
hence thesis by A2;
end;
end;
hence a = Top L by LATTICES:def 17;
end;
hence thesis by Th5;
end;
theorem Th7:
for L being lower-bounded Lattice holds not(ex b being Element of
L st b is-lower-neighbour-of Bottom L)
proof
let L be lower-bounded Lattice;
given b being Element of L such that
A1: b is-lower-neighbour-of Bottom L;
A2: Bottom L [= b by LATTICES:16;
b [= Bottom L & b <> Bottom L by A1;
hence thesis by A2,LATTICES:8;
end;
theorem Th8:
for L being co-noetherian lower-bounded Lattice for a being
Element of L holds a = Bottom L iff not(ex b being Element of L st b
is-lower-neighbour-of a)
proof
let L be co-noetherian lower-bounded Lattice;
let a be Element of L;
now
assume
A1: not(ex b being Element of L st b is-lower-neighbour-of a);
for b being Element of L holds a "/\" b = a & b "/\" a = a
proof
let b be Element of L;
consider c being Element of L such that
A2: c = a "/\" b;
A3: c [= a by A2,LATTICES:6;
per cases;
suppose
a <> c;
then ex d being Element of L st c [= d & d is-lower-neighbour-of a by
A3,Th4;
hence thesis by A1;
end;
suppose
a = c;
hence thesis by A2;
end;
end;
hence a = Bottom L by LATTICES:def 16;
end;
hence thesis by Th7;
end;
definition
let L be complete Lattice;
let a be Element of L;
func a*' -> Element of L equals
"/\"({d where d is Element of L : a [= d & d
<> a},L);
correctness;
func *'a -> Element of L equals
"\/"({d where d is Element of L : d [= a & d
<> a},L);
correctness;
end;
definition
let L be complete Lattice;
let a be Element of L;
attr a is completely-meet-irreducible means
a*' <> a;
attr a is completely-join-irreducible means
*'a <> a;
end;
theorem Th9:
for L being complete Lattice for a being Element of L holds a [=
a*' & *'a [= a
proof
let L be complete Lattice;
let a be Element of L;
set X = {d where d is Element of L : a [= d & d <> a};
for q being Element of L st q in X holds a [= q
proof
let q be Element of L;
assume q in X;
then ex q9 being Element of L st q9 = q & a [= q9 & q9 <> a;
hence thesis;
end;
then
A1: a is_less_than X by LATTICE3:def 16;
set X = {d where d is Element of L : d [= a & d <> a};
for q being Element of L st q in X holds q [= a
proof
let q be Element of L;
assume q in X;
then ex q9 being Element of L st q9 = q & q9 [= a & q9 <> a;
hence thesis;
end;
then X is_less_than a by LATTICE3:def 17;
hence thesis by A1,LATTICE3:34,def 21;
end;
theorem
for L being complete Lattice holds Top L*' = Top L & (Top L)% is
meet-irreducible
proof
let L be complete Lattice;
set X = {d where d is Element of L : Top L [= d & d <> Top L};
A1: X = {}
proof
assume X <> {};
then reconsider X as non empty set;
set x = the Element of X;
x in X;
then consider x9 being Element of L such that
x9 = x and
A2: Top L [= x9 & x9 <> Top L;
x9 [= Top L by LATTICES:19;
hence thesis by A2,LATTICES:8;
end;
A3: for b being Element of L st b is_less_than {} holds b [= Top L by
LATTICES:19;
for q being Element of L st q in {} holds Top L [= q;
then
A4: Top L is_less_than {} by LATTICE3:def 16;
Top (LattPOSet L) = "/\"({},LattPOSet L) by YELLOW_0:def 12
.= "/\"({},L) by YELLOW_0:29
.= Top L by A4,A3,LATTICE3:34;
then (Top L)% = Top (LattPOSet L) by LATTICE3:def 3;
hence thesis by A1,A4,A3,LATTICE3:34,WAYBEL_6:10;
end;
theorem
for L being complete Lattice holds *'Bottom L = Bottom L & (Bottom L)%
is join-irreducible
proof
let L be complete Lattice;
set X = {d where d is Element of L : d [= Bottom L & d <> Bottom L};
A1: X = {}
proof
assume X <> {};
then reconsider X as non empty set;
set x = the Element of X;
x in X;
then consider x9 being Element of L such that
x9 = x and
A2: x9 [= Bottom L & x9 <> Bottom L;
Bottom L [= x9 by LATTICES:16;
hence thesis by A2,LATTICES:8;
end;
A3: for b being Element of L st b is_greater_than {} holds Bottom L [= b by
LATTICES:16;
A4: for x,y being Element of LattPOSet L st Bottom (LattPOSet L) = x "\/" y
holds x = Bottom (LattPOSet L) or y = Bottom (LattPOSet L)
proof
reconsider L9 = LattPOSet L as lower-bounded antisymmetric non empty
RelStr;
let x,y be Element of LattPOSet L;
reconsider x9 = x as Element of L9;
reconsider y9 = y as Element of L9;
assume Bottom (LattPOSet L) = x "\/" y;
then
A5: Bottom (LattPOSet L) >= x & Bottom (LattPOSet L) >= y by YELLOW_0:22;
x9 >= Bottom (L9) or y9 >= Bottom (L9) by YELLOW_0:44;
hence thesis by A5,ORDERS_2:2;
end;
for q being Element of L st q in {} holds q [= Bottom L;
then
A6: Bottom L is_greater_than {} by LATTICE3:def 17;
Bottom (LattPOSet L) = "\/"({},LattPOSet L) by YELLOW_0:def 11
.= "\/"({},L) by YELLOW_0:29
.= Bottom L by A6,A3,LATTICE3:def 21;
then (Bottom L)% = Bottom (LattPOSet L) by LATTICE3:def 3;
hence thesis by A1,A6,A3,A4,LATTICE3:def 21,WAYBEL_6:def 3;
end;
theorem Th12:
for L being complete Lattice for a being Element of L st a is
completely-meet-irreducible holds a*' is-upper-neighbour-of a & for c being
Element of L holds c is-upper-neighbour-of a implies c = a*'
proof
let L be complete Lattice;
let a be Element of L;
set X = { x where x is Element of L : a [= x & x <> a};
for c being Element of L st a [= c & c [= a*' holds c = a or c = a*'
proof
let c be Element of L;
assume that
A1: a [= c and
A2: c [= a*';
assume c <> a;
then c in X by A1;
then a*' [= c by LATTICE3:38;
hence thesis by A2,LATTICES:8;
end;
then
A3: for c being Element of L holds a [= c & c [= a*' implies (c = a*' or c
= a);
assume a is completely-meet-irreducible;
then
A4: a*' <> a;
A5: for c being Element of L holds c is-upper-neighbour-of a implies c = a *'
proof
let c be Element of L;
assume
A6: c is-upper-neighbour-of a;
then a <> c & a [= c;
then c in X;
then
A7: a*' [= c by LATTICE3:38;
a [= a*' by Th9;
hence thesis by A4,A6,A7;
end;
a [= a*' by Th9;
hence thesis by A4,A3,A5;
end;
theorem Th13:
for L being complete Lattice for a being Element of L st a is
completely-join-irreducible holds *'a is-lower-neighbour-of a & for c being
Element of L holds c is-lower-neighbour-of a implies c = *'a
proof
let L be complete Lattice;
let a be Element of L;
set X = { x where x is Element of L : x [= a & x <> a};
A1: for c being Element of L st *'a [= c & c [= a holds c = a or c = *'a
proof
let c be Element of L;
assume that
A2: *'a [= c and
A3: c [= a;
assume c <> a;
then c in X by A3;
then c [= *'a by LATTICE3:38;
hence thesis by A2,LATTICES:8;
end;
assume a is completely-join-irreducible;
then
A4: *'a <> a;
A5: for c being Element of L holds c is-lower-neighbour-of a implies c = *' a
proof
let c be Element of L;
assume
A6: c is-lower-neighbour-of a;
then a <> c & c [= a;
then c in X;
then
A7: c [= *'a by LATTICE3:38;
*'a [= a by Th9;
hence thesis by A4,A6,A7;
end;
*'a [= a by Th9;
hence thesis by A4,A1,A5;
end;
theorem Th14:
for L being noetherian complete Lattice for a being Element of L
holds a is completely-meet-irreducible iff ex b being Element of L st b
is-upper-neighbour-of a & for c being Element of L holds c
is-upper-neighbour-of a implies c = b
proof
let L be noetherian complete Lattice;
let a be Element of L;
set X = { x where x is Element of L : a [= x & x <> a};
hereby
assume a is completely-meet-irreducible;
then a*' is-upper-neighbour-of a & for c being Element of L holds c
is-upper-neighbour-of a implies c = a*' by Th12;
hence ex b being Element of L st b is-upper-neighbour-of a & for c being
Element of L holds c is-upper-neighbour-of a implies c = b;
end;
given b being Element of L such that
A1: b is-upper-neighbour-of a and
A2: for c being Element of L holds c is-upper-neighbour-of a implies c = b;
A3: a <> b by A1;
for q being Element of L st q in X holds b [= q
proof
let q be Element of L;
assume q in X;
then ex q9 being Element of L st q9 = q & a [= q9 & q9 <> a;
then ex c being Element of L st c [= q & c is-upper-neighbour-of a by Th3;
hence thesis by A2;
end;
then
A4: b is_less_than X by LATTICE3:def 16;
a [= b by A1;
then b in X by A3;
hence a <> a*' by A3,A4,LATTICE3:41;
end;
theorem Th15:
for L being co-noetherian complete Lattice for a being Element
of L holds a is completely-join-irreducible iff ex b being Element of L st b
is-lower-neighbour-of a & for c being Element of L holds c
is-lower-neighbour-of a implies c = b
proof
let L be co-noetherian complete Lattice;
let a be Element of L;
set X = { x where x is Element of L : x [= a & x <> a};
A1: now
given b being Element of L such that
A2: b is-lower-neighbour-of a and
A3: for c being Element of L holds c is-lower-neighbour-of a implies c = b;
A4: a <> b by A2;
for q being Element of L st q in X holds q [= b
proof
let q be Element of L;
assume q in X;
then ex q9 being Element of L st q9 = q & q9 [= a & q9 <> a;
then ex c being Element of L st q [= c & c is-lower-neighbour-of a by Th4
;
hence thesis by A3;
end;
then
A5: b is_greater_than X by LATTICE3:def 17;
b [= a by A2;
then b in X by A4;
then a <> *'a by A4,A5,LATTICE3:40;
hence a is completely-join-irreducible;
end;
now
assume a is completely-join-irreducible;
then *'a is-lower-neighbour-of a & for c being Element of L holds c
is-lower-neighbour-of a implies c = *'a by Th13;
hence ex b being Element of L st b is-lower-neighbour-of a & for c being
Element of L holds c is-lower-neighbour-of a implies c = b;
end;
hence thesis by A1;
end;
theorem Th16:
for L being complete Lattice for a being Element of L holds a is
completely-meet-irreducible implies a% is meet-irreducible
proof
let L be complete Lattice;
let a be Element of L;
set X = {d where d is Element of L : a [= d & d <> a};
assume a is completely-meet-irreducible;
then
A1: a <> a*';
for x,y being Element of LattPOSet L st a% = x "/\" y holds x = a% or y = a%
proof
a [= a*' by Th9;
then
A2: a% <= (a*')% by LATTICE3:7;
A3: %(a%) = a% by LATTICE3:def 4;
A4: a = a% & a*' = (a*')% by LATTICE3:def 3;
A5: a*' is_less_than X by LATTICE3:34;
let x,y be Element of LattPOSet L;
A6: a = a% by LATTICE3:def 3
.= %(a%) by LATTICE3:def 4;
A7: x = %x by LATTICE3:def 4
.= (%x)% by LATTICE3:def 3;
assume
A8: a% = x "/\" y;
then a% <= x by YELLOW_0:23;
then
A9: a [= %x by A7,LATTICE3:7;
assume that
A10: x <> a% and
A11: y <> a%;
A12: y = %y by LATTICE3:def 4
.= (%y)% by LATTICE3:def 3;
a% <= y by A8,YELLOW_0:23;
then
A13: a [= %y by A12,LATTICE3:7;
y = %y by LATTICE3:def 4;
then %y in X by A6,A13,A3,A11;
then a*' [= %y by A5,LATTICE3:def 16;
then
A14: (a*')% <= (%y)% by LATTICE3:7;
x = %x by LATTICE3:def 4;
then %x in X by A6,A9,A3,A10;
then a*' [= %x by A5,LATTICE3:def 16;
then (a*')% <= (%x)% by LATTICE3:7;
then (a*')% <= a% by A8,A12,A7,A14,YELLOW_0:23;
hence contradiction by A1,A2,A4,ORDERS_2:2;
end;
hence thesis by WAYBEL_6:def 2;
end;
Lm8: for L being Lattice for a,b being Element of L holds a "/\" b = a% "/\" b
% & a "\/" b = a% "\/" b%
proof
let L be Lattice;
let a,b be Element of L;
consider c being Element of L such that
A1: c = a "/\" b;
A2: for d being Element of LattPOSet L st d <= a% & d <= b% holds c% >= d
proof
let d be Element of LattPOSet L;
assume that
A3: d <= a% and
A4: d <= b%;
A5: (%d)% = %d by LATTICE3:def 3
.= d by LATTICE3:def 4;
then
A6: %d [= a by A3,LATTICE3:7;
A7: %d [= b by A4,A5,LATTICE3:7;
%d "/\" c = (%d "/\" a) "/\" b by A1,LATTICES:def 7
.= %d "/\" b by A6,LATTICES:4
.= %d by A7,LATTICES:4;
then %d [= c by LATTICES:4;
hence thesis by A5,LATTICE3:7;
end;
c [= b by A1,LATTICES:6;
then
A8: c% <= b% by LATTICE3:7;
c [= a by A1,LATTICES:6;
then c% <= a% by LATTICE3:7;
then
A9: c% = a% "/\" b% by A8,A2,YELLOW_0:23;
consider c being Element of L such that
A10: c = a "\/" b;
A11: for d being Element of LattPOSet L st a% <= d & b% <= d holds d >= c%
proof
let d be Element of LattPOSet L;
assume that
A12: a% <= d and
A13: b% <= d;
A14: (%d)% = %d by LATTICE3:def 3
.= d by LATTICE3:def 4;
then
A15: a [= %d by A12,LATTICE3:7;
A16: b [= %d by A13,A14,LATTICE3:7;
%d "\/" c = (%d "\/" a) "\/" b by A10,LATTICES:def 5
.= %d "\/" b by A15,LATTICES:def 3
.= %d by A16,LATTICES:def 3;
then c [= %d by LATTICES:def 3;
hence thesis by A14,LATTICE3:7;
end;
b [= c by A10,LATTICES:5;
then
A17: b% <= c% by LATTICE3:7;
a [= c by A10,LATTICES:5;
then a% <= c% by LATTICE3:7;
then c% = a% "\/" b% by A17,A11,YELLOW_0:22;
hence thesis by A1,A9,A10,LATTICE3:def 3;
end;
theorem Th17:
for L being complete noetherian Lattice for a being Element of L
st a <> Top L holds a is completely-meet-irreducible iff a% is meet-irreducible
proof
let L be complete noetherian Lattice;
let a be Element of L;
assume a <> Top L;
then consider b being Element of L such that
A1: b is-upper-neighbour-of a by Th6;
A2: b <> a by A1;
now
assume
A3: a% is meet-irreducible;
for d being Element of L holds d is-upper-neighbour-of a implies d = b
proof
let d be Element of L;
A4: a% = a by LATTICE3:def 3;
A5: d% = d & b% = b by LATTICE3:def 3;
assume
A6: d is-upper-neighbour-of a;
then
A7: d <> a;
assume d <> b;
then a = d "/\" b by A1,A6,Th2;
then a% = d% "/\" b% by A4,Lm8;
hence thesis by A2,A3,A7,A4,A5,WAYBEL_6:def 2;
end;
hence a is completely-meet-irreducible by A1,Th14;
end;
hence thesis by Th16;
end;
theorem Th18:
for L being complete Lattice for a being Element of L holds a is
completely-join-irreducible implies a% is join-irreducible
proof
let L be complete Lattice;
let a be Element of L;
set X = {d where d is Element of L : d [= a & d <> a};
assume a is completely-join-irreducible;
then
A1: a <> *'a;
for x,y being Element of LattPOSet L st a% = x "\/" y holds x = a% or y = a%
proof
*'a [= a by Th9;
then
A2: a% >= (*'a)% by LATTICE3:7;
A3: %(a%) = a% by LATTICE3:def 4;
A4: a = a% & *'a = (*'a)% by LATTICE3:def 3;
A5: X is_less_than *'a by LATTICE3:def 21;
let x,y be Element of LattPOSet L;
A6: a = a% by LATTICE3:def 3
.= %(a%) by LATTICE3:def 4;
A7: x = %x by LATTICE3:def 4
.= (%x)% by LATTICE3:def 3;
assume
A8: a% = x "\/" y;
then x <= a% by YELLOW_0:22;
then
A9: %x [= a by A7,LATTICE3:7;
assume that
A10: x <> a% and
A11: y <> a%;
A12: y = %y by LATTICE3:def 4
.= (%y)% by LATTICE3:def 3;
y <= a% by A8,YELLOW_0:22;
then
A13: %y [= a by A12,LATTICE3:7;
y = %y by LATTICE3:def 4;
then %y in X by A6,A13,A3,A11;
then %y [= *'a by A5,LATTICE3:def 17;
then
A14: (*'a)% >= y by A12,LATTICE3:7;
x = %x by LATTICE3:def 4;
then %x in X by A6,A9,A3,A10;
then %x [= *'a by A5,LATTICE3:def 17;
then (*'a)% >= x by A7,LATTICE3:7;
then (*'a)% >= a% by A8,A14,YELLOW_0:22;
hence contradiction by A1,A2,A4,ORDERS_2:2;
end;
hence thesis by WAYBEL_6:def 3;
end;
theorem Th19:
for L being complete co-noetherian Lattice for a being Element
of L st a <> Bottom L holds a is completely-join-irreducible iff a% is
join-irreducible
proof
let L be complete co-noetherian Lattice;
let a be Element of L;
assume a <> Bottom L;
then consider b being Element of L such that
A1: b is-lower-neighbour-of a by Th8;
A2: a <> b by A1;
now
assume
A3: a% is join-irreducible;
for d being Element of L holds d is-lower-neighbour-of a implies d = b
proof
let d be Element of L;
A4: a% = a by LATTICE3:def 3;
A5: d% = d & b% = b by LATTICE3:def 3;
assume
A6: d is-lower-neighbour-of a;
then
A7: a <> d;
assume d <> b;
then a = d "\/" b by A1,A6,Th2;
then a% = d% "\/" b% by A4,Lm8;
hence thesis by A2,A3,A7,A4,A5,WAYBEL_6:def 3;
end;
hence a is completely-join-irreducible by A1,Th15;
end;
hence thesis by Th18;
end;
theorem
for L being finite Lattice for a being Element of L st a <> Bottom L &
a <> Top L holds (a is completely-meet-irreducible iff a% is meet-irreducible)
& (a is completely-join-irreducible iff a% is join-irreducible) by Th17,Th19;
definition
let L be Lattice;
let a be Element of L;
attr a is atomic means
a is-upper-neighbour-of Bottom L;
attr a is co-atomic means
a is-lower-neighbour-of Top L;
end;
theorem
for L being complete Lattice for a being Element of L st a is atomic
holds a is completely-join-irreducible
proof
let L be complete Lattice;
let a be Element of L;
set X = { x where x is Element of L : x [= a & x <> a};
assume a is atomic;
then
A1: a is-upper-neighbour-of Bottom L;
then
A2: a <> Bottom L;
A3: for x being object holds x in X implies x in {Bottom L}
proof
let x be object;
assume x in X;
then
A4: ex x9 being Element of L st x9 = x & x9 [= a & x9 <> a;
then reconsider x as Element of L;
Bottom L [= x by LATTICES:16;
then x = Bottom L by A1,A4;
hence thesis by TARSKI:def 1;
end;
A5: Bottom L [= a by A1;
A6: for x being object holds x in {Bottom L} implies x in X
proof
let x be object;
assume x in {Bottom L};
then x = Bottom L by TARSKI:def 1;
hence thesis by A2,A5;
end;
Bottom L = "\/"({Bottom L},L) by LATTICE3:42
.= *'a by A3,A6,TARSKI:2;
hence thesis by A2;
end;
theorem
for L being complete Lattice for a being Element of L st a is
co-atomic holds a is completely-meet-irreducible
proof
let L be complete Lattice;
let a be Element of L;
set X = { x where x is Element of L : a [= x & x <> a};
assume a is co-atomic;
then
A1: a is-lower-neighbour-of Top L;
then
A2: a <> Top L;
A3: for x being object holds x in X implies x in {Top L}
proof
let x be object;
assume x in X;
then
A4: ex x9 being Element of L st x9 = x & a [= x9 & x9 <> a;
then reconsider x as Element of L;
x [= Top L by LATTICES:19;
then x = Top L by A1,A4;
hence thesis by TARSKI:def 1;
end;
A5: a [= Top L by A1;
A6: for x being object holds x in {Top L} implies x in X
proof
let x be object;
assume x in {Top L};
then x = Top L by TARSKI:def 1;
hence thesis by A2,A5;
end;
Top L = "/\"({Top L},L) by LATTICE3:42
.= a*' by A3,A6,TARSKI:2;
hence thesis by A2;
end;
definition
let L be Lattice;
attr L is atomic means
for a being Element of L holds ex X being
Subset of L st (for x being Element of L st x in X holds x is atomic) & a =
"\/"(X,L);
end;
registration
cluster strict 1-element for Lattice;
existence
proof
set X = {{}};
set XJ = the BinOp of X;
reconsider L = LattStr(#X,XJ,XJ#) as non empty LattStr;
A1: L is trivial;
then
A2: ( for a,b being Element of L holds (a"/\"b)"\/"b = b)& for a,b being
Element of L holds a"/\"b = b"/\"a by STRUCT_0:def 10;
A3: ( for a,b,c being Element of L holds a"/\"(b"/\"c) = (a"/\"b)"/\"c)&
for a,b being Element of L holds a"/\"(a"\/"b)=a by A1,STRUCT_0:def 10;
( for a,b being Element of L holds a"\/"b = b"\/"a)& for a,b,c being
Element of L holds a"\/"(b"\/"c) = (a"\/"b)"\/"c by A1,STRUCT_0:def 10;
then
L is join-commutative join-associative meet-absorbing meet-commutative
meet-associative join-absorbing by A2,A3,LATTICES:def 4,def 5,def 6,def 7
,def 8,def 9;
then reconsider L as Lattice;
take L;
thus thesis by STRUCT_0:def 19;
end;
end;
registration
cluster atomic complete for Lattice;
existence
proof
set L = the strict 1-element Lattice;
consider x being object such that
A1: the carrier of L = {x} by ZFMISC_1:131;
reconsider x as Element of L by A1,TARSKI:def 1;
reconsider L as complete Lattice;
for a being Element of L holds ex X being Subset of L st (for u being
Element of L st u in X holds u is atomic) & a = "\/"(X,L)
proof
let a be Element of L;
for u being object holds u in {} implies u in the carrier of L;
then
A2: ( for u being Element of L st u in {} holds u is atomic)& {} is Subset
of L by TARSKI:def 3;
a = x & x = "\/"({},L) by A1,TARSKI:def 1;
hence thesis by A2;
end;
then L is atomic;
hence thesis;
end;
end;
definition
let L be complete Lattice;
let D be Subset of L;
attr D is supremum-dense means
for a being Element of L holds ex D9 being Subset of D st a = "\/"(D9,L);
attr D is infimum-dense means
for a being Element of L holds ex D9 being Subset of D st a = "/\"(D9,L);
end;
theorem Th23:
for L being complete Lattice for D being Subset of L holds D is
supremum-dense iff for a being Element of L holds a = "\/"({d where d is
Element of L: d in D & d [= a},L)
proof
let L be complete Lattice;
let D be Subset of L;
A1: now
assume
A2: D is supremum-dense;
thus for a being Element of L holds a = "\/"({d where d is Element of L: d
in D & d [= a},L)
proof
let a be Element of L;
set X = {d where d is Element of L: d in D & d [= a};
consider D9 being Subset of D such that
A3: a = "\/"(D9,L) by A2;
for x being object holds x in D9 implies x in X
proof
let x be object;
assume
A4: x in D9;
then x in D;
then reconsider x as Element of L;
D9 is_less_than a by A3,LATTICE3:def 21;
then x [= a by A4,LATTICE3:def 17;
hence thesis by A4;
end;
then D9 c= X;
then
A5: a [= "\/"(X,L) by A3,LATTICE3:45;
for q being Element of L st q in X holds q [= a
proof
let q be Element of L;
assume q in X;
then ex q9 being Element of L st q9 = q & q9 in D & q9 [= a;
hence thesis;
end;
then X is_less_than a by LATTICE3:def 17;
then "\/"(X,L) [= a by LATTICE3:def 21;
hence thesis by A5,LATTICES:8;
end;
end;
now
assume
A6: for a being Element of L holds a = "\/"({d where d is Element of
L: d in D & d [= a},L);
for a being Element of L holds ex D9 being Subset of D st a = "\/"(D9 ,L)
proof
let a be Element of L;
set X = {d where d is Element of L: d in D & d [= a};
for x being object holds x in X implies x in D
proof
let x be object;
assume x in X;
then ex x9 being Element of L st x9 = x & x9 in D & x9 [= a;
hence thesis;
end;
then
A7: X is Subset of D by TARSKI:def 3;
a = "\/"(X,L) by A6;
hence thesis by A7;
end;
hence D is supremum-dense;
end;
hence thesis by A1;
end;
theorem Th24:
for L being complete Lattice for D being Subset of L holds D is
infimum-dense iff for a being Element of L holds a = "/\"({d where d is Element
of L : d in D & a [= d},L)
proof
let L be complete Lattice;
let D be Subset of L;
A1: now
assume
A2: D is infimum-dense;
thus for a being Element of L holds a = "/\"({d where d is Element of L: d
in D & a [= d},L)
proof
let a be Element of L;
set X = {d where d is Element of L: d in D & a [= d};
consider D9 being Subset of D such that
A3: a = "/\"(D9,L) by A2;
for x being object holds x in D9 implies x in X
proof
let x be object;
assume
A4: x in D9;
then x in D;
then reconsider x as Element of L;
a is_less_than D9 by A3,LATTICE3:34;
then a [= x by A4,LATTICE3:def 16;
hence thesis by A4;
end;
then D9 c= X;
then
A5: "/\"(X,L) [= a by A3,LATTICE3:45;
for q being Element of L st q in X holds a [= q
proof
let q be Element of L;
assume q in X;
then ex q9 being Element of L st q9 = q & q9 in D & a [= q9;
hence thesis;
end;
then a is_less_than X by LATTICE3:def 16;
then a [= "/\"(X,L) by LATTICE3:39;
hence thesis by A5,LATTICES:8;
end;
end;
now
assume
A6: for a being Element of L holds a = "/\"({d where d is Element of
L: d in D & a [= d},L);
for a being Element of L holds ex D9 being Subset of D st a = "/\"(D9 ,L)
proof
let a be Element of L;
set X = {d where d is Element of L: d in D & a [= d};
for x being object holds x in X implies x in D
proof
let x be object;
assume x in X;
then ex x9 being Element of L st x9 = x & x9 in D & a [= x9;
hence thesis;
end;
then
A7: X is Subset of D by TARSKI:def 3;
a = "/\"(X,L) by A6;
hence thesis by A7;
end;
hence D is infimum-dense;
end;
hence thesis by A1;
end;
theorem
for L being complete Lattice for D being Subset of L holds D is
infimum-dense iff D% is order-generating
proof
let L be complete Lattice;
let D be Subset of L;
A1: now
assume
A2: D% is order-generating;
for a being Element of L holds ex D9 being Subset of D st a = "/\"(D9 ,L)
proof
let a be Element of L;
consider Y being Subset of D% such that
A3: a% = "/\"(Y,LattPOSet L) by A2,WAYBEL_6:15;
A4: for x being object
holds x in Y implies x in the carrier of LattPOSet L
proof
let x be object;
assume x in Y;
then x in D%;
hence thesis;
end;
A5: a% is_<=_than Y by A3,YELLOW_0:33;
reconsider Y as Subset of LattPOSet L by A4,TARSKI:def 3;
A6: for b being Element of L st b is_less_than %Y holds b [= a
proof
let b be Element of L;
assume
A7: b is_less_than %Y;
for u being Element of LattPOSet L st u in Y holds b% <= u
proof
let u be Element of LattPOSet L;
assume u in Y;
then %u in {%d where d is Element of LattPOSet L : d in Y};
then
A8: b [= %u by A7,LATTICE3:def 16;
(%u)% = %u by LATTICE3:def 3
.= u by LATTICE3:def 4;
hence thesis by A8,LATTICE3:7;
end;
then b% is_<=_than Y by LATTICE3:def 8;
then b% <= a% by A3,YELLOW_0:33;
hence thesis by LATTICE3:7;
end;
for x being object holds x in %Y implies x in D
proof
let x be object;
assume x in %Y;
then consider x9 being Element of LattPOSet L such that
A9: x = %(x9) and
A10: x9 in Y;
x9 in D% by A10;
then consider y being Element of L such that
A11: x9 = y% and
A12: y in D;
x = y% by A9,A11,LATTICE3:def 4
.= y by LATTICE3:def 3;
hence thesis by A12;
end;
then
A13: %Y is Subset of D by TARSKI:def 3;
for q being Element of L st q in %Y holds a [= q
proof
let q be Element of L;
assume q in %Y;
then consider q9 being Element of LattPOSet L such that
A14: q = %(q9) and
A15: q9 in Y;
A16: q9 = %(q9) by LATTICE3:def 4
.= (%(q9))% by LATTICE3:def 3;
a% <= q9 by A5,A15,LATTICE3:def 8;
hence thesis by A14,A16,LATTICE3:7;
end;
then a is_less_than %Y by LATTICE3:def 16;
then a = "/\"(%Y,L) by A6,LATTICE3:34;
hence thesis by A13;
end;
hence D is infimum-dense;
end;
now
assume
A17: D is infimum-dense;
for a being Element of LattPOSet L ex Y being Subset of D% st a = "/\"
(Y,LattPOSet L)
proof
let a be Element of LattPOSet L;
consider D9 being Subset of D such that
A18: %a = "/\"(D9,L) by A17;
A19: for x being object holds x in D9 implies x in the carrier of L
proof
let x be object;
assume x in D9;
then x in D;
hence thesis;
end;
A20: %a is_less_than D9 by A18,LATTICE3:34;
reconsider D9 as Subset of L by A19,TARSKI:def 3;
A21: for b being Element of LattPOSet L st (D9)% is_>=_than b holds b <= a
proof
let b be Element of LattPOSet L;
A22: b = %b by LATTICE3:def 4
.= (%b)% by LATTICE3:def 3;
assume
A23: (D9)% is_>=_than b;
for u being Element of L st u in D9 holds %b [= u
proof
let u be Element of L;
assume u in D9;
then u% in {d% where d is Element of L : d in D9};
then b <= u% by A23,LATTICE3:def 8;
hence thesis by A22,LATTICE3:7;
end;
then %b is_less_than D9 by LATTICE3:def 16;
then
A24: %b [= %a by A18,LATTICE3:34;
a = %a by LATTICE3:def 4
.= (%a)% by LATTICE3:def 3;
hence thesis by A22,A24,LATTICE3:7;
end;
for x being object holds x in (D9)% implies x in D%
proof
let x be object;
assume x in (D9)%;
then ex x9 being Element of L st x = (x9)% & x9 in D9;
hence thesis;
end;
then
A25: (D9)% is Subset of D% by TARSKI:def 3;
for u being Element of LattPOSet L st u in (D9)% holds a <= u
proof
let u be Element of LattPOSet L;
A26: (%a)% = %a by LATTICE3:def 3
.= a by LATTICE3:def 4;
assume u in (D9)%;
then consider u9 being Element of L such that
A27: u = (u9)% and
A28: u9 in D9;
%a [= u9 by A20,A28,LATTICE3:def 16;
hence thesis by A27,A26,LATTICE3:7;
end;
then (D9)% is_>=_than a by LATTICE3:def 8;
then a = "/\"((D9)%,LattPOSet L)by A21,YELLOW_0:33;
hence thesis by A25;
end;
hence D% is order-generating by WAYBEL_6:15;
end;
hence thesis by A1;
end;
definition
let L be complete Lattice;
func MIRRS(L) -> Subset of L equals
{a where a is Element of L : a is
completely-meet-irreducible};
correctness
proof
set X = {a where a is Element of L : a is completely-meet-irreducible};
for x being object holds x in X implies x in the carrier of L
proof
let x be object;
assume x in X;
then ex x9 being Element of L st x9 = x & x9 is
completely-meet-irreducible;
hence thesis;
end;
hence thesis by TARSKI:def 3;
end;
func JIRRS(L) -> Subset of L equals
{a where a is Element of L : a is
completely-join-irreducible };
correctness
proof
set X = {a where a is Element of L : a is completely-join-irreducible };
for x being object holds x in X implies x in the carrier of L
proof
let x be object;
assume x in X;
then ex x9 being Element of L st x9 = x & x9 is
completely-join-irreducible;
hence thesis;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem
for L being complete Lattice for D being Subset of L st D is
supremum-dense holds JIRRS(L) c= D
proof
let L be complete Lattice;
let D be Subset of L;
assume
A1: D is supremum-dense;
for x being object holds x in JIRRS(L) implies x in D
proof
let x be object;
assume x in JIRRS(L);
then consider x9 being Element of L such that
A2: x9 = x and
A3: x9 is completely-join-irreducible;
assume
A4: not x in D;
reconsider x as Element of L by A2;
set D9 = {d where d is Element of L: d in D & d [= x};
set X = {d where d is Element of L: d [= x & d <> x};
A5: not x in D9
proof
assume x in D9;
then ex x9 being Element of L st x9 = x & x9 in D & x9 [= x;
hence thesis by A4;
end;
for u being object holds u in D9 implies u in X
proof
let u be object;
assume
A6: u in D9;
then
ex u9 being Element of L st u9 = u & u9 in D & u9 [= x;
hence thesis by A5,A6;
end;
then D9 c= X;
then "\/"(D9,L) [= "\/"(X,L) by LATTICE3:45;
then
A7: x [= "\/"(X,L) by A1,Th23;
for q being Element of L st q in X holds q [= x
proof
let q be Element of L;
assume q in X;
then ex q9 being Element of L st q9 = q & q9 [= x & q9 <> x;
hence thesis;
end;
then X is_less_than x by LATTICE3:def 17;
then
A8: "\/"(X,L) [= x by LATTICE3:def 21;
*'(x9) <> x9 by A3;
hence thesis by A2,A7,A8,LATTICES:8;
end;
hence thesis;
end;
theorem
for L being complete Lattice for D being Subset of L st D is
infimum-dense holds MIRRS(L) c= D
proof
let L be complete Lattice;
let D be Subset of L;
assume
A1: D is infimum-dense;
let x be object;
assume x in MIRRS(L);
then consider x9 being Element of L such that
A2: x9 = x and
A3: x9 is completely-meet-irreducible;
assume
A4: not x in D;
reconsider x as Element of L by A2;
set D9 = {d where d is Element of L: d in D & x [= d};
set X = {d where d is Element of L: x [= d & d <> x};
A5: not x in D9
proof
assume x in D9;
then ex x9 being Element of L st x9 = x & x9 in D & x [= x9;
hence thesis by A4;
end;
for u being object holds u in D9 implies u in X
proof
let u be object;
assume
A6: u in D9;
then
ex u9 being Element of L st u9 = u & u9 in D & x [= u9;
hence thesis by A5,A6;
end;
then D9 c= X;
then "/\"(X,L) [= "/\"(D9,L) by LATTICE3:45;
then
A7: "/\"(X,L) [= x by A1,Th24;
for q being Element of L st q in X holds x [= q
proof
let q be Element of L;
assume q in X;
then ex q9 being Element of L st q9 = q & x [= q9 & q9 <> x;
hence thesis;
end;
then x is_less_than X by LATTICE3:def 16;
then
A8: x [= "/\"(X,L) by LATTICE3:39;
(x9)*' <> x9 by A3;
hence thesis by A2,A7,A8,LATTICES:8;
end;
Lm9: for L being co-noetherian complete Lattice holds MIRRS(L) is
infimum-dense
proof
let L be co-noetherian complete Lattice;
defpred P[Element of (LattPOSet L)~] means ex D9 being Subset of MIRRS(L) st
$1 = ("/\"(D9,L))%;
A1: for x being Element of (LattPOSet L)~ st for y being Element of (
LattPOSet L)~ st y <> x & [y,x] in the InternalRel of (LattPOSet L)~ holds P[y]
holds P[x]
proof
let x be Element of (LattPOSet L)~;
set X = {d where d is Element of L: %(~x) [= d & d <> %(~x)};
A2: for u being Element of L st u in X holds (u%)~ <> x & [(u%)~,x] in the
InternalRel of (LattPOSet L)~
proof
let u be Element of L;
A3: ((%(~x))%)~ = (%(~x))% by LATTICE3:def 6
.= %(~x) by LATTICE3:def 3
.= ~x by LATTICE3:def 4
.= x by LATTICE3:def 7;
assume u in X;
then
A4: ex u9 being Element of L st u9 = u & %(~x) [= u9 & %(~x ) <> u9;
then (%(~x))% <= u% by LATTICE3:7;
then
A5: (u%)~ <= x by A3,LATTICE3:9;
A6: (u%)~ = u% by LATTICE3:def 6
.= u by LATTICE3:def 3;
%(~x) = ~x by LATTICE3:def 4
.= x by LATTICE3:def 7;
hence thesis by A4,A5,A6,ORDERS_2:def 5;
end;
assume
A7: for y being Element of (LattPOSet L)~ st y <> x & [y,x] in the
InternalRel of (LattPOSet L)~ holds P[y];
A8: for u being Element of L st u in X holds P[(u%)~]
proof
let u be Element of L;
assume u in X;
then
(u%)~ <> x & [(u%)~,x] in the InternalRel of (LattPOSet L)~ by A2;
hence thesis by A7;
end;
per cases;
suppose
%(~x) is completely-meet-irreducible;
then %(~x) in {a where a is Element of L : a is
completely-meet-irreducible };
then for y being object holds y in {%(~x)} implies y in MIRRS(L) by
TARSKI:def 1;
then
A9: {%(~x)} is Subset of MIRRS(L) by TARSKI:def 3;
("/\"({%(~x)},L))% = "/\"({%(~x)},L) by LATTICE3:def 3
.= %(~x) by LATTICE3:42
.= ~x by LATTICE3:def 4
.= x by LATTICE3:def 7;
hence thesis by A9;
end;
suppose
A10: not %(~x) is completely-meet-irreducible;
set G = {H where H is Subset of MIRRS(L) : ex u being Element of
LattPOSet L st %u in X & %u = "/\" (H,L)};
set D9 = union G;
A11: (%(~x))*' = %(~x) by A10;
A12: for r being Element of L st r is_less_than D9 holds r [= %(~x)
proof
let r be Element of L;
assume
A13: r is_less_than D9;
for q being Element of L st q in X holds r [= q
proof
let q be Element of L;
assume
A14: q in X;
then consider D being Subset of MIRRS(L) such that
A15: (q%)~ = ("/\"(D,L))% by A8;
A16: q% = q by LATTICE3:def 3;
for v being object holds v in D implies v in D9
proof
let v be object;
(q%)~ = q% by LATTICE3:def 6
.= %(q%) by LATTICE3:def 4;
then
A17: %(q%) = "/\"(D,L) by A15,LATTICE3:def 3;
%(q%) in X by A14,A16,LATTICE3:def 4;
then
A18: D in G by A17;
assume v in D;
hence thesis by A18,TARSKI:def 4;
end;
then D c= D9;
then for p being Element of L st p in D holds r [= p by A13,
LATTICE3:def 16;
then
A19: r is_less_than D by LATTICE3:def 16;
q = (q%)~ by A16,LATTICE3:def 6
.= "/\"(D,L) by A15,LATTICE3:def 3;
hence thesis by A19,LATTICE3:34;
end;
then r is_less_than X by LATTICE3:def 16;
hence thesis by A11,LATTICE3:34;
end;
for v being object holds v in D9 implies v in MIRRS(L)
proof
let v be object;
assume v in D9;
then consider v9 being set such that
A20: v in v9 and
A21: v9 in G by TARSKI:def 4;
ex H being Subset of MIRRS(L) st H = v9 & ex u being Element of
LattPOSet L st %u in X & %u = "/\" (H,L) by A21;
hence thesis by A20;
end;
then
A22: D9 is Subset of MIRRS(L) by TARSKI:def 3;
A23: %(~x) = ~x by LATTICE3:def 4
.= x by LATTICE3:def 7;
A24: ("/\"(D9,L))% = "/\"(D9,L) by LATTICE3:def 3;
for q being Element of L st q in D9 holds %(~x) [= q
proof
let q be Element of L;
assume q in D9;
then consider h being set such that
A25: q in h and
A26: h in G by TARSKI:def 4;
ex h9 being Subset of MIRRS(L) st h9 = h & ex u being Element of
LattPOSet L st %u in X & %u = "/\"(h9,L) by A26;
then consider u being Element of LattPOSet L such that
A27: %u in X and
A28: %u = "/\"(h,L);
%u is_less_than h by A28,LATTICE3:34;
then
A29: %u [= q by A25,LATTICE3:def 16;
%(~x) is_less_than X by A11,LATTICE3:34;
then %(~x) [= %u by A27,LATTICE3:def 16;
hence thesis by A29,LATTICES:7;
end;
then %(~x) is_less_than D9 by LATTICE3:def 16;
then %(~x) = "/\"(D9,L) by A12,LATTICE3:34;
hence thesis by A22,A23,A24;
end;
end;
A30: (LattPOSet L)~ is well_founded by Def4;
A31: for x being Element of (LattPOSet L)~ holds P[x] from WELLFND1:sch 3 (
A1,A30);
for a being Element of L holds ex D9 being Subset of MIRRS(L) st a =
"/\"(D9,L)
proof
let a be Element of L;
(LattPOSet L)~ = RelStr(#the carrier of LattPOSet L, (the InternalRel
of LattPOSet L)~#) by LATTICE3:def 5;
then reconsider a9 = a% as Element of (LattPOSet L)~;
(ex D9 being Subset of MIRRS(L) st a9 = ("/\" (D9,L))% )& a% = a by A31,
LATTICE3:def 3;
hence thesis by LATTICE3:def 3;
end;
hence thesis;
end;
registration
let L be co-noetherian complete Lattice;
cluster MIRRS(L) -> infimum-dense;
coherence by Lm9;
end;
Lm10: for L being noetherian complete Lattice holds JIRRS(L) is supremum-dense
proof
let L be noetherian complete Lattice;
defpred P[Element of LattPOSet L] means ex D9 being Subset of JIRRS(L) st %(
$1) = "\/"(D9,L);
A1: for x being Element of LattPOSet L st for y being Element of LattPOSet L
st y <> x & [y,x] in the InternalRel of LattPOSet L holds P[y] holds P[x]
proof
let x be Element of LattPOSet L;
set X = {d where d is Element of L: d [= %x & d <> %x};
A2: for u being Element of L st u in X holds u% <> x & [u%,x] in the
InternalRel of LattPOSet L
proof
let u be Element of L;
assume u in X;
then
A3: ex u9 being Element of L st u9 = u & u9 [= %x & %x <> u9;
A4: %x = x by LATTICE3:def 4;
then (%x)% = x by LATTICE3:def 3;
then u% <= x by A3,LATTICE3:7;
hence thesis by A3,A4,LATTICE3:def 3,ORDERS_2:def 5;
end;
assume
A5: for y being Element of LattPOSet L st y <> x & [y,x] in the
InternalRel of LattPOSet L holds P[y];
A6: for u being Element of L st u in X holds P[u%]
proof
let u be Element of L;
assume u in X;
then u% <> x & [u%,x] in the InternalRel of LattPOSet L by A2;
hence thesis by A5;
end;
per cases;
suppose
%x is completely-join-irreducible;
then
%x in {a where a is Element of L : a is completely-join-irreducible };
then for y being object holds y in {%x} implies y in JIRRS(L) by
TARSKI:def 1;
then
A7: {%x} is Subset of JIRRS(L) by TARSKI:def 3;
"\/"({%x},L) = %x by LATTICE3:42;
hence thesis by A7;
end;
suppose
A8: not %x is completely-join-irreducible;
set G = {H where H is Subset of JIRRS(L) : ex u being Element of
LattPOSet L st %u in X & %u = "\/" (H,L)};
set D9 = union G;
A9: *'(%x) = %x by A8;
A10: for r being Element of L st D9 is_less_than r holds %x [= r
proof
let r be Element of L;
assume
A11: D9 is_less_than r;
for q being Element of L st q in X holds q [= r
proof
let q be Element of L;
assume
A12: q in X;
then consider D being Subset of JIRRS(L) such that
A13: %(q%) = "\/"(D,L) by A6;
q% = q by LATTICE3:def 3;
then
A14: q = "\/"(D,L) by A13,LATTICE3:def 4;
for v being object holds v in D implies v in D9
proof
let v be object;
assume
A15: v in D;
D in G by A12,A13,A14;
hence thesis by A15,TARSKI:def 4;
end;
then D c= D9;
then for p being Element of L st p in D holds p [= r by A11,
LATTICE3:def 17;
then D is_less_than r by LATTICE3:def 17;
hence thesis by A14,LATTICE3:def 21;
end;
then X is_less_than r by LATTICE3:def 17;
hence thesis by A9,LATTICE3:def 21;
end;
for v being object holds v in D9 implies v in JIRRS(L)
proof
let v be object;
assume v in D9;
then consider v9 being set such that
A16: v in v9 and
A17: v9 in G by TARSKI:def 4;
ex H being Subset of JIRRS(L) st H = v9 & ex u being Element of
LattPOSet L st %u in X & %u = "\/" (H,L) by A17;
hence thesis by A16;
end;
then
A18: D9 is Subset of JIRRS(L) by TARSKI:def 3;
for q being Element of L st q in D9 holds q [= %x
proof
let q be Element of L;
assume q in D9;
then consider h being set such that
A19: q in h and
A20: h in G by TARSKI:def 4;
ex h9 being Subset of JIRRS(L) st h9 = h & ex u being Element of
LattPOSet L st %u in X & %u = "\/"(h9,L) by A20;
then consider u being Element of LattPOSet L such that
A21: %u in X and
A22: %u = "\/"(h,L);
h is_less_than %u by A22,LATTICE3:def 21;
then
A23: q [= %u by A19,LATTICE3:def 17;
X is_less_than %x by A9,LATTICE3:def 21;
then %u [= %x by A21,LATTICE3:def 17;
hence thesis by A23,LATTICES:7;
end;
then D9 is_less_than %x by LATTICE3:def 17;
then %x = "\/"(D9,L) by A10,LATTICE3:def 21;
hence thesis by A18;
end;
end;
A24: LattPOSet L is well_founded by Def3;
A25: for x being Element of LattPOSet L holds P[x] from WELLFND1:sch 3(A1,
A24);
for a being Element of L holds ex D9 being Subset of JIRRS(L) st a =
"\/"(D9,L)
proof
let a be Element of L;
%(a%) = a% by LATTICE3:def 4
.= a by LATTICE3:def 3;
hence thesis by A25;
end;
hence thesis;
end;
registration
let L be noetherian complete Lattice;
cluster JIRRS(L) -> supremum-dense;
coherence by Lm10;
end;