:: Completely-Irreducible Elements
:: by Robert Milewski
::
:: Received February 9, 1998
:: Copyright (c) 1998-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 WAYBEL_0, SUBSET_1, LATTICES, XBOOLE_0, EQREL_1, ORDERS_2,
ORDERS_1, STRUCT_0, XXREAL_0, TARSKI, ARYTM_3, LATTICE3, ARYTM_0,
RELAT_1, RELAT_2, CARD_FIL, REWRITE1, FUNCT_1, FUNCOP_1, YELLOW_0,
SEQM_3, FINSET_1, ORDINAL2, YELLOW_1, SETFAM_1, WELLORD2, ZFMISC_1,
WAYBEL_1, WAYBEL_6, YELLOW_8, WAYBEL_2, INT_2, WAYBEL_3, WAYBEL_8,
RCOMP_1, WAYBEL16;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, RELSET_1, FUNCT_2,
FUNCOP_1, DOMAIN_1, ORDERS_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0,
YELLOW_1, YELLOW_4, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3,
WAYBEL_4, WAYBEL_6, WAYBEL_8;
constructors DOMAIN_1, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_2, WAYBEL_3,
WAYBEL_4, WAYBEL_6, WAYBEL_8, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, LATTICE3,
YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_2, WAYBEL_3, YELLOW_7,
WAYBEL_6, WAYBEL_8;
requirements BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, SUBSET_1, SETFAM_1, RELAT_1, ZFMISC_1, FUNCOP_1, ORDERS_2,
LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_4, YELLOW_7, WAYBEL_0,
WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_7, WAYBEL_8,
WAYBEL13, WAYBEL14, WAYBEL15, XBOOLE_0, XBOOLE_1;
schemes DOMAIN_1, SUBSET_1;
begin :: Preliminaries
theorem Th1:
for L be sup-Semilattice for x,y be Element of L holds "/\"((
uparrow x) /\ (uparrow y),L) = x "\/" y
proof
let L be sup-Semilattice;
let x,y be Element of L;
(uparrow x) /\ (uparrow y) = uparrow (x "\/" y) by WAYBEL14:4;
hence thesis by WAYBEL_0:39;
end;
theorem
for L be Semilattice for x,y be Element of L holds "\/"((downarrow x)
/\ (downarrow y),L) = x "/\" y
proof
let L be Semilattice;
let x,y be Element of L;
(downarrow x) /\ (downarrow y) = downarrow (x "/\" y) by WAYBEL14:3;
hence thesis by WAYBEL_0:34;
end;
theorem Th3:
for L be non empty RelStr for x,y be Element of L st x
is_maximal_in (the carrier of L) \ uparrow y holds (uparrow x) \ {x} = (uparrow
x) /\ (uparrow y)
proof
let L be non empty RelStr;
let x,y be Element of L;
assume
A1: x is_maximal_in (the carrier of L) \ uparrow y;
then x in (the carrier of L) \ uparrow y by WAYBEL_4:55;
then not x in uparrow y by XBOOLE_0:def 5;
then
A2: not y <= x by WAYBEL_0:18;
thus (uparrow x) \ {x} c= (uparrow x) /\ (uparrow y)
proof
let a be object;
assume
A3: a in (uparrow x) \ {x};
then reconsider a1 = a as Element of L;
not a in {x} by A3,XBOOLE_0:def 5;
then
A4: a1 <> x by TARSKI:def 1;
A5: a in uparrow x by A3,XBOOLE_0:def 5;
then x <= a1 by WAYBEL_0:18;
then x < a1 by A4,ORDERS_2:def 6;
then not a1 in (the carrier of L) \ uparrow y by A1,WAYBEL_4:55;
then a in uparrow y by XBOOLE_0:def 5;
hence thesis by A5,XBOOLE_0:def 4;
end;
let a be object;
assume
A6: a in (uparrow x) /\ (uparrow y);
then
A7: a in uparrow x by XBOOLE_0:def 4;
reconsider a1 = a as Element of L by A6;
a in uparrow y by A6,XBOOLE_0:def 4;
then y <= a1 by WAYBEL_0:18;
then not a in {x} by A2,TARSKI:def 1;
hence thesis by A7,XBOOLE_0:def 5;
end;
theorem
for L be non empty RelStr for x,y be Element of L st x is_minimal_in (
the carrier of L) \ downarrow y holds (downarrow x) \ {x} = (downarrow x) /\ (
downarrow y)
proof
let L be non empty RelStr;
let x,y be Element of L;
assume
A1: x is_minimal_in (the carrier of L) \ downarrow y;
then x in (the carrier of L) \ downarrow y by WAYBEL_4:56;
then not x in downarrow y by XBOOLE_0:def 5;
then
A2: not x <= y by WAYBEL_0:17;
thus (downarrow x) \ {x} c= (downarrow x) /\ (downarrow y)
proof
let a be object;
assume
A3: a in (downarrow x) \ {x};
then reconsider a1 = a as Element of L;
not a in {x} by A3,XBOOLE_0:def 5;
then
A4: a1 <> x by TARSKI:def 1;
A5: a in downarrow x by A3,XBOOLE_0:def 5;
then a1 <= x by WAYBEL_0:17;
then a1 < x by A4,ORDERS_2:def 6;
then not a1 in (the carrier of L) \ downarrow y by A1,WAYBEL_4:56;
then a in downarrow y by XBOOLE_0:def 5;
hence thesis by A5,XBOOLE_0:def 4;
end;
let a be object;
assume
A6: a in (downarrow x) /\ (downarrow y);
then
A7: a in downarrow x by XBOOLE_0:def 4;
reconsider a1 = a as Element of L by A6;
a in downarrow y by A6,XBOOLE_0:def 4;
then a1 <= y by WAYBEL_0:17;
then not a in {x} by A2,TARSKI:def 1;
hence thesis by A7,XBOOLE_0:def 5;
end;
theorem Th5:
for L be with_suprema Poset for X,Y be Subset of L for X9,Y9 be
Subset of L opp st X = X9 & Y = Y9 holds X "\/" Y = X9 "/\" Y9
proof
let L be with_suprema Poset;
let X,Y be Subset of L;
let X9,Y9 be Subset of L opp;
assume
A1: X = X9 & Y = Y9;
thus X "\/" Y c= X9 "/\" Y9
proof
let a be object;
assume a in X "\/" Y;
then a in { p "\/" q where p,q is Element of L : p in X & q in Y } by
YELLOW_4:def 3;
then consider x,y be Element of L such that
A2: a = x "\/" y and
A3: x in X & y in Y;
A4: a = x~ "/\" y~ by A2,YELLOW_7:23;
x~ in X9 & y~ in Y9 by A1,A3,LATTICE3:def 6;
then
a in { p "/\" q where p,q is Element of L opp : p in X9 & q in Y9 } by A4;
hence thesis by YELLOW_4:def 4;
end;
let a be object;
assume a in X9 "/\" Y9;
then a in { p "/\" q where p,q is Element of L opp : p in X9 & q in Y9 } by
YELLOW_4:def 4;
then consider x,y be Element of L opp such that
A5: a = x "/\" y and
A6: x in X9 & y in Y9;
A7: a = ~x "\/" ~y by A5,YELLOW_7:24;
~x in X & ~y in Y by A1,A6,LATTICE3:def 7;
then a in { p "\/" q where p,q is Element of L : p in X & q in Y } by A7;
hence thesis by YELLOW_4:def 3;
end;
theorem
for L be with_infima Poset for X,Y be Subset of L for X9,Y9 be Subset
of L opp st X = X9 & Y = Y9 holds X "/\" Y = X9 "\/" Y9
proof
let L be with_infima Poset;
let X,Y be Subset of L;
let X9,Y9 be Subset of L opp;
assume
A1: X = X9 & Y = Y9;
thus X "/\" Y c= X9 "\/" Y9
proof
let a be object;
assume a in X "/\" Y;
then a in { p "/\" q where p,q is Element of L : p in X & q in Y } by
YELLOW_4:def 4;
then consider x,y be Element of L such that
A2: a = x "/\" y and
A3: x in X & y in Y;
A4: a = x~ "\/" y~ by A2,YELLOW_7:21;
x~ in X9 & y~ in Y9 by A1,A3,LATTICE3:def 6;
then
a in { p "\/" q where p,q is Element of L opp : p in X9 & q in Y9 } by A4;
hence thesis by YELLOW_4:def 3;
end;
let a be object;
assume a in X9 "\/" Y9;
then a in { p "\/" q where p,q is Element of L opp : p in X9 & q in Y9 } by
YELLOW_4:def 3;
then consider x,y be Element of L opp such that
A5: a = x "\/" y and
A6: x in X9 & y in Y9;
A7: a = ~x "/\" ~y by A5,YELLOW_7:22;
~x in X & ~y in Y by A1,A6,LATTICE3:def 7;
then a in { p "/\" q where p,q is Element of L : p in X & q in Y } by A7;
hence thesis by YELLOW_4:def 4;
end;
theorem Th7:
for L be non empty reflexive transitive RelStr holds Filt L = Ids (L opp)
proof
let L be non empty reflexive transitive RelStr;
A1: Ids (L opp) c= Filt L
proof
let x be object;
assume x in Ids L opp;
then x in the set of all X where X is Ideal of L opp by
WAYBEL_0:def 23;
then consider x1 be Ideal of L opp such that
A2: x1 = x;
x1 is upper Subset of L & x1 is filtered Subset of L by YELLOW_7:27,29;
then x in the set of all X where X is Filter of L by A2;
hence thesis by WAYBEL_0:def 24;
end;
Filt L c= Ids (L opp)
proof
let x be object;
assume x in Filt L;
then x in the set of all X where X is Filter of L by
WAYBEL_0:def 24;
then consider x1 be Filter of L such that
A3: x1 = x;
x1 is lower Subset of L opp & x1 is directed Subset of L opp by YELLOW_7:27
,29;
then x in the set of all X where X is Ideal of L opp by A3;
hence thesis by WAYBEL_0:def 23;
end;
hence thesis by A1;
end;
theorem
for L be non empty reflexive transitive RelStr holds Ids L = Filt (L opp)
proof
let L be non empty reflexive transitive RelStr;
A1: Filt (L opp) c= Ids L
proof
let x be object;
assume x in Filt L opp;
then x in the set of all X where X is Filter of L opp by
WAYBEL_0:def 24;
then consider x1 be Filter of L opp such that
A2: x1 = x;
x1 is lower Subset of L & x1 is directed Subset of L by YELLOW_7:26,28;
then x in the set of all X where X is Ideal of L by A2;
hence thesis by WAYBEL_0:def 23;
end;
Ids L c= Filt (L opp)
proof
let x be object;
assume x in Ids L;
then x in the set of all X where X is Ideal of L by
WAYBEL_0:def 23;
then consider x1 be Ideal of L such that
A3: x1 = x;
x1 is upper Subset of L opp & x1 is filtered Subset of L opp by YELLOW_7:26
,28;
then x in the set of all X where X is Filter of L opp by A3;
hence thesis by WAYBEL_0:def 24;
end;
hence thesis by A1;
end;
begin :: Free Generation Set
definition
let S,T be complete non empty Poset;
mode CLHomomorphism of S,T -> Function of S,T means
it is directed-sups-preserving infs-preserving;
existence
proof
reconsider f = (the carrier of S) --> Top T as Function of the carrier of
S,the carrier of T;
reconsider f as Function of S,T;
take f;
now
let X be Subset of S;
assume
A1: X is non empty directed;
now
assume ex_sup_of X,S;
rng f = {Top T} by FUNCOP_1:8;
then
A2: f.:X c= {Top T} by RELAT_1:111;
now
let x,y be Element of S;
assume x <= y;
f.x = Top T by FUNCOP_1:7
.= f.y by FUNCOP_1:7;
hence f.x <= f.y;
end;
then f is monotone by WAYBEL_1:def 2;
then
A3: f.:X is non empty finite directed Subset of T by A1,A2,YELLOW_2:15;
hence ex_sup_of f.:X,T by WAYBEL_0:75;
sup (f.:X) in f.:X by A3,WAYBEL_3:16;
then sup (f.:X) = Top T by A2,TARSKI:def 1;
hence sup (f.:X) = f.sup X by FUNCOP_1:7;
end;
hence f preserves_sup_of X by WAYBEL_0:def 31;
end;
hence f is directed-sups-preserving by WAYBEL_0:def 37;
now
let X be Subset of S;
now
assume ex_inf_of X,S;
thus ex_inf_of f.:X,T by YELLOW_0:17;
rng f = {Top T} by FUNCOP_1:8;
then
A4: f.:X is Subset of {Top T} by RELAT_1:111;
now
per cases;
suppose
f.:X = {};
hence inf (f.:X) = Top T by YELLOW_0:def 12
.= f.inf X by FUNCOP_1:7;
end;
suppose
f.:X <> {};
then f.:X = {Top T} by A4,ZFMISC_1:33;
hence inf (f.:X) = Top T by YELLOW_0:39
.= f.inf X by FUNCOP_1:7;
end;
end;
hence inf (f.:X) = f.inf X;
end;
hence f preserves_inf_of X by WAYBEL_0:def 30;
end;
hence thesis by WAYBEL_0:def 32;
end;
end;
definition
let S be continuous complete non empty Poset;
let A be Subset of S;
pred A is_FG_set means
for T be continuous complete non empty Poset for f
be Function of A,the carrier of T ex h be CLHomomorphism of S,T st h|A = f &
for h9 be CLHomomorphism of S,T st h9|A = f holds h9 = h;
end;
registration
let L be upper-bounded non empty Poset;
cluster Filt L -> non empty;
coherence
proof
now
let x,y be Element of L;
assume that
A1: x in {Top L} and
A2: x <= y;
x = Top L by A1,TARSKI:def 1;
then y = Top L by A2,WAYBEL15:3;
hence y in {Top L} by TARSKI:def 1;
end;
then {Top L} is Filter of L by WAYBEL_0:5,def 20;
then {Top L} in the set of all Y where Y is Filter of L ;
hence thesis by WAYBEL_0:def 24;
end;
end;
theorem Th9:
for X be set for Y be non empty Subset of InclPoset Filt
BoolePoset X holds meet Y is Filter of BoolePoset X
proof
let X be set;
set L = BoolePoset X;
let Y be non empty Subset of InclPoset Filt L;
A1: now
let Z be set;
assume Z in Y;
then Z in the carrier of InclPoset Filt L;
then Z in the carrier of RelStr(#Filt L, RelIncl (Filt L)#) by
YELLOW_1:def 1;
then Z in the set of all V where V is Filter of L by
WAYBEL_0:def 24;
then ex Z1 be Filter of L st Z1 = Z;
hence Top L in Z by WAYBEL_4:22;
end;
Y c= the carrier of InclPoset Filt L;
then
A2: Y c= the carrier of RelStr(#Filt L, RelIncl (Filt L)#) by YELLOW_1:def 1;
A3: for Z be Subset of L st Z in Y holds Z is upper
proof
let Z be Subset of L;
assume Z in Y;
then Z in Filt L by A2;
then Z in the set of all V where V is Filter of L by
WAYBEL_0:def 24;
then ex Z1 be Filter of L st Z1 = Z;
hence thesis;
end;
A4: now
let V be Subset of L;
assume V in Y;
then V in Filt L by A2;
then V in the set of all Z where Z is Filter of L by
WAYBEL_0:def 24;
then
A5: ex V1 be Filter of L st V1 = V;
hence V is upper;
thus V is filtered by A5;
end;
Y c= bool the carrier of L
proof
let v be object;
assume v in Y;
then v in Filt L by A2;
then v in the set of all V where V is Filter of L by
WAYBEL_0:def 24;
then ex v1 be Filter of L st v1 = v;
hence thesis;
end;
hence thesis by A1,A3,A4,SETFAM_1:def 1,YELLOW_2:37,39;
end;
theorem
for X be set for Y be non empty Subset of InclPoset Filt BoolePoset X
holds ex_inf_of Y,InclPoset Filt BoolePoset X & "/\"(Y,InclPoset Filt
BoolePoset X) = meet Y
proof
let X be set;
set L = InclPoset Filt BoolePoset X;
let Y be non empty Subset of L;
meet Y is Filter of BoolePoset X by Th9;
then meet Y in the set of all Z where Z is Filter of BoolePoset X;
then meet Y in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt
BoolePoset X)#) by WAYBEL_0:def 24;
then reconsider a = meet Y as Element of L by YELLOW_1:def 1;
A1: for b be Element of L st b is_<=_than Y holds b <= a
proof
let b be Element of L;
assume
A2: b is_<=_than Y;
for x being set st x in Y holds b c= x by YELLOW_1:3,A2,LATTICE3:def 8;
then b c= meet Y by SETFAM_1:5;
hence thesis by YELLOW_1:3;
end;
for b being Element of L st b in Y holds a <= b by YELLOW_1:3,SETFAM_1:3;
then a is_<=_than Y by LATTICE3:def 8;
hence thesis by A1,YELLOW_0:31;
end;
theorem Th11:
for X be set holds bool X is Filter of BoolePoset X
proof
let X be set;
bool X c= the carrier of BoolePoset X by WAYBEL_7:2;
then reconsider A = bool X as non empty Subset of BoolePoset X;
A1: now
let x,y be set;
assume x in A & y in A;
then x /\ y c= X /\ X by XBOOLE_1:27;
hence x /\ y in A;
end;
for x,y be set st x c= y & y c= X & x in A holds y in A;
then A is upper by WAYBEL_7:7;
hence thesis by A1,WAYBEL_7:9;
end;
theorem Th12:
for X be set holds {X} is Filter of BoolePoset X
proof
let X be set;
now
let c be object;
assume c in {X};
then c = X by TARSKI:def 1;
then c is Element of BoolePoset X by WAYBEL_8:26;
hence c in the carrier of BoolePoset X;
end;
then reconsider A = {X} as non empty Subset of BoolePoset X by TARSKI:def 3;
for x,y be set st x c= y & y c= X & x in A holds y in A
proof
let x,y be set;
assume that
A1: x c= y & y c= X and
A2: x in A;
x = X by A2,TARSKI:def 1;
then y = X by A1;
hence thesis by TARSKI:def 1;
end;
then
A3: A is upper by WAYBEL_7:7;
now
let x,y be set;
assume x in A & y in A;
then x = X & y = X by TARSKI:def 1;
hence x /\ y in A by TARSKI:def 1;
end;
hence thesis by A3,WAYBEL_7:9;
end;
theorem
for X be set holds InclPoset Filt BoolePoset X is upper-bounded
proof
let X be set;
set L = InclPoset Filt BoolePoset X;
bool X is Filter of BoolePoset X by Th11;
then bool X in the set of all Z where Z is Filter of BoolePoset X;
then bool X in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt
BoolePoset X)#) by WAYBEL_0:def 24;
then reconsider x = bool X as Element of L by YELLOW_1:def 1;
now
let b be Element of L;
assume b in the carrier of L;
then b in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt
BoolePoset X)#) by YELLOW_1:def 1;
then b in the set of all V where V is Filter of BoolePoset X by
WAYBEL_0:def 24;
then ex b1 be Filter of BoolePoset X st b1 = b;
then b c= the carrier of BoolePoset X;
then b c= bool X by WAYBEL_7:2;
hence b <= x by YELLOW_1:3;
end;
then x is_>=_than the carrier of L by LATTICE3:def 9;
hence thesis by YELLOW_0:def 5;
end;
theorem
for X be set holds InclPoset Filt BoolePoset X is lower-bounded
proof
let X be set;
set L = InclPoset Filt BoolePoset X;
{X} is Filter of BoolePoset X by Th12;
then {X} in the set of all Z where Z is Filter of BoolePoset X;
then {X} in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt
BoolePoset X)#) by WAYBEL_0:def 24;
then reconsider x = {X} as Element of L by YELLOW_1:def 1;
now
let b be Element of L;
assume b in the carrier of L;
then b in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt
BoolePoset X)#) by YELLOW_1:def 1;
then b in the set of all V where V is Filter of BoolePoset X by
WAYBEL_0:def 24;
then consider b1 be Filter of BoolePoset X such that
A1: b1 = b;
consider d be object such that
A2: d in b1 by XBOOLE_0:def 1;
reconsider d as set by TARSKI:1;
A3: d c= X by A2,WAYBEL_8:26;
now
let c be object;
assume c in {X};
then c = X by TARSKI:def 1;
hence c in b by A1,A2,A3,WAYBEL_7:7;
end;
then {X} c= b;
hence x <= b by YELLOW_1:3;
end;
then x is_<=_than the carrier of L by LATTICE3:def 8;
hence thesis by YELLOW_0:def 4;
end;
theorem
for X be set holds Top (InclPoset Filt BoolePoset X) = bool X
proof
let X be set;
set L = InclPoset Filt BoolePoset X;
bool X is Filter of BoolePoset X by Th11;
then bool X in the set of all Z where Z is Filter of BoolePoset X;
then bool X in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt
BoolePoset X)#) by WAYBEL_0:def 24;
then reconsider bX = bool X as Element of L by YELLOW_1:def 1;
A1: for b be Element of L st b is_<=_than {} holds bX >= b
proof
let b be Element of L;
assume b is_<=_than {};
b in the carrier of L;
then b in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt
BoolePoset X)#) by YELLOW_1:def 1;
then b in the set of all V where V is Filter of BoolePoset X by
WAYBEL_0:def 24;
then ex b1 be Filter of BoolePoset X st b1 = b;
then b c= the carrier of BoolePoset X;
then b c= bool X by WAYBEL_7:2;
hence thesis by YELLOW_1:3;
end;
bX is_<=_than {} by YELLOW_0:6;
then "/\"({},L) = bool X by A1,YELLOW_0:31;
hence thesis by YELLOW_0:def 12;
end;
theorem
for X be set holds Bottom (InclPoset Filt BoolePoset X) = {X}
proof
let X be set;
set L = InclPoset Filt BoolePoset X;
{X} is Filter of BoolePoset X by Th12;
then {X} in the set of all Z where Z is Filter of BoolePoset X;
then {X} in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt
BoolePoset X)#) by WAYBEL_0:def 24;
then reconsider bX = {X} as Element of L by YELLOW_1:def 1;
A1: for b be Element of L st b is_>=_than {} holds bX <= b
proof
let b be Element of L;
assume b is_>=_than {};
b in the carrier of L;
then b in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt
BoolePoset X)#) by YELLOW_1:def 1;
then b in the set of all V where V is Filter of BoolePoset X by
WAYBEL_0:def 24;
then consider b1 be Filter of BoolePoset X such that
A2: b1 = b;
consider d be object such that
A3: d in b1 by XBOOLE_0:def 1;
reconsider d as set by TARSKI:1;
A4: d c= X by A3,WAYBEL_8:26;
now
let c be object;
assume c in {X};
then c = X by TARSKI:def 1;
hence c in b by A2,A3,A4,WAYBEL_7:7;
end;
then {X} c= b;
hence thesis by YELLOW_1:3;
end;
bX is_>=_than {} by YELLOW_0:6;
then "\/"({},L) = {X} by A1,YELLOW_0:30;
hence thesis by YELLOW_0:def 11;
end;
theorem
for X be non empty set for Y be non empty Subset of InclPoset X st
ex_sup_of Y,InclPoset X holds union Y c= sup Y
proof
let X be non empty set;
let Y be non empty Subset of InclPoset X;
assume
A1: ex_sup_of Y,InclPoset X;
now
let x be set;
assume
A2: x in Y;
then reconsider x1 = x as Element of InclPoset X;
sup Y is_>=_than Y by A1,YELLOW_0:30;
then sup Y >= x1 by A2,LATTICE3:def 9;
hence x c= sup Y by YELLOW_1:3;
end;
hence thesis by ZFMISC_1:76;
end;
theorem Th18:
for L be upper-bounded Semilattice holds InclPoset Filt L is complete
proof
let L be upper-bounded Semilattice;
InclPoset Ids (L opp) is complete;
hence thesis by Th7;
end;
registration
let L be upper-bounded Semilattice;
cluster InclPoset Filt L -> complete;
coherence by Th18;
end;
begin :: Completely-irreducible Elements
definition
let L be non empty RelStr;
let p be Element of L;
attr p is completely-irreducible means
ex_min_of (uparrow p)\{p},L;
end;
theorem Th19:
for L be non empty RelStr for p be Element of L st p is
completely-irreducible holds "/\"((uparrow p)\{p},L) <> p
proof
let L be non empty RelStr;
let p be Element of L;
assume p is completely-irreducible;
then ex_min_of (uparrow p)\{p},L;
then "/\"((uparrow p)\{p},L) in (uparrow p)\{p} by WAYBEL_1:def 4;
then not "/\"((uparrow p)\{p},L) in {p} by XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
definition
let L be non empty RelStr;
func Irr L -> Subset of L means
:Def4:
for x be Element of L holds x in it iff x is completely-irreducible;
existence
proof
defpred P[Element of L] means $1 is completely-irreducible;
consider X be Subset of L such that
A1: for x be Element of L holds x in X iff P[x] from SUBSET_1:sch 3;
take X;
thus thesis by A1;
end;
uniqueness
proof
let S1,S2 be Subset of L such that
A2: for x be Element of L holds x in S1 iff x is completely-irreducible and
A3: for x be Element of L holds x in S2 iff x is completely-irreducible;
for x1 being object holds x1 in S1 iff x1 in S2 by A2,A3;
hence thesis by TARSKI:2;
end;
end;
theorem Th20: :: THEOREM 4.19 (i)
for L be non empty Poset for p be Element of L holds p is
completely-irreducible iff ex q be Element of L st p < q & (for s be Element of
L st p < s holds q <= s) & uparrow p = {p} \/ uparrow q
proof
let L be non empty Poset;
let p be Element of L;
thus p is completely-irreducible implies ex q be Element of L st p < q & (
for s be Element of L st p < s holds q <= s) & uparrow p = {p} \/ uparrow q
proof
assume
A1: p is completely-irreducible;
then ex_min_of (uparrow p)\{p},L;
then
A2: ex_inf_of (uparrow p)\{p},L by WAYBEL_1:def 4;
take q = "/\" ((uparrow p)\{p},L);
now
let s be Element of L;
assume s in (uparrow p)\{p};
then s in uparrow p by XBOOLE_0:def 5;
hence p <= s by WAYBEL_0:18;
end;
then p is_<=_than (uparrow p)\{p} by LATTICE3:def 8;
then
A3: p <= q by A2,YELLOW_0:def 10;
A4: {p} \/ uparrow q c= uparrow p
proof
let x be object;
assume
A5: x in {p} \/ uparrow q;
now
per cases by A5,XBOOLE_0:def 3;
suppose
A6: x in {p};
A7: p <= p;
x = p by A6,TARSKI:def 1;
hence thesis by A7,WAYBEL_0:18;
end;
suppose
A8: x in uparrow q;
then reconsider x1 = x as Element of L;
q <= x1 by A8,WAYBEL_0:18;
then p <= x1 by A3,ORDERS_2:3;
hence thesis by WAYBEL_0:18;
end;
end;
hence thesis;
end;
"/\"((uparrow p)\{p},L) <> p by A1,Th19;
hence p < q by A3,ORDERS_2:def 6;
A9: q is_<=_than (uparrow p)\{p} by A2,YELLOW_0:def 10;
thus for s be Element of L st p < s holds q <= s
proof
let s be Element of L;
assume
A10: p < s;
then p <= s by ORDERS_2:def 6;
then
A11: s in uparrow p by WAYBEL_0:18;
not s in {p} by A10,TARSKI:def 1;
then s in (uparrow p)\{p} by A11,XBOOLE_0:def 5;
hence thesis by A9,LATTICE3:def 8;
end;
uparrow p c= {p} \/ uparrow q
proof
let x be object;
assume
A12: x in uparrow p;
then reconsider x1 = x as Element of L;
p = x1 or x1 in uparrow p & not x1 in {p} by A12,TARSKI:def 1;
then p = x1 or x1 in (uparrow p)\{p} by XBOOLE_0:def 5;
then p = x1 or "/\" ((uparrow p)\{p},L) <= x1 by A9,LATTICE3:def 8;
then x in {p} or x in uparrow q by TARSKI:def 1,WAYBEL_0:18;
hence thesis by XBOOLE_0:def 3;
end;
hence uparrow p = {p} \/ uparrow q by A4;
end;
thus (ex q be Element of L st p < q & (for s be Element of L st p < s holds
q <= s) & uparrow p = {p} \/ uparrow q) implies p is completely-irreducible
proof
given q be Element of L such that
A13: p < q and
A14: for s be Element of L st p < s holds q <= s and
A15: uparrow p = {p} \/ uparrow q;
A16: not q in {p} by A13,TARSKI:def 1;
ex q be Element of L st (uparrow p)\{p} is_>=_than q & for b be
Element of L st (uparrow p)\{p} is_>=_than b holds q >= b
proof
take q;
now
let a be Element of L;
assume
A17: a in (uparrow p)\{p};
then not a in {p} by XBOOLE_0:def 5;
then
A18: a <> p by TARSKI:def 1;
a in uparrow p by A17,XBOOLE_0:def 5;
then p <= a by WAYBEL_0:18;
then p < a by A18,ORDERS_2:def 6;
hence q <= a by A14;
end;
hence (uparrow p)\{p} is_>=_than q by LATTICE3:def 8;
let b be Element of L;
assume
A19: (uparrow p)\{p} is_>=_than b;
q <= q;
then q in uparrow q by WAYBEL_0:18;
then
A20: q in {p} \/ uparrow q by XBOOLE_0:def 3;
not q in {p} by A13,TARSKI:def 1;
then q in (uparrow p)\{p} by A15,A20,XBOOLE_0:def 5;
hence thesis by A19,LATTICE3:def 8;
end;
then
A21: ex_inf_of (uparrow p)\{p},L by YELLOW_0:16;
A22: now
let b be Element of L;
assume
A23: b is_<=_than (uparrow p)\{p};
p <= q by A13,ORDERS_2:def 6;
then
A24: q in uparrow p by WAYBEL_0:18;
not q in {p} by A13,TARSKI:def 1;
then q in (uparrow p)\{p} by A24,XBOOLE_0:def 5;
hence q >= b by A23,LATTICE3:def 8;
end;
p <= q by A13,ORDERS_2:def 6;
then
A25: q in uparrow p by WAYBEL_0:18;
now
let c be Element of L;
assume c in (uparrow p)\{p};
then c in uparrow p & not c in {p} by XBOOLE_0:def 5;
then c in uparrow q by A15,XBOOLE_0:def 3;
hence q <= c by WAYBEL_0:18;
end;
then q is_<=_than (uparrow p)\{p} by LATTICE3:def 8;
then q = "/\"((uparrow p)\{p},L) by A22,YELLOW_0:31;
then "/\"((uparrow p)\{p},L) in (uparrow p)\{p} by A25,A16,XBOOLE_0:def 5;
then ex_min_of (uparrow p)\{p},L by A21,WAYBEL_1:def 4;
hence thesis;
end;
end;
theorem Th21: :: THEOREM 4.19 (ii)
for L be upper-bounded non empty Poset holds not Top L in Irr L
proof
let L be upper-bounded non empty Poset;
assume Top L in Irr L;
then Top L is completely-irreducible by Def4;
then "/\" ((uparrow Top L)\{Top L},L) <> Top L by Th19;
then "/\" ({Top L}\{Top L},L) <> Top L by WAYBEL_4:24;
then "/\" ({},L) <> Top L by XBOOLE_1:37;
hence contradiction by YELLOW_0:def 12;
end;
theorem Th22: :: THEOREM 4.19 (iii)
for L be Semilattice holds Irr L c= IRR L
proof
let L be Semilattice;
let x be object;
assume
A1: x in Irr L;
then reconsider x1 = x as Element of L;
x1 is completely-irreducible by A1,Def4;
then consider q be Element of L such that
A2: x1 < q and
A3: for s be Element of L st x1 < s holds q <= s and
uparrow x1 = {x1} \/ uparrow q by Th20;
now
let a,b be Element of L;
assume that
A4: x1 = a "/\" b and
A5: a <> x1 and
A6: b <> x1;
x1 <= b by A4,YELLOW_0:23;
then x1 < b by A6,ORDERS_2:def 6;
then
A7: q <= b by A3;
A8: x1 <= q by A2,ORDERS_2:def 6;
x1 <= a by A4,YELLOW_0:23;
then x1 < a by A5,ORDERS_2:def 6;
then q <= a by A3;
then q <= x1 by A4,A7,YELLOW_0:23;
hence contradiction by A2,A8,ORDERS_2:2;
end;
then x1 is irreducible by WAYBEL_6:def 2;
hence thesis by WAYBEL_6:def 4;
end;
theorem Th23:
for L be Semilattice for x be Element of L holds x is
completely-irreducible implies x is irreducible
proof
let L be Semilattice;
let x be Element of L;
assume x is completely-irreducible;
then
A1: x in Irr L by Def4;
Irr L c= IRR L by Th22;
hence thesis by A1,WAYBEL_6:def 4;
end;
theorem Th24:
for L be non empty Poset for x be Element of L holds x is
completely-irreducible implies for X be Subset of L st ex_inf_of X,L & x = inf
X holds x in X
proof
let L be non empty Poset;
let x be Element of L;
assume x is completely-irreducible;
then consider q be Element of L such that
A1: x < q and
A2: for s be Element of L st x < s holds q <= s and
uparrow x = {x} \/ uparrow q by Th20;
let X be Subset of L;
assume that
A3: ex_inf_of X,L and
A4: x = inf X and
A5: not x in X;
A6: X c= uparrow q
proof
let y be object;
assume
A7: y in X;
then reconsider y1 = y as Element of L;
inf X is_<=_than X by A3,YELLOW_0:31;
then x <= y1 by A4,A7,LATTICE3:def 8;
then x < y1 by A5,A7,ORDERS_2:def 6;
then q <= y1 by A2;
hence thesis by WAYBEL_0:18;
end;
ex_inf_of uparrow q,L by WAYBEL_0:39;
then inf (uparrow q) <= inf X by A3,A6,YELLOW_0:35;
then q <= x by A4,WAYBEL_0:39;
hence contradiction by A1,ORDERS_2:6;
end;
theorem Th25: :: REMARK 4.20
for L be non empty Poset for X be Subset of L st X is
order-generating holds Irr L c= X
proof
let L be non empty Poset;
let X be Subset of L;
assume
A1: X is order-generating;
let x be object;
assume
A2: x in Irr L;
then reconsider x1 = x as Element of L;
A3: x1 = "/\" ((uparrow x1) /\ X,L) & ex_inf_of (uparrow x1) /\ X,L by A1,
WAYBEL_6:def 5;
x1 is completely-irreducible by A2,Def4;
then x1 in (uparrow x1) /\ X by A3,Th24;
hence thesis by XBOOLE_0:def 4;
end;
theorem Th26: :: PROPOSITION 4.21 (i)
for L be complete LATTICE for p be Element of L holds (ex k be
Element of L st p is_maximal_in (the carrier of L) \ uparrow k) implies p is
completely-irreducible
proof
let L be complete LATTICE;
let p be Element of L;
given k be Element of L such that
A1: p is_maximal_in (the carrier of L) \ uparrow k;
k <= p "\/" k by YELLOW_0:22;
then
A2: p "\/" k in uparrow k by WAYBEL_0:18;
p <= p "\/" k by YELLOW_0:22;
then p "\/" k in uparrow p by WAYBEL_0:18;
then
A3: ex_inf_of (uparrow p) \ {p},L & p "\/" k in (uparrow p) /\ (uparrow k)
by A2,XBOOLE_0:def 4,YELLOW_0:17;
A4: (uparrow p) \ {p} = (uparrow p) /\ (uparrow k) by A1,Th3;
then "/\" ((uparrow p) \ {p},L) = p "\/" k by Th1;
then ex_min_of (uparrow p) \ {p},L by A4,A3,WAYBEL_1:def 4;
hence thesis;
end;
theorem Th27:
for L be transitive antisymmetric with_suprema RelStr for p,q,u
be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & not
u <= p holds p "\/" u = q "\/" u
proof
let L be transitive antisymmetric with_suprema RelStr;
let p,q,u be Element of L;
assume that
A1: p < q and
A2: for s be Element of L st p < s holds q <= s and
A3: not u <= p;
A4: q "\/" u >= q by YELLOW_0:22;
A5: now
let v be Element of L;
assume that
A6: v >= p and
A7: v >= u;
v > p by A3,A6,A7,ORDERS_2:def 6;
then v >= q by A2;
hence q "\/" u <= v by A7,YELLOW_0:22;
end;
p <= q by A1,ORDERS_2:def 6;
then
A8: q "\/" u >= p by A4,ORDERS_2:3;
q "\/" u >= u by YELLOW_0:22;
hence thesis by A8,A5,YELLOW_0:22;
end;
theorem Th28:
for L be distributive LATTICE for p,q,u be Element of L st p < q
& (for s be Element of L st p < s holds q <= s) & not u <= p holds not u "/\" q
<= p
proof
let L be distributive LATTICE;
let p,q,u be Element of L;
assume that
A1: p < q and
A2: ( for s be Element of L st p < s holds q <= s)& not u <= p and
A3: u "/\" q <= p;
A4: p <= q by A1,ORDERS_2:def 6;
p = p "\/" (u "/\" q) by A3,YELLOW_0:24
.= (p "\/" u) "/\" (q "\/" p) by WAYBEL_1:5
.= (p "\/" u) "/\" q by A4,YELLOW_0:24
.= q "/\" (q "\/" u) by A1,A2,Th27
.= q by LATTICE3:18;
hence contradiction by A1;
end;
theorem Th29:
for L be distributive complete LATTICE st L opp is
meet-continuous for p be Element of L st p is completely-irreducible holds (the
carrier of L) \ downarrow p is Open Filter of L
proof
let L be distributive complete LATTICE;
assume
A1: L opp is meet-continuous;
let p be Element of L;
assume
A2: p is completely-irreducible;
then consider q be Element of L such that
A3: p < q and
A4: for s be Element of L st p < s holds q <= s and
uparrow p = {p} \/ uparrow q by Th20;
defpred P[Element of L] means $1 <= q & not $1 <= p;
reconsider F = { t where t is Element of L : P[t]} as Subset of L from
DOMAIN_1:sch 7;
not q <= p by A3,ORDERS_2:6;
then
A5: q in F;
A6: now
let x,y be Element of L;
assume that
A7: x in F and
A8: y in F;
A9: ex x1 be Element of L st x1 = x & x1 <= q & not x1 <= p by A7;
take z = x "/\" y;
A10: z <= x by YELLOW_0:23;
A11: ex y1 be Element of L st y1 = y & y1 <= q & not y1 <= p by A8;
A12: not z <= p
proof
A13: now
let d be Element of L;
assume d >= y & d >= p;
then d > p by A11,ORDERS_2:def 6;
hence q <= d by A4;
end;
assume
A14: z <= p;
A15: q >= p by A3,ORDERS_2:def 6;
x = x "/\" q by A9,YELLOW_0:25
.= x "/\" (y "\/" p) by A11,A15,A13,YELLOW_0:22
.= z "\/" (x "/\" p) by WAYBEL_1:def 3
.= (x "\/" z) "/\" (z "\/" p) by WAYBEL_1:5
.= x "/\" (p "\/" z) by A10,YELLOW_0:24
.= x "/\" p by A14,YELLOW_0:24;
hence contradiction by A9,YELLOW_0:25;
end;
z <= q by A9,A10,ORDERS_2:3;
hence z in F by A12;
thus z <= x by YELLOW_0:23;
thus z <= y by YELLOW_0:23;
end;
p is irreducible by A2,Th23;
then
A16: p is prime by WAYBEL_6:27;
not Top L in Irr L by Th21;
then p <> Top L by A2,Def4;
then (downarrow p)` is Filter of L by A16,WAYBEL_6:26;
then reconsider V = (the carrier of L) \ downarrow p as Filter of L by
SUBSET_1:def 4;
reconsider F as non empty filtered Subset of L by A5,A6,WAYBEL_0:def 2;
reconsider F1 = F as non empty directed Subset of L opp by YELLOW_7:27;
now
let x be Element of L;
assume
A17: x in V;
take y = inf F;
thus y in V
proof
now
let r be Element of L;
assume r in {p} "\/" F;
then r in {p "\/" v where v is Element of L : v in F} by YELLOW_4:15;
then consider v be Element of L such that
A18: r = p "\/" v and
A19: v in F;
ex v1 be Element of L st v = v1 & v1 <= q & not v1 <= p by A19;
then
A20: p <> r by A18,YELLOW_0:24;
p <= r by A18,YELLOW_0:22;
then p < r by A20,ORDERS_2:def 6;
hence q <= r by A4;
end;
then
A21: q is_<=_than {p} "\/" F by LATTICE3:def 8;
A22: ex_inf_of {p~} "/\" F1,L by YELLOW_0:17;
ex_inf_of F,L by YELLOW_0:17;
then
A23: inf F = sup F1 by YELLOW_7:13;
A24: {p~} = {p} by LATTICE3:def 6;
assume not y in V;
then y in downarrow p by XBOOLE_0:def 5;
then y <= p by WAYBEL_0:17;
then p = p "\/" y by YELLOW_0:24
.= p~ "/\" (inf F)~ by YELLOW_7:23
.= p~ "/\" sup F1 by A23,LATTICE3:def 6
.= sup ({p~} "/\" F1) by A1,WAYBEL_2:def 6
.= "/\"({p~} "/\" F1,L) by A22,YELLOW_7:13
.= "/\"({p} "\/" F,L) by A24,Th5;
then q <= p by A21,YELLOW_0:33;
hence contradiction by A3,ORDERS_2:6;
end;
then not y in downarrow p by XBOOLE_0:def 5;
then
A25: not y <= p by WAYBEL_0:17;
now
let D be non empty directed Subset of L;
assume
A26: y <= sup D;
D \ downarrow p is non empty
proof
assume D \ downarrow p is empty;
then D c= downarrow p by XBOOLE_1:37;
then sup D <= sup (downarrow p) by WAYBEL_7:1;
then y <= sup (downarrow p) by A26,ORDERS_2:3;
hence contradiction by A25,WAYBEL_0:34;
end;
then consider d be object such that
A27: d in D \ downarrow p;
reconsider d as Element of L by A27;
take d;
thus d in D by A27,XBOOLE_0:def 5;
not d in downarrow p by A27,XBOOLE_0:def 5;
then not d <= p by WAYBEL_0:17;
then d "/\" q <= q & not d "/\" q <= p by A3,A4,Th28,YELLOW_0:23;
then y is_<=_than F & d "/\" q in F by YELLOW_0:33;
then d "/\" q <= d & y <= d "/\" q by LATTICE3:def 8,YELLOW_0:23;
hence y <= d by ORDERS_2:3;
end;
then
A28: y << y by WAYBEL_3:def 1;
not x in downarrow p by A17,XBOOLE_0:def 5;
then not x <= p by WAYBEL_0:17;
then x "/\" q <= q & not x "/\" q <= p by A3,A4,Th28,YELLOW_0:23;
then y is_<=_than F & x "/\" q in F by YELLOW_0:33;
then x "/\" q <= x & y <= x "/\" q by LATTICE3:def 8,YELLOW_0:23;
then y <= x by ORDERS_2:3;
hence y << x by A28,WAYBEL_3:2;
end;
hence thesis by WAYBEL_6:def 1;
end;
theorem :: PROPOSITION 4.21 (ii)
for L be distributive complete LATTICE st L opp is meet-continuous for
p be Element of L holds p is completely-irreducible implies ex k be Element of
L st k in the carrier of CompactSublatt L & p is_maximal_in (the carrier of L)
\ uparrow k
proof
let L be distributive complete LATTICE;
assume
A1: L opp is meet-continuous;
let p be Element of L;
assume
A2: p is completely-irreducible;
then reconsider
V = (the carrier of L) \ downarrow p as Open Filter of L by A1,Th29;
now
let b be Element of L;
assume b in (uparrow p) \ {p};
then b in uparrow p by XBOOLE_0:def 5;
hence p <= b by WAYBEL_0:18;
end;
then p is_<=_than (uparrow p) \ {p} by LATTICE3:def 8;
then
A3: p <= "/\"((uparrow p) \ {p},L) by YELLOW_0:33;
"/\"((uparrow p) \ {p},L) <> p by A2,Th19;
then
A4: p < "/\"((uparrow p) \ {p},L) by A3,ORDERS_2:def 6;
A5: ex_inf_of V,L & (inf V)~ = inf V by LATTICE3:def 6,YELLOW_0:17;
take k = inf V;
reconsider V9 = V as non empty directed Subset of L opp by YELLOW_7:27;
A6: ex_inf_of {p~} "/\" V9,L by YELLOW_0:17;
A7: ex_inf_of {p} "\/" V,L & ex_inf_of (uparrow p) \ {p},L by YELLOW_0:17;
A8: {p} "\/" V c= (uparrow p) \ {p}
proof
let x be object;
assume x in {p} "\/" V;
then x in {p "\/" v where v is Element of L: v in V} by YELLOW_4:15;
then consider v be Element of L such that
A9: x = p "\/" v and
A10: v in V;
not v in downarrow p by A10,XBOOLE_0:def 5;
then not v <= p by WAYBEL_0:17;
then p "\/" v <> p by YELLOW_0:22;
then
A11: not p "\/" v in {p} by TARSKI:def 1;
p <= p "\/" v by YELLOW_0:22;
then p "\/" v in uparrow p by WAYBEL_0:18;
hence thesis by A9,A11,XBOOLE_0:def 5;
end;
A12: p = p~ by LATTICE3:def 6;
p "\/" k = (p~) "/\" (inf V)~ by YELLOW_7:23
.= (p~) "/\" "\/"(V,L opp) by A5,YELLOW_7:13
.= "\/"({p~} "/\" V9,L opp) by A1,WAYBEL_2:def 6
.= "/\"({p~} "/\" V9,L) by A6,YELLOW_7:13
.= inf ({p} "\/" V) by A12,Th5;
then
A13: "/\"((uparrow p) \ {p},L) <= p "\/" k by A7,A8,YELLOW_0:35;
A14: not k <= p
proof
assume k <= p;
then p "\/" k = p by YELLOW_0:24;
hence contradiction by A13,A4,ORDERS_2:7;
end;
uparrow k = V
proof
thus uparrow k c= V
proof
let x be object;
assume
A15: x in uparrow k;
then reconsider x1 = x as Element of L;
k <= x1 by A15,WAYBEL_0:18;
then not x1 <= p by A14,ORDERS_2:3;
then not x1 in downarrow p by WAYBEL_0:17;
hence thesis by XBOOLE_0:def 5;
end;
let x be object;
assume
A16: x in V;
then reconsider x1 = x as Element of L;
k is_<=_than V by YELLOW_0:33;
then k <= x1 by A16,LATTICE3:def 8;
hence thesis by WAYBEL_0:18;
end;
then k is compact by WAYBEL_8:2;
hence k in the carrier of CompactSublatt L by WAYBEL_8:def 1;
A17: not ex y be Element of L st y in (the carrier of L) \ uparrow k & p < y
proof
given y be Element of L such that
A18: y in (the carrier of L) \ uparrow k and
A19: p < y;
not y in uparrow k by A18,XBOOLE_0:def 5;
then k is_<=_than V & not k <= y by WAYBEL_0:18,YELLOW_0:33;
then not y in V by LATTICE3:def 8;
then y in downarrow p by XBOOLE_0:def 5;
then y <= p by WAYBEL_0:17;
hence contradiction by A19,ORDERS_2:6;
end;
not p in uparrow k by A14,WAYBEL_0:18;
then p in (the carrier of L) \ uparrow k by XBOOLE_0:def 5;
hence thesis by A17,WAYBEL_4:55;
end;
theorem Th31: :: THEOREM 4.22
for L be lower-bounded algebraic LATTICE for x,y be Element of L
holds not y <= x implies ex p be Element of L st p is completely-irreducible &
x <= p & not y <= p
proof
let L be lower-bounded algebraic LATTICE;
let x,y be Element of L;
assume
A1: not y <= x;
for z be Element of L holds waybelow z is non empty directed;
then consider k1 be Element of L such that
A2: k1 << y and
A3: not k1 <= x by A1,WAYBEL_3:24;
consider k be Element of L such that
A4: k in the carrier of CompactSublatt L and
A5: k1 <= k and
A6: k <= y by A2,WAYBEL_8:7;
not k <= x by A3,A5,ORDERS_2:3;
then not x in uparrow k by WAYBEL_0:18;
then x in (the carrier of L) \ (uparrow k) by XBOOLE_0:def 5;
then
A7: x in (uparrow k)` by SUBSET_1:def 4;
k is compact by A4,WAYBEL_8:def 1;
then uparrow k is Open Filter of L by WAYBEL_8:2;
then consider p be Element of L such that
A8: x <= p and
A9: p is_maximal_in ((uparrow k)`) by A7,WAYBEL_6:9;
take p;
(the carrier of L) \ uparrow k = (uparrow k)` by SUBSET_1:def 4;
hence p is completely-irreducible by A9,Th26;
thus x <= p by A8;
thus not y <= p
proof
p in (uparrow k)` by A9,WAYBEL_4:55;
then p in (the carrier of L) \ uparrow k by SUBSET_1:def 4;
then
A10: not p in uparrow k by XBOOLE_0:def 5;
assume y <= p;
then k <= p by A6,ORDERS_2:3;
hence contradiction by A10,WAYBEL_0:18;
end;
end;
theorem Th32: :: THEOREM 4.23 (i)
for L be lower-bounded algebraic LATTICE holds Irr L is
order-generating & for X be Subset of L st X is order-generating holds Irr L c=
X
proof
let L be lower-bounded algebraic LATTICE;
now
let x,y be Element of L;
assume not y <= x;
then consider p be Element of L such that
A1: p is completely-irreducible and
A2: x <= p and
A3: not y <= p by Th31;
take p;
thus p in Irr L by A1,Def4;
thus x <= p by A2;
thus not y <= p by A3;
end;
hence Irr L is order-generating by WAYBEL_6:17;
let X be Subset of L;
assume X is order-generating;
hence thesis by Th25;
end;
theorem :: THEOREM 4.23 (ii)
for L be lower-bounded algebraic LATTICE for s be Element of L holds s
= "/\" (uparrow s /\ Irr L,L)
proof
let L be lower-bounded algebraic LATTICE;
let s be Element of L;
Irr L is order-generating by Th32;
hence thesis by WAYBEL_6:def 5;
end;
theorem Th34:
for L be complete non empty Poset for X be Subset of L for p
be Element of L st p is completely-irreducible & p = inf X holds p in X
proof
let L be complete non empty Poset;
let X be Subset of L;
let p be Element of L;
assume that
A1: p is completely-irreducible and
A2: p = inf X;
assume
A3: not p in X;
consider q be Element of L such that
A4: p < q and
A5: for s be Element of L st p < s holds q <= s and
uparrow p = {p} \/ uparrow q by A1,Th20;
A6: p is_<=_than X by A2,YELLOW_0:33;
now
let b be Element of L;
assume
A7: b in X;
then p <= b by A6,LATTICE3:def 8;
then p < b by A3,A7,ORDERS_2:def 6;
hence q <= b by A5;
end;
then
A8: q is_<=_than X by LATTICE3:def 8;
A9: p <= q by A4,ORDERS_2:def 6;
now
let b be Element of L;
assume b is_<=_than X;
then p >= b by A2,YELLOW_0:33;
hence q >= b by A9,ORDERS_2:3;
end;
hence contradiction by A2,A4,A8,YELLOW_0:33;
end;
theorem Th35:
for L be complete algebraic LATTICE for p be Element of L st p
is completely-irreducible holds p = "/\" ({ x where x is Element of L : x in
uparrow p & ex k be Element of L st k in the carrier of CompactSublatt L & x
is_maximal_in (the carrier of L) \ uparrow k },L)
proof
let L be complete algebraic LATTICE;
let p be Element of L;
set A = { x where x is Element of L : x in uparrow p & ex k be Element of L
st k in the carrier of CompactSublatt L & x is_maximal_in (the carrier of L) \
uparrow k };
p <= p;
then
A1: p in uparrow p by WAYBEL_0:18;
now
let a be Element of L;
assume a in A;
then
ex a1 be Element of L st a1 = a & a1 in uparrow p & ex k be Element of
L st k in the carrier of CompactSublatt L & a1 is_maximal_in ( the carrier of L
) \ uparrow k;
hence p <= a by WAYBEL_0:18;
end;
then
A2: p is_<=_than A by LATTICE3:def 8;
assume p is completely-irreducible;
then consider q be Element of L such that
A3: p < q and
A4: for s be Element of L st p < s holds q <= s and
uparrow p = {p} \/ uparrow q by Th20;
A5: compactbelow p <> compactbelow q
proof
assume compactbelow p = compactbelow q;
then p = sup compactbelow q by WAYBEL_8:def 3
.= q by WAYBEL_8:def 3;
hence contradiction by A3;
end;
p <= q by A3,ORDERS_2:def 6;
then compactbelow p c= compactbelow q by WAYBEL13:1;
then not compactbelow q c= compactbelow p by A5;
then consider k1 be object such that
A6: k1 in compactbelow q and
A7: not k1 in compactbelow p;
k1 in { y where y is Element of L: q >= y & y is compact } by A6,
WAYBEL_8:def 2;
then consider k be Element of L such that
A8: k = k1 and
A9: q >= k and
A10: k is compact;
A11: not ex y be Element of L st y in (the carrier of L) \ uparrow k & p < y
proof
given y be Element of L such that
A12: y in (the carrier of L) \ uparrow k and
A13: p < y;
q <= y by A4,A13;
then k <= y by A9,ORDERS_2:3;
then y in uparrow k by WAYBEL_0:18;
hence contradiction by A12,XBOOLE_0:def 5;
end;
not k <= p by A7,A8,A10,WAYBEL_8:4;
then not p in uparrow k by WAYBEL_0:18;
then p in (the carrier of L) \ uparrow k by XBOOLE_0:def 5;
then
A14: p is_maximal_in (the carrier of L) \ uparrow k by A11,WAYBEL_4:55;
k in the carrier of CompactSublatt L by A10,WAYBEL_8:def 1;
then p in A by A1,A14;
then for u be Element of L st u is_<=_than A holds p >= u by LATTICE3:def 8;
hence thesis by A2,YELLOW_0:33;
end;
theorem :: COROLLARY 4.24
for L be complete algebraic LATTICE for p be Element of L holds (ex k
be Element of L st k in the carrier of CompactSublatt L & p is_maximal_in (the
carrier of L) \ uparrow k) iff p is completely-irreducible
proof
let L be complete algebraic LATTICE;
let p be Element of L;
thus (ex k be Element of L st k in the carrier of CompactSublatt L & p
is_maximal_in (the carrier of L) \ uparrow k) implies p is
completely-irreducible by Th26;
thus p is completely-irreducible implies ex k be Element of L st k in the
carrier of CompactSublatt L & p is_maximal_in (the carrier of L) \ uparrow k
proof
defpred P[Element of L] means $1 in uparrow p & ex k be Element of L st k
in the carrier of CompactSublatt L & $1 is_maximal_in (the carrier of L) \
uparrow k;
reconsider A = { x where x is Element of L : P[x]} as Subset of L from
DOMAIN_1:sch 7;
assume
A1: p is completely-irreducible;
then p = inf A by Th35;
then p in A by A1,Th34;
then consider x be Element of L such that
A2: x = p and
x in uparrow p and
A3: ex k be Element of L st k in the carrier of CompactSublatt L & x
is_maximal_in (the carrier of L) \ uparrow k;
consider k be Element of L such that
A4: k in the carrier of CompactSublatt L and
A5: x is_maximal_in (the carrier of L) \ uparrow k by A3;
take k;
thus k in the carrier of CompactSublatt L by A4;
thus thesis by A2,A5;
end;
end;