:: WAYBEL16 semantic presentation
begin
theorem Th1: :: WAYBEL16:1
for L being sup-Semilattice
for x, y being Element of L holds "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y
proof
let L be sup-Semilattice; ::_thesis: for x, y being Element of L holds "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y
let x, y be Element of L; ::_thesis: "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y
(uparrow x) /\ (uparrow y) = uparrow (x "\/" y) by WAYBEL14:4;
hence "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y by WAYBEL_0:39; ::_thesis: verum
end;
theorem :: WAYBEL16:2
for L being Semilattice
for x, y being Element of L holds "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y
proof
let L be Semilattice; ::_thesis: for x, y being Element of L holds "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y
let x, y be Element of L; ::_thesis: "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y
(downarrow x) /\ (downarrow y) = downarrow (x "/\" y) by WAYBEL14:3;
hence "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y by WAYBEL_0:34; ::_thesis: verum
end;
theorem Th3: :: WAYBEL16:3
for L being non empty RelStr
for x, y being 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 ; ::_thesis: for x, y being Element of L st x is_maximal_in the carrier of L \ (uparrow y) holds
(uparrow x) \ {x} = (uparrow x) /\ (uparrow y)
let x, y be Element of L; ::_thesis: ( x is_maximal_in the carrier of L \ (uparrow y) implies (uparrow x) \ {x} = (uparrow x) /\ (uparrow y) )
assume A1: x is_maximal_in the carrier of L \ (uparrow y) ; ::_thesis: (uparrow x) \ {x} = (uparrow x) /\ (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) :: according to XBOOLE_0:def_10 ::_thesis: (uparrow x) /\ (uparrow y) c= (uparrow x) \ {x}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (uparrow x) \ {x} or a in (uparrow x) /\ (uparrow y) )
assume A3: a in (uparrow x) \ {x} ; ::_thesis: a in (uparrow x) /\ (uparrow y)
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 a in (uparrow x) /\ (uparrow y) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (uparrow x) /\ (uparrow y) or a in (uparrow x) \ {x} )
assume A6: a in (uparrow x) /\ (uparrow y) ; ::_thesis: a in (uparrow x) \ {x}
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 a in (uparrow x) \ {x} by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: WAYBEL16:4
for L being non empty RelStr
for x, y being 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 ; ::_thesis: for x, y being Element of L st x is_minimal_in the carrier of L \ (downarrow y) holds
(downarrow x) \ {x} = (downarrow x) /\ (downarrow y)
let x, y be Element of L; ::_thesis: ( x is_minimal_in the carrier of L \ (downarrow y) implies (downarrow x) \ {x} = (downarrow x) /\ (downarrow y) )
assume A1: x is_minimal_in the carrier of L \ (downarrow y) ; ::_thesis: (downarrow x) \ {x} = (downarrow x) /\ (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) :: according to XBOOLE_0:def_10 ::_thesis: (downarrow x) /\ (downarrow y) c= (downarrow x) \ {x}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (downarrow x) \ {x} or a in (downarrow x) /\ (downarrow y) )
assume A3: a in (downarrow x) \ {x} ; ::_thesis: a in (downarrow x) /\ (downarrow y)
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 a in (downarrow x) /\ (downarrow y) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (downarrow x) /\ (downarrow y) or a in (downarrow x) \ {x} )
assume A6: a in (downarrow x) /\ (downarrow y) ; ::_thesis: a in (downarrow x) \ {x}
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 a in (downarrow x) \ {x} by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th5: :: WAYBEL16:5
for L being with_suprema Poset
for X, Y being Subset of L
for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "\/" Y = X9 "/\" Y9
proof
let L be with_suprema Poset; ::_thesis: for X, Y being Subset of L
for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "\/" Y = X9 "/\" Y9
let X, Y be Subset of L; ::_thesis: for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "\/" Y = X9 "/\" Y9
let X9, Y9 be Subset of (L opp); ::_thesis: ( X = X9 & Y = Y9 implies X "\/" Y = X9 "/\" Y9 )
assume A1: ( X = X9 & Y = Y9 ) ; ::_thesis: X "\/" Y = X9 "/\" Y9
thus X "\/" Y c= X9 "/\" Y9 :: according to XBOOLE_0:def_10 ::_thesis: X9 "/\" Y9 c= X "\/" Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X "\/" Y or a in X9 "/\" Y9 )
assume a in X "\/" Y ; ::_thesis: a in X9 "/\" Y9
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 being 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 a in X9 "/\" Y9 by YELLOW_4:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X9 "/\" Y9 or a in X "\/" Y )
assume a in X9 "/\" Y9 ; ::_thesis: a in X "\/" Y
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 being 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 a in X "\/" Y by YELLOW_4:def_3; ::_thesis: verum
end;
theorem :: WAYBEL16:6
for L being with_infima Poset
for X, Y being Subset of L
for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "/\" Y = X9 "\/" Y9
proof
let L be with_infima Poset; ::_thesis: for X, Y being Subset of L
for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "/\" Y = X9 "\/" Y9
let X, Y be Subset of L; ::_thesis: for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "/\" Y = X9 "\/" Y9
let X9, Y9 be Subset of (L opp); ::_thesis: ( X = X9 & Y = Y9 implies X "/\" Y = X9 "\/" Y9 )
assume A1: ( X = X9 & Y = Y9 ) ; ::_thesis: X "/\" Y = X9 "\/" Y9
thus X "/\" Y c= X9 "\/" Y9 :: according to XBOOLE_0:def_10 ::_thesis: X9 "\/" Y9 c= X "/\" Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X "/\" Y or a in X9 "\/" Y9 )
assume a in X "/\" Y ; ::_thesis: a in X9 "\/" Y9
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 being 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 a in X9 "\/" Y9 by YELLOW_4:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X9 "\/" Y9 or a in X "/\" Y )
assume a in X9 "\/" Y9 ; ::_thesis: a in X "/\" Y
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 being 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 a in X "/\" Y by YELLOW_4:def_4; ::_thesis: verum
end;
theorem Th7: :: WAYBEL16:7
for L being non empty reflexive transitive RelStr holds Filt L = Ids (L opp)
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: Filt L = Ids (L opp)
A1: Ids (L opp) c= Filt L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ids (L opp) or x in Filt L )
assume x in Ids (L opp) ; ::_thesis: x in Filt L
then x in { X where X is Ideal of (L opp) : verum } by WAYBEL_0:def_23;
then consider x1 being 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, YELLOW_7:29;
then x in { X where X is Filter of L : verum } by A2;
hence x in Filt L by WAYBEL_0:def_24; ::_thesis: verum
end;
Filt L c= Ids (L opp)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Filt L or x in Ids (L opp) )
assume x in Filt L ; ::_thesis: x in Ids (L opp)
then x in { X where X is Filter of L : verum } by WAYBEL_0:def_24;
then consider x1 being 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, YELLOW_7:29;
then x in { X where X is Ideal of (L opp) : verum } by A3;
hence x in Ids (L opp) by WAYBEL_0:def_23; ::_thesis: verum
end;
hence Filt L = Ids (L opp) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: WAYBEL16:8
for L being non empty reflexive transitive RelStr holds Ids L = Filt (L opp)
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: Ids L = Filt (L opp)
A1: Filt (L opp) c= Ids L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Filt (L opp) or x in Ids L )
assume x in Filt (L opp) ; ::_thesis: x in Ids L
then x in { X where X is Filter of (L opp) : verum } by WAYBEL_0:def_24;
then consider x1 being 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, YELLOW_7:28;
then x in { X where X is Ideal of L : verum } by A2;
hence x in Ids L by WAYBEL_0:def_23; ::_thesis: verum
end;
Ids L c= Filt (L opp)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ids L or x in Filt (L opp) )
assume x in Ids L ; ::_thesis: x in Filt (L opp)
then x in { X where X is Ideal of L : verum } by WAYBEL_0:def_23;
then consider x1 being 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, YELLOW_7:28;
then x in { X where X is Filter of (L opp) : verum } by A3;
hence x in Filt (L opp) by WAYBEL_0:def_24; ::_thesis: verum
end;
hence Ids L = Filt (L opp) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
definition
let S, T be non empty complete Poset;
mode CLHomomorphism of S,T -> Function of S,T means :: WAYBEL16:def 1
( it is directed-sups-preserving & it is infs-preserving );
existence
ex b1 being Function of S,T st
( b1 is directed-sups-preserving & b1 is infs-preserving )
proof
reconsider f = the carrier of S --> (Top T) as Function of the carrier of S, the carrier of T ;
reconsider f = f as Function of S,T ;
take f ; ::_thesis: ( f is directed-sups-preserving & f is infs-preserving )
now__::_thesis:_for_X_being_Subset_of_S_st_not_X_is_empty_&_X_is_directed_holds_
f_preserves_sup_of_X
let X be Subset of S; ::_thesis: ( not X is empty & X is directed implies f preserves_sup_of X )
assume A1: ( not X is empty & X is directed ) ; ::_thesis: f preserves_sup_of X
now__::_thesis:_(_ex_sup_of_X,S_implies_(_ex_sup_of_f_.:_X,T_&_sup_(f_.:_X)_=_f_._(sup_X)_)_)
assume ex_sup_of X,S ; ::_thesis: ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) )
rng f = {(Top T)} by FUNCOP_1:8;
then A2: f .: X c= {(Top T)} by RELAT_1:111;
now__::_thesis:_for_x,_y_being_Element_of_S_st_x_<=_y_holds_
f_._x_<=_f_._y
let x, y be Element of S; ::_thesis: ( x <= y implies f . x <= f . y )
assume x <= y ; ::_thesis: f . x <= f . y
f . x = Top T by FUNCOP_1:7
.= f . y by FUNCOP_1:7 ;
hence f . x <= f . y ; ::_thesis: verum
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; ::_thesis: sup (f .: X) = f . (sup X)
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; ::_thesis: verum
end;
hence f preserves_sup_of X by WAYBEL_0:def_31; ::_thesis: verum
end;
hence f is directed-sups-preserving by WAYBEL_0:def_37; ::_thesis: f is infs-preserving
now__::_thesis:_for_X_being_Subset_of_S_holds_f_preserves_inf_of_X
let X be Subset of S; ::_thesis: f preserves_inf_of X
now__::_thesis:_(_ex_inf_of_X,S_implies_(_ex_inf_of_f_.:_X,T_&_inf_(f_.:_X)_=_f_._(inf_X)_)_)
assume ex_inf_of X,S ; ::_thesis: ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) )
thus ex_inf_of f .: X,T by YELLOW_0:17; ::_thesis: inf (f .: X) = f . (inf X)
rng f = {(Top T)} by FUNCOP_1:8;
then A4: f .: X is Subset of {(Top T)} by RELAT_1:111;
now__::_thesis:_inf_(f_.:_X)_=_f_._(inf_X)
percases ( f .: X = {} or f .: X <> {} ) ;
suppose f .: X = {} ; ::_thesis: inf (f .: X) = f . (inf X)
hence inf (f .: X) = Top T by YELLOW_0:def_12
.= f . (inf X) by FUNCOP_1:7 ;
::_thesis: verum
end;
suppose f .: X <> {} ; ::_thesis: inf (f .: X) = f . (inf 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 ;
::_thesis: verum
end;
end;
end;
hence inf (f .: X) = f . (inf X) ; ::_thesis: verum
end;
hence f preserves_inf_of X by WAYBEL_0:def_30; ::_thesis: verum
end;
hence f is infs-preserving by WAYBEL_0:def_32; ::_thesis: verum
end;
end;
:: deftheorem defines CLHomomorphism WAYBEL16:def_1_:_
for S, T being non empty complete Poset
for b3 being Function of S,T holds
( b3 is CLHomomorphism of S,T iff ( b3 is directed-sups-preserving & b3 is infs-preserving ) );
definition
let S be non empty complete continuous Poset;
let A be Subset of S;
predA is_FG_set means :: WAYBEL16:def 2
for T being non empty complete continuous Poset
for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) );
end;
:: deftheorem defines is_FG_set WAYBEL16:def_2_:_
for S being non empty complete continuous Poset
for A being Subset of S holds
( A is_FG_set iff for T being non empty complete continuous Poset
for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) ) );
registration
let L be non empty upper-bounded Poset;
cluster Filt L -> non empty ;
coherence
not Filt L is empty
proof
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_{(Top_L)}_&_x_<=_y_holds_
y_in_{(Top_L)}
let x, y be Element of L; ::_thesis: ( x in {(Top L)} & x <= y implies y in {(Top L)} )
assume that
A1: x in {(Top L)} and
A2: x <= y ; ::_thesis: y in {(Top L)}
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; ::_thesis: verum
end;
then {(Top L)} is Filter of L by WAYBEL_0:5, WAYBEL_0:def_20;
then {(Top L)} in { Y where Y is Filter of L : verum } ;
hence not Filt L is empty by WAYBEL_0:def_24; ::_thesis: verum
end;
end;
theorem Th9: :: WAYBEL16:9
for X being set
for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds meet Y is Filter of (BoolePoset X)
proof
let X be set ; ::_thesis: for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds meet Y is Filter of (BoolePoset X)
set L = BoolePoset X;
let Y be non empty Subset of (InclPoset (Filt (BoolePoset X))); ::_thesis: meet Y is Filter of (BoolePoset X)
A1: now__::_thesis:_for_Z_being_set_st_Z_in_Y_holds_
Top_(BoolePoset_X)_in_Z
let Z be set ; ::_thesis: ( Z in Y implies Top (BoolePoset X) in Z )
assume Z in Y ; ::_thesis: Top (BoolePoset X) in Z
then Z in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then Z in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
then Z in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def_24;
then ex Z1 being Filter of (BoolePoset X) st Z1 = Z ;
hence Top (BoolePoset X) in Z by WAYBEL_4:22; ::_thesis: verum
end;
Y c= the carrier of (InclPoset (Filt (BoolePoset X))) ;
then A2: Y c= the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
A3: for Z being Subset of (BoolePoset X) st Z in Y holds
Z is upper
proof
let Z be Subset of (BoolePoset X); ::_thesis: ( Z in Y implies Z is upper )
assume Z in Y ; ::_thesis: Z is upper
then Z in Filt (BoolePoset X) by A2;
then Z in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def_24;
then ex Z1 being Filter of (BoolePoset X) st Z1 = Z ;
hence Z is upper ; ::_thesis: verum
end;
A4: now__::_thesis:_for_V_being_Subset_of_(BoolePoset_X)_st_V_in_Y_holds_
(_V_is_upper_&_V_is_filtered_)
let V be Subset of (BoolePoset X); ::_thesis: ( V in Y implies ( V is upper & V is filtered ) )
assume V in Y ; ::_thesis: ( V is upper & V is filtered )
then V in Filt (BoolePoset X) by A2;
then V in { Z where Z is Filter of (BoolePoset X) : verum } by WAYBEL_0:def_24;
then A5: ex V1 being Filter of (BoolePoset X) st V1 = V ;
hence V is upper ; ::_thesis: V is filtered
thus V is filtered by A5; ::_thesis: verum
end;
Y c= bool the carrier of (BoolePoset X)
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in Y or v in bool the carrier of (BoolePoset X) )
assume v in Y ; ::_thesis: v in bool the carrier of (BoolePoset X)
then v in Filt (BoolePoset X) by A2;
then v in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def_24;
then ex v1 being Filter of (BoolePoset X) st v1 = v ;
hence v in bool the carrier of (BoolePoset X) ; ::_thesis: verum
end;
hence meet Y is Filter of (BoolePoset X) by A1, A3, A4, SETFAM_1:def_1, YELLOW_2:37, YELLOW_2:39; ::_thesis: verum
end;
theorem :: WAYBEL16:10
for X being set
for Y being 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 ; ::_thesis: for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds
( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y )
set L = InclPoset (Filt (BoolePoset X));
let Y be non empty Subset of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y )
meet Y is Filter of (BoolePoset X) by Th9;
then meet Y in { Z where Z is Filter of (BoolePoset X) : verum } ;
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 (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def_1;
A1: for b being Element of (InclPoset (Filt (BoolePoset X))) st b is_<=_than Y holds
b <= a
proof
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b is_<=_than Y implies b <= a )
assume A2: b is_<=_than Y ; ::_thesis: b <= a
now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
b_c=_x
let x be set ; ::_thesis: ( x in Y implies b c= x )
assume A3: x in Y ; ::_thesis: b c= x
then reconsider x9 = x as Element of (InclPoset (Filt (BoolePoset X))) ;
b <= x9 by A2, A3, LATTICE3:def_8;
hence b c= x by YELLOW_1:3; ::_thesis: verum
end;
then b c= meet Y by SETFAM_1:5;
hence b <= a by YELLOW_1:3; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_(InclPoset_(Filt_(BoolePoset_X)))_st_b_in_Y_holds_
a_<=_b
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b in Y implies a <= b )
assume b in Y ; ::_thesis: a <= b
then meet Y c= b by SETFAM_1:3;
hence a <= b by YELLOW_1:3; ::_thesis: verum
end;
then a is_<=_than Y by LATTICE3:def_8;
hence ( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y ) by A1, YELLOW_0:31; ::_thesis: verum
end;
theorem Th11: :: WAYBEL16:11
for X being set holds bool X is Filter of (BoolePoset X)
proof
let X be set ; ::_thesis: bool X is Filter of (BoolePoset X)
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__::_thesis:_for_x,_y_being_set_st_x_in_A_&_y_in_A_holds_
x_/\_y_in_A
let x, y be set ; ::_thesis: ( x in A & y in A implies x /\ y in A )
assume ( x in A & y in A ) ; ::_thesis: x /\ y in A
then x /\ y c= X /\ X by XBOOLE_1:27;
hence x /\ y in A ; ::_thesis: verum
end;
for x, y being set st x c= y & y c= X & x in A holds
y in A ;
then A is upper by WAYBEL_7:7;
hence bool X is Filter of (BoolePoset X) by A1, WAYBEL_7:9; ::_thesis: verum
end;
theorem Th12: :: WAYBEL16:12
for X being set holds {X} is Filter of (BoolePoset X)
proof
let X be set ; ::_thesis: {X} is Filter of (BoolePoset X)
now__::_thesis:_for_c_being_set_st_c_in_{X}_holds_
c_in_the_carrier_of_(BoolePoset_X)
let c be set ; ::_thesis: ( c in {X} implies c in the carrier of (BoolePoset X) )
assume c in {X} ; ::_thesis: c in the carrier of (BoolePoset 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) ; ::_thesis: verum
end;
then reconsider A = {X} as non empty Subset of (BoolePoset X) by TARSKI:def_3;
for x, y being set st x c= y & y c= X & x in A holds
y in A
proof
let x, y be set ; ::_thesis: ( x c= y & y c= X & x in A implies y in A )
assume that
A1: ( x c= y & y c= X ) and
A2: x in A ; ::_thesis: y in A
x = X by A2, TARSKI:def_1;
then y = X by A1, XBOOLE_0:def_10;
hence y in A by TARSKI:def_1; ::_thesis: verum
end;
then A3: A is upper by WAYBEL_7:7;
now__::_thesis:_for_x,_y_being_set_st_x_in_A_&_y_in_A_holds_
x_/\_y_in_A
let x, y be set ; ::_thesis: ( x in A & y in A implies x /\ y in A )
assume ( x in A & y in A ) ; ::_thesis: x /\ y in A
then ( x = X & y = X ) by TARSKI:def_1;
hence x /\ y in A by TARSKI:def_1; ::_thesis: verum
end;
hence {X} is Filter of (BoolePoset X) by A3, WAYBEL_7:9; ::_thesis: verum
end;
theorem :: WAYBEL16:13
for X being set holds InclPoset (Filt (BoolePoset X)) is upper-bounded
proof
let X be set ; ::_thesis: InclPoset (Filt (BoolePoset X)) is upper-bounded
set L = InclPoset (Filt (BoolePoset X));
bool X is Filter of (BoolePoset X) by Th11;
then bool X in { Z where Z is Filter of (BoolePoset X) : verum } ;
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 (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def_1;
now__::_thesis:_for_b_being_Element_of_(InclPoset_(Filt_(BoolePoset_X)))_st_b_in_the_carrier_of_(InclPoset_(Filt_(BoolePoset_X)))_holds_
b_<=_x
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b in the carrier of (InclPoset (Filt (BoolePoset X))) implies b <= x )
assume b in the carrier of (InclPoset (Filt (BoolePoset X))) ; ::_thesis: b <= x
then b in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
then b in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def_24;
then ex b1 being 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; ::_thesis: verum
end;
then x is_>=_than the carrier of (InclPoset (Filt (BoolePoset X))) by LATTICE3:def_9;
hence InclPoset (Filt (BoolePoset X)) is upper-bounded by YELLOW_0:def_5; ::_thesis: verum
end;
theorem :: WAYBEL16:14
for X being set holds InclPoset (Filt (BoolePoset X)) is lower-bounded
proof
let X be set ; ::_thesis: InclPoset (Filt (BoolePoset X)) is lower-bounded
set L = InclPoset (Filt (BoolePoset X));
{X} is Filter of (BoolePoset X) by Th12;
then {X} in { Z where Z is Filter of (BoolePoset X) : verum } ;
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 (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def_1;
now__::_thesis:_for_b_being_Element_of_(InclPoset_(Filt_(BoolePoset_X)))_st_b_in_the_carrier_of_(InclPoset_(Filt_(BoolePoset_X)))_holds_
x_<=_b
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b in the carrier of (InclPoset (Filt (BoolePoset X))) implies x <= b )
assume b in the carrier of (InclPoset (Filt (BoolePoset X))) ; ::_thesis: x <= b
then b in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
then b in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def_24;
then consider b1 being Filter of (BoolePoset X) such that
A1: b1 = b ;
consider d being set such that
A2: d in b1 by XBOOLE_0:def_1;
A3: d c= X by A2, WAYBEL_8:26;
now__::_thesis:_for_c_being_set_st_c_in_{X}_holds_
c_in_b
let c be set ; ::_thesis: ( c in {X} implies c in b )
assume c in {X} ; ::_thesis: c in b
then c = X by TARSKI:def_1;
hence c in b by A1, A2, A3, WAYBEL_7:7; ::_thesis: verum
end;
then {X} c= b by TARSKI:def_3;
hence x <= b by YELLOW_1:3; ::_thesis: verum
end;
then x is_<=_than the carrier of (InclPoset (Filt (BoolePoset X))) by LATTICE3:def_8;
hence InclPoset (Filt (BoolePoset X)) is lower-bounded by YELLOW_0:def_4; ::_thesis: verum
end;
theorem :: WAYBEL16:15
for X being set holds Top (InclPoset (Filt (BoolePoset X))) = bool X
proof
let X be set ; ::_thesis: Top (InclPoset (Filt (BoolePoset X))) = bool X
set L = InclPoset (Filt (BoolePoset X));
bool X is Filter of (BoolePoset X) by Th11;
then bool X in { Z where Z is Filter of (BoolePoset X) : verum } ;
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 (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def_1;
A1: for b being Element of (InclPoset (Filt (BoolePoset X))) st b is_<=_than {} holds
bX >= b
proof
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b is_<=_than {} implies bX >= b )
assume b is_<=_than {} ; ::_thesis: bX >= b
b in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then b in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
then b in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def_24;
then ex b1 being 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 bX >= b by YELLOW_1:3; ::_thesis: verum
end;
bX is_<=_than {} by YELLOW_0:6;
then "/\" ({},(InclPoset (Filt (BoolePoset X)))) = bool X by A1, YELLOW_0:31;
hence Top (InclPoset (Filt (BoolePoset X))) = bool X by YELLOW_0:def_12; ::_thesis: verum
end;
theorem :: WAYBEL16:16
for X being set holds Bottom (InclPoset (Filt (BoolePoset X))) = {X}
proof
let X be set ; ::_thesis: Bottom (InclPoset (Filt (BoolePoset X))) = {X}
set L = InclPoset (Filt (BoolePoset X));
{X} is Filter of (BoolePoset X) by Th12;
then {X} in { Z where Z is Filter of (BoolePoset X) : verum } ;
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 (InclPoset (Filt (BoolePoset X))) by YELLOW_1:def_1;
A1: for b being Element of (InclPoset (Filt (BoolePoset X))) st b is_>=_than {} holds
bX <= b
proof
let b be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: ( b is_>=_than {} implies bX <= b )
assume b is_>=_than {} ; ::_thesis: bX <= b
b in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then b in the carrier of RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
then b in { V where V is Filter of (BoolePoset X) : verum } by WAYBEL_0:def_24;
then consider b1 being Filter of (BoolePoset X) such that
A2: b1 = b ;
consider d being set such that
A3: d in b1 by XBOOLE_0:def_1;
A4: d c= X by A3, WAYBEL_8:26;
now__::_thesis:_for_c_being_set_st_c_in_{X}_holds_
c_in_b
let c be set ; ::_thesis: ( c in {X} implies c in b )
assume c in {X} ; ::_thesis: c in b
then c = X by TARSKI:def_1;
hence c in b by A2, A3, A4, WAYBEL_7:7; ::_thesis: verum
end;
then {X} c= b by TARSKI:def_3;
hence bX <= b by YELLOW_1:3; ::_thesis: verum
end;
bX is_>=_than {} by YELLOW_0:6;
then "\/" ({},(InclPoset (Filt (BoolePoset X)))) = {X} by A1, YELLOW_0:30;
hence Bottom (InclPoset (Filt (BoolePoset X))) = {X} by YELLOW_0:def_11; ::_thesis: verum
end;
theorem :: WAYBEL16:17
for X being non empty set
for Y being 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 ; ::_thesis: for Y being non empty Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds
union Y c= sup Y
let Y be non empty Subset of (InclPoset X); ::_thesis: ( ex_sup_of Y, InclPoset X implies union Y c= sup Y )
assume A1: ex_sup_of Y, InclPoset X ; ::_thesis: union Y c= sup Y
now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
x_c=_sup_Y
let x be set ; ::_thesis: ( x in Y implies x c= sup Y )
assume A2: x in Y ; ::_thesis: x c= sup 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; ::_thesis: verum
end;
hence union Y c= sup Y by ZFMISC_1:76; ::_thesis: verum
end;
theorem Th18: :: WAYBEL16:18
for L being upper-bounded Semilattice holds InclPoset (Filt L) is complete
proof
let L be upper-bounded Semilattice; ::_thesis: InclPoset (Filt L) is complete
InclPoset (Ids (L opp)) is complete ;
hence InclPoset (Filt L) is complete by Th7; ::_thesis: verum
end;
registration
let L be upper-bounded Semilattice;
cluster InclPoset (Filt L) -> complete ;
coherence
InclPoset (Filt L) is complete by Th18;
end;
begin
definition
let L be non empty RelStr ;
let p be Element of L;
attrp is completely-irreducible means :Def3: :: WAYBEL16:def 3
ex_min_of (uparrow p) \ {p},L;
end;
:: deftheorem Def3 defines completely-irreducible WAYBEL16:def_3_:_
for L being non empty RelStr
for p being Element of L holds
( p is completely-irreducible iff ex_min_of (uparrow p) \ {p},L );
theorem Th19: :: WAYBEL16:19
for L being non empty RelStr
for p being Element of L st p is completely-irreducible holds
"/\" (((uparrow p) \ {p}),L) <> p
proof
let L be non empty RelStr ; ::_thesis: for p being Element of L st p is completely-irreducible holds
"/\" (((uparrow p) \ {p}),L) <> p
let p be Element of L; ::_thesis: ( p is completely-irreducible implies "/\" (((uparrow p) \ {p}),L) <> p )
assume p is completely-irreducible ; ::_thesis: "/\" (((uparrow p) \ {p}),L) <> p
then ex_min_of (uparrow p) \ {p},L by Def3;
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 "/\" (((uparrow p) \ {p}),L) <> p by TARSKI:def_1; ::_thesis: verum
end;
definition
let L be non empty RelStr ;
func Irr L -> Subset of L means :Def4: :: WAYBEL16:def 4
for x being Element of L holds
( x in it iff x is completely-irreducible );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is completely-irreducible )
proof
defpred S1[ Element of L] means $1 is completely-irreducible ;
consider X being Subset of L such that
A1: for x being Element of L holds
( x in X iff S1[x] ) from SUBSET_1:sch_3();
take X ; ::_thesis: for x being Element of L holds
( x in X iff x is completely-irreducible )
thus for x being Element of L holds
( x in X iff x is completely-irreducible ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is completely-irreducible ) ) & ( for x being Element of L holds
( x in b2 iff x is completely-irreducible ) ) holds
b1 = b2
proof
let S1, S2 be Subset of L; ::_thesis: ( ( for x being Element of L holds
( x in S1 iff x is completely-irreducible ) ) & ( for x being Element of L holds
( x in S2 iff x is completely-irreducible ) ) implies S1 = S2 )
assume that
A2: for x being Element of L holds
( x in S1 iff x is completely-irreducible ) and
A3: for x being Element of L holds
( x in S2 iff x is completely-irreducible ) ; ::_thesis: S1 = S2
now__::_thesis:_for_x1_being_set_holds_
(_(_x1_in_S1_implies_x1_in_S2_)_&_(_x1_in_S2_implies_x1_in_S1_)_)
let x1 be set ; ::_thesis: ( ( x1 in S1 implies x1 in S2 ) & ( x1 in S2 implies x1 in S1 ) )
thus ( x1 in S1 implies x1 in S2 ) ::_thesis: ( x1 in S2 implies x1 in S1 )
proof
assume A4: x1 in S1 ; ::_thesis: x1 in S2
then reconsider x2 = x1 as Element of L ;
x2 is completely-irreducible by A2, A4;
hence x1 in S2 by A3; ::_thesis: verum
end;
thus ( x1 in S2 implies x1 in S1 ) ::_thesis: verum
proof
assume A5: x1 in S2 ; ::_thesis: x1 in S1
then reconsider x2 = x1 as Element of L ;
x2 is completely-irreducible by A3, A5;
hence x1 in S1 by A2; ::_thesis: verum
end;
end;
hence S1 = S2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Irr WAYBEL16:def_4_:_
for L being non empty RelStr
for b2 being Subset of L holds
( b2 = Irr L iff for x being Element of L holds
( x in b2 iff x is completely-irreducible ) );
theorem Th20: :: WAYBEL16:20
for L being non empty Poset
for p being Element of L holds
( p is completely-irreducible iff ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) )
proof
let L be non empty Poset; ::_thesis: for p being Element of L holds
( p is completely-irreducible iff ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) )
let p be Element of L; ::_thesis: ( p is completely-irreducible iff ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) )
thus ( p is completely-irreducible implies ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) ) ::_thesis: ( ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) implies p is completely-irreducible )
proof
assume A1: p is completely-irreducible ; ::_thesis: ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) )
then ex_min_of (uparrow p) \ {p},L by Def3;
then A2: ex_inf_of (uparrow p) \ {p},L by WAYBEL_1:def_4;
take q = "/\" (((uparrow p) \ {p}),L); ::_thesis: ( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) )
now__::_thesis:_for_s_being_Element_of_L_st_s_in_(uparrow_p)_\_{p}_holds_
p_<=_s
let s be Element of L; ::_thesis: ( s in (uparrow p) \ {p} implies p <= s )
assume s in (uparrow p) \ {p} ; ::_thesis: p <= s
then s in uparrow p by XBOOLE_0:def_5;
hence p <= s by WAYBEL_0:18; ::_thesis: verum
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p} \/ (uparrow q) or x in uparrow p )
assume A5: x in {p} \/ (uparrow q) ; ::_thesis: x in uparrow p
now__::_thesis:_x_in_uparrow_p
percases ( x in {p} or x in uparrow q ) by A5, XBOOLE_0:def_3;
supposeA6: x in {p} ; ::_thesis: x in uparrow p
A7: p <= p ;
x = p by A6, TARSKI:def_1;
hence x in uparrow p by A7, WAYBEL_0:18; ::_thesis: verum
end;
supposeA8: x in uparrow q ; ::_thesis: x in uparrow p
then reconsider x1 = x as Element of L ;
q <= x1 by A8, WAYBEL_0:18;
then p <= x1 by A3, ORDERS_2:3;
hence x in uparrow p by WAYBEL_0:18; ::_thesis: verum
end;
end;
end;
hence x in uparrow p ; ::_thesis: verum
end;
"/\" (((uparrow p) \ {p}),L) <> p by A1, Th19;
hence p < q by A3, ORDERS_2:def_6; ::_thesis: ( ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) )
A9: q is_<=_than (uparrow p) \ {p} by A2, YELLOW_0:def_10;
thus for s being Element of L st p < s holds
q <= s ::_thesis: uparrow p = {p} \/ (uparrow q)
proof
let s be Element of L; ::_thesis: ( p < s implies q <= s )
assume A10: p < s ; ::_thesis: q <= 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 q <= s by A9, LATTICE3:def_8; ::_thesis: verum
end;
uparrow p c= {p} \/ (uparrow q)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow p or x in {p} \/ (uparrow q) )
assume A12: x in uparrow p ; ::_thesis: x in {p} \/ (uparrow q)
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 x in {p} \/ (uparrow q) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence uparrow p = {p} \/ (uparrow q) by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
thus ( ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) implies p is completely-irreducible ) ::_thesis: verum
proof
given q being Element of L such that A13: p < q and
A14: for s being Element of L st p < s holds
q <= s and
A15: uparrow p = {p} \/ (uparrow q) ; ::_thesis: p is completely-irreducible
A16: not q in {p} by A13, TARSKI:def_1;
ex q being Element of L st
( (uparrow p) \ {p} is_>=_than q & ( for b being Element of L st (uparrow p) \ {p} is_>=_than b holds
q >= b ) )
proof
take q ; ::_thesis: ( (uparrow p) \ {p} is_>=_than q & ( for b being Element of L st (uparrow p) \ {p} is_>=_than b holds
q >= b ) )
now__::_thesis:_for_a_being_Element_of_L_st_a_in_(uparrow_p)_\_{p}_holds_
q_<=_a
let a be Element of L; ::_thesis: ( a in (uparrow p) \ {p} implies q <= a )
assume A17: a in (uparrow p) \ {p} ; ::_thesis: q <= a
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; ::_thesis: verum
end;
hence (uparrow p) \ {p} is_>=_than q by LATTICE3:def_8; ::_thesis: for b being Element of L st (uparrow p) \ {p} is_>=_than b holds
q >= b
let b be Element of L; ::_thesis: ( (uparrow p) \ {p} is_>=_than b implies q >= b )
assume A19: (uparrow p) \ {p} is_>=_than b ; ::_thesis: q >= 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 q >= b by A19, LATTICE3:def_8; ::_thesis: verum
end;
then A21: ex_inf_of (uparrow p) \ {p},L by YELLOW_0:16;
A22: now__::_thesis:_for_b_being_Element_of_L_st_b_is_<=_than_(uparrow_p)_\_{p}_holds_
q_>=_b
let b be Element of L; ::_thesis: ( b is_<=_than (uparrow p) \ {p} implies q >= b )
assume A23: b is_<=_than (uparrow p) \ {p} ; ::_thesis: q >= b
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; ::_thesis: verum
end;
p <= q by A13, ORDERS_2:def_6;
then A25: q in uparrow p by WAYBEL_0:18;
now__::_thesis:_for_c_being_Element_of_L_st_c_in_(uparrow_p)_\_{p}_holds_
q_<=_c
let c be Element of L; ::_thesis: ( c in (uparrow p) \ {p} implies q <= c )
assume c in (uparrow p) \ {p} ; ::_thesis: q <= c
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; ::_thesis: verum
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 p is completely-irreducible by Def3; ::_thesis: verum
end;
end;
theorem Th21: :: WAYBEL16:21
for L being non empty upper-bounded Poset holds not Top L in Irr L
proof
let L be non empty upper-bounded Poset; ::_thesis: not Top L in Irr L
assume Top L in Irr L ; ::_thesis: contradiction
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; ::_thesis: verum
end;
theorem Th22: :: WAYBEL16:22
for L being Semilattice holds Irr L c= IRR L
proof
let L be Semilattice; ::_thesis: Irr L c= IRR L
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Irr L or x in IRR L )
assume A1: x in Irr L ; ::_thesis: x in IRR L
then reconsider x1 = x as Element of L ;
x1 is completely-irreducible by A1, Def4;
then consider q being Element of L such that
A2: x1 < q and
A3: for s being Element of L st x1 < s holds
q <= s and
uparrow x1 = {x1} \/ (uparrow q) by Th20;
now__::_thesis:_for_a,_b_being_Element_of_L_st_x1_=_a_"/\"_b_&_a_<>_x1_holds_
not_b_<>_x1
let a, b be Element of L; ::_thesis: ( x1 = a "/\" b & a <> x1 implies not b <> x1 )
assume that
A4: x1 = a "/\" b and
A5: a <> x1 and
A6: b <> x1 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then x1 is irreducible by WAYBEL_6:def_2;
hence x in IRR L by WAYBEL_6:def_4; ::_thesis: verum
end;
theorem Th23: :: WAYBEL16:23
for L being Semilattice
for x being Element of L st x is completely-irreducible holds
x is irreducible
proof
let L be Semilattice; ::_thesis: for x being Element of L st x is completely-irreducible holds
x is irreducible
let x be Element of L; ::_thesis: ( x is completely-irreducible implies x is irreducible )
assume x is completely-irreducible ; ::_thesis: x is irreducible
then A1: x in Irr L by Def4;
Irr L c= IRR L by Th22;
hence x is irreducible by A1, WAYBEL_6:def_4; ::_thesis: verum
end;
theorem Th24: :: WAYBEL16:24
for L being non empty Poset
for x being Element of L st x is completely-irreducible holds
for X being Subset of L st ex_inf_of X,L & x = inf X holds
x in X
proof
let L be non empty Poset; ::_thesis: for x being Element of L st x is completely-irreducible holds
for X being Subset of L st ex_inf_of X,L & x = inf X holds
x in X
let x be Element of L; ::_thesis: ( x is completely-irreducible implies for X being Subset of L st ex_inf_of X,L & x = inf X holds
x in X )
assume x is completely-irreducible ; ::_thesis: for X being Subset of L st ex_inf_of X,L & x = inf X holds
x in X
then consider q being Element of L such that
A1: x < q and
A2: for s being Element of L st x < s holds
q <= s and
uparrow x = {x} \/ (uparrow q) by Th20;
let X be Subset of L; ::_thesis: ( ex_inf_of X,L & x = inf X implies x in X )
assume that
A3: ex_inf_of X,L and
A4: x = inf X and
A5: not x in X ; ::_thesis: contradiction
A6: X c= uparrow q
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in uparrow q )
assume A7: y in X ; ::_thesis: y in uparrow q
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 y in uparrow q by WAYBEL_0:18; ::_thesis: verum
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; ::_thesis: verum
end;
theorem Th25: :: WAYBEL16:25
for L being non empty Poset
for X being Subset of L st X is order-generating holds
Irr L c= X
proof
let L be non empty Poset; ::_thesis: for X being Subset of L st X is order-generating holds
Irr L c= X
let X be Subset of L; ::_thesis: ( X is order-generating implies Irr L c= X )
assume A1: X is order-generating ; ::_thesis: Irr L c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Irr L or x in X )
assume A2: x in Irr L ; ::_thesis: x in X
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 x in X by XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th26: :: WAYBEL16:26
for L being complete LATTICE
for p being Element of L st ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) holds
p is completely-irreducible
proof
let L be complete LATTICE; ::_thesis: for p being Element of L st ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) holds
p is completely-irreducible
let p be Element of L; ::_thesis: ( ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) implies p is completely-irreducible )
given k being Element of L such that A1: p is_maximal_in the carrier of L \ (uparrow k) ; ::_thesis: p is completely-irreducible
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 p is completely-irreducible by Def3; ::_thesis: verum
end;
theorem Th27: :: WAYBEL16:27
for L being transitive antisymmetric with_suprema RelStr
for p, q, u being Element of L st p < q & ( for s being 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 ; ::_thesis: for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p holds
p "\/" u = q "\/" u
let p, q, u be Element of L; ::_thesis: ( p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p implies p "\/" u = q "\/" u )
assume that
A1: p < q and
A2: for s being Element of L st p < s holds
q <= s and
A3: not u <= p ; ::_thesis: p "\/" u = q "\/" u
A4: q "\/" u >= q by YELLOW_0:22;
A5: now__::_thesis:_for_v_being_Element_of_L_st_v_>=_p_&_v_>=_u_holds_
q_"\/"_u_<=_v
let v be Element of L; ::_thesis: ( v >= p & v >= u implies q "\/" u <= v )
assume that
A6: v >= p and
A7: v >= u ; ::_thesis: q "\/" u <= v
v > p by A3, A6, A7, ORDERS_2:def_6;
then v >= q by A2;
hence q "\/" u <= v by A7, YELLOW_0:22; ::_thesis: verum
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 p "\/" u = q "\/" u by A8, A5, YELLOW_0:22; ::_thesis: verum
end;
theorem Th28: :: WAYBEL16:28
for L being distributive LATTICE
for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p holds
not u "/\" q <= p
proof
let L be distributive LATTICE; ::_thesis: for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p holds
not u "/\" q <= p
let p, q, u be Element of L; ::_thesis: ( p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p implies not u "/\" q <= p )
assume that
A1: p < q and
A2: ( ( for s being Element of L st p < s holds
q <= s ) & not u <= p ) and
A3: u "/\" q <= p ; ::_thesis: contradiction
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; ::_thesis: verum
end;
theorem Th29: :: WAYBEL16:29
for L being distributive complete LATTICE st L opp is meet-continuous holds
for p being 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; ::_thesis: ( L opp is meet-continuous implies for p being Element of L st p is completely-irreducible holds
the carrier of L \ (downarrow p) is Open Filter of L )
assume A1: L opp is meet-continuous ; ::_thesis: for p being Element of L st p is completely-irreducible holds
the carrier of L \ (downarrow p) is Open Filter of L
let p be Element of L; ::_thesis: ( p is completely-irreducible implies the carrier of L \ (downarrow p) is Open Filter of L )
assume A2: p is completely-irreducible ; ::_thesis: the carrier of L \ (downarrow p) is Open Filter of L
then consider q being Element of L such that
A3: p < q and
A4: for s being Element of L st p < s holds
q <= s and
uparrow p = {p} \/ (uparrow q) by Th20;
defpred S1[ Element of L] means ( $1 <= q & not $1 <= p );
reconsider F = { t where t is Element of L : S1[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__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_F_&_y_in_F_holds_
ex_z_being_Element_of_the_carrier_of_L_st_
(_z_in_F_&_z_<=_x_&_z_<=_y_)
let x, y be Element of L; ::_thesis: ( x in F & y in F implies ex z being Element of the carrier of L st
( z in F & z <= x & z <= y ) )
assume that
A7: x in F and
A8: y in F ; ::_thesis: ex z being Element of the carrier of L st
( z in F & z <= x & z <= y )
A9: ex x1 being Element of L st
( x1 = x & x1 <= q & not x1 <= p ) by A7;
take z = x "/\" y; ::_thesis: ( z in F & z <= x & z <= y )
A10: z <= x by YELLOW_0:23;
A11: ex y1 being Element of L st
( y1 = y & y1 <= q & not y1 <= p ) by A8;
A12: not z <= p
proof
A13: now__::_thesis:_for_d_being_Element_of_L_st_d_>=_y_&_d_>=_p_holds_
q_<=_d
let d be Element of L; ::_thesis: ( d >= y & d >= p implies q <= d )
assume ( d >= y & d >= p ) ; ::_thesis: q <= d
then d > p by A11, ORDERS_2:def_6;
hence q <= d by A4; ::_thesis: verum
end;
assume A14: z <= p ; ::_thesis: contradiction
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; ::_thesis: verum
end;
z <= q by A9, A10, ORDERS_2:3;
hence z in F by A12; ::_thesis: ( z <= x & z <= y )
thus z <= x by YELLOW_0:23; ::_thesis: z <= y
thus z <= y by YELLOW_0:23; ::_thesis: verum
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 = 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__::_thesis:_for_x_being_Element_of_L_st_x_in_V_holds_
ex_y_being_Element_of_the_carrier_of_L_st_
(_y_in_V_&_y_<<_x_)
let x be Element of L; ::_thesis: ( x in V implies ex y being Element of the carrier of L st
( y in V & y << x ) )
assume A17: x in V ; ::_thesis: ex y being Element of the carrier of L st
( y in V & y << x )
take y = inf F; ::_thesis: ( y in V & y << x )
thus y in V ::_thesis: y << x
proof
now__::_thesis:_for_r_being_Element_of_L_st_r_in_{p}_"\/"_F_holds_
q_<=_r
let r be Element of L; ::_thesis: ( r in {p} "\/" F implies q <= r )
assume r in {p} "\/" F ; ::_thesis: q <= r
then r in { (p "\/" v) where v is Element of L : v in F } by YELLOW_4:15;
then consider v being Element of L such that
A18: r = p "\/" v and
A19: v in F ;
ex v1 being 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; ::_thesis: verum
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 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then not y in downarrow p by XBOOLE_0:def_5;
then A25: not y <= p by WAYBEL_0:17;
now__::_thesis:_for_D_being_non_empty_directed_Subset_of_L_st_y_<=_sup_D_holds_
ex_d_being_Element_of_L_st_
(_d_in_D_&_y_<=_d_)
let D be non empty directed Subset of L; ::_thesis: ( y <= sup D implies ex d being Element of L st
( d in D & y <= d ) )
assume A26: y <= sup D ; ::_thesis: ex d being Element of L st
( d in D & y <= d )
not D \ (downarrow p) is empty
proof
assume D \ (downarrow p) is empty ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then consider d being set such that
A27: d in D \ (downarrow p) by XBOOLE_0:def_1;
reconsider d = d as Element of L by A27;
take d = d; ::_thesis: ( d in D & y <= d )
thus d in D by A27, XBOOLE_0:def_5; ::_thesis: y <= d
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; ::_thesis: verum
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; ::_thesis: verum
end;
hence the carrier of L \ (downarrow p) is Open Filter of L by WAYBEL_6:def_1; ::_thesis: verum
end;
theorem :: WAYBEL16:30
for L being distributive complete LATTICE st L opp is meet-continuous holds
for p being Element of L st p is completely-irreducible holds
ex k being 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; ::_thesis: ( L opp is meet-continuous implies for p being Element of L st p is completely-irreducible holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) )
assume A1: L opp is meet-continuous ; ::_thesis: for p being Element of L st p is completely-irreducible holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
let p be Element of L; ::_thesis: ( p is completely-irreducible implies ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) )
assume A2: p is completely-irreducible ; ::_thesis: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
then reconsider V = the carrier of L \ (downarrow p) as Open Filter of L by A1, Th29;
now__::_thesis:_for_b_being_Element_of_L_st_b_in_(uparrow_p)_\_{p}_holds_
p_<=_b
let b be Element of L; ::_thesis: ( b in (uparrow p) \ {p} implies p <= b )
assume b in (uparrow p) \ {p} ; ::_thesis: p <= b
then b in uparrow p by XBOOLE_0:def_5;
hence p <= b by WAYBEL_0:18; ::_thesis: verum
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; ::_thesis: ( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p} "\/" V or x in (uparrow p) \ {p} )
assume x in {p} "\/" V ; ::_thesis: x in (uparrow p) \ {p}
then x in { (p "\/" v) where v is Element of L : v in V } by YELLOW_4:15;
then consider v being 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 x in (uparrow p) \ {p} by A9, A11, XBOOLE_0:def_5; ::_thesis: verum
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 ; ::_thesis: contradiction
then p "\/" k = p by YELLOW_0:24;
hence contradiction by A13, A4, ORDERS_2:7; ::_thesis: verum
end;
uparrow k = V
proof
thus uparrow k c= V :: according to XBOOLE_0:def_10 ::_thesis: V c= uparrow k
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow k or x in V )
assume A15: x in uparrow k ; ::_thesis: x in V
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 x in V by XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V or x in uparrow k )
assume A16: x in V ; ::_thesis: x in uparrow k
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 x in uparrow k by WAYBEL_0:18; ::_thesis: verum
end;
then k is compact by WAYBEL_8:2;
hence k in the carrier of (CompactSublatt L) by WAYBEL_8:def_1; ::_thesis: p is_maximal_in the carrier of L \ (uparrow k)
A17: for y being Element of L holds
( not y in the carrier of L \ (uparrow k) or not p < y )
proof
given y being Element of L such that A18: y in the carrier of L \ (uparrow k) and
A19: p < y ; ::_thesis: contradiction
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; ::_thesis: verum
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 p is_maximal_in the carrier of L \ (uparrow k) by A17, WAYBEL_4:55; ::_thesis: verum
end;
theorem Th31: :: WAYBEL16:31
for L being lower-bounded algebraic LATTICE
for x, y being Element of L st not y <= x holds
ex p being Element of L st
( p is completely-irreducible & x <= p & not y <= p )
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: for x, y being Element of L st not y <= x holds
ex p being Element of L st
( p is completely-irreducible & x <= p & not y <= p )
let x, y be Element of L; ::_thesis: ( not y <= x implies ex p being Element of L st
( p is completely-irreducible & x <= p & not y <= p ) )
assume A1: not y <= x ; ::_thesis: ex p being Element of L st
( p is completely-irreducible & x <= p & not y <= p )
for z being Element of L holds
( not waybelow z is empty & waybelow z is directed ) ;
then consider k1 being Element of L such that
A2: k1 << y and
A3: not k1 <= x by A1, WAYBEL_3:24;
consider k being 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 being Element of L such that
A8: x <= p and
A9: p is_maximal_in (uparrow k) ` by A7, WAYBEL_6:9;
take p ; ::_thesis: ( p is completely-irreducible & x <= p & not y <= p )
the carrier of L \ (uparrow k) = (uparrow k) ` by SUBSET_1:def_4;
hence p is completely-irreducible by A9, Th26; ::_thesis: ( x <= p & not y <= p )
thus x <= p by A8; ::_thesis: not y <= p
thus not y <= p ::_thesis: verum
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 ; ::_thesis: contradiction
then k <= p by A6, ORDERS_2:3;
hence contradiction by A10, WAYBEL_0:18; ::_thesis: verum
end;
end;
theorem Th32: :: WAYBEL16:32
for L being lower-bounded algebraic LATTICE holds
( Irr L is order-generating & ( for X being Subset of L st X is order-generating holds
Irr L c= X ) )
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: ( Irr L is order-generating & ( for X being Subset of L st X is order-generating holds
Irr L c= X ) )
now__::_thesis:_for_x,_y_being_Element_of_L_st_not_y_<=_x_holds_
ex_p_being_Element_of_L_st_
(_p_in_Irr_L_&_x_<=_p_&_not_y_<=_p_)
let x, y be Element of L; ::_thesis: ( not y <= x implies ex p being Element of L st
( p in Irr L & x <= p & not y <= p ) )
assume not y <= x ; ::_thesis: ex p being Element of L st
( p in Irr L & x <= p & not y <= p )
then consider p being Element of L such that
A1: p is completely-irreducible and
A2: x <= p and
A3: not y <= p by Th31;
take p = p; ::_thesis: ( p in Irr L & x <= p & not y <= p )
thus p in Irr L by A1, Def4; ::_thesis: ( x <= p & not y <= p )
thus x <= p by A2; ::_thesis: not y <= p
thus not y <= p by A3; ::_thesis: verum
end;
hence Irr L is order-generating by WAYBEL_6:17; ::_thesis: for X being Subset of L st X is order-generating holds
Irr L c= X
let X be Subset of L; ::_thesis: ( X is order-generating implies Irr L c= X )
assume X is order-generating ; ::_thesis: Irr L c= X
hence Irr L c= X by Th25; ::_thesis: verum
end;
theorem :: WAYBEL16:33
for L being lower-bounded algebraic LATTICE
for s being Element of L holds s = "/\" (((uparrow s) /\ (Irr L)),L)
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: for s being Element of L holds s = "/\" (((uparrow s) /\ (Irr L)),L)
let s be Element of L; ::_thesis: s = "/\" (((uparrow s) /\ (Irr L)),L)
Irr L is order-generating by Th32;
hence s = "/\" (((uparrow s) /\ (Irr L)),L) by WAYBEL_6:def_5; ::_thesis: verum
end;
theorem Th34: :: WAYBEL16:34
for L being non empty complete Poset
for X being Subset of L
for p being Element of L st p is completely-irreducible & p = inf X holds
p in X
proof
let L be non empty complete Poset; ::_thesis: for X being Subset of L
for p being Element of L st p is completely-irreducible & p = inf X holds
p in X
let X be Subset of L; ::_thesis: for p being Element of L st p is completely-irreducible & p = inf X holds
p in X
let p be Element of L; ::_thesis: ( p is completely-irreducible & p = inf X implies p in X )
assume that
A1: p is completely-irreducible and
A2: p = inf X ; ::_thesis: p in X
assume A3: not p in X ; ::_thesis: contradiction
consider q being Element of L such that
A4: p < q and
A5: for s being 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__::_thesis:_for_b_being_Element_of_L_st_b_in_X_holds_
q_<=_b
let b be Element of L; ::_thesis: ( b in X implies q <= b )
assume A7: b in X ; ::_thesis: q <= b
then p <= b by A6, LATTICE3:def_8;
then p < b by A3, A7, ORDERS_2:def_6;
hence q <= b by A5; ::_thesis: verum
end;
then A8: q is_<=_than X by LATTICE3:def_8;
A9: p <= q by A4, ORDERS_2:def_6;
now__::_thesis:_for_b_being_Element_of_L_st_b_is_<=_than_X_holds_
q_>=_b
let b be Element of L; ::_thesis: ( b is_<=_than X implies q >= b )
assume b is_<=_than X ; ::_thesis: q >= b
then p >= b by A2, YELLOW_0:33;
hence q >= b by A9, ORDERS_2:3; ::_thesis: verum
end;
hence contradiction by A2, A4, A8, YELLOW_0:33; ::_thesis: verum
end;
theorem Th35: :: WAYBEL16:35
for L being complete algebraic LATTICE
for p being Element of L st p is completely-irreducible holds
p = "/\" ( { x where x is Element of L : ( x in uparrow p & ex k being 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; ::_thesis: for p being Element of L st p is completely-irreducible holds
p = "/\" ( { x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } ,L)
let p be Element of L; ::_thesis: ( p is completely-irreducible implies p = "/\" ( { x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } ,L) )
set A = { x where x is Element of L : ( x in uparrow p & ex k being 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__::_thesis:_for_a_being_Element_of_L_st_a_in__{__x_where_x_is_Element_of_L_:_(_x_in_uparrow_p_&_ex_k_being_Element_of_L_st_
(_k_in_the_carrier_of_(CompactSublatt_L)_&_x_is_maximal_in_the_carrier_of_L_\_(uparrow_k)_)_)__}__holds_
p_<=_a
let a be Element of L; ::_thesis: ( a in { x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } implies p <= a )
assume a in { x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } ; ::_thesis: p <= a
then ex a1 being Element of L st
( a1 = a & a1 in uparrow p & ex k being 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; ::_thesis: verum
end;
then A2: p is_<=_than { x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } by LATTICE3:def_8;
assume p is completely-irreducible ; ::_thesis: p = "/\" ( { x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } ,L)
then consider q being Element of L such that
A3: p < q and
A4: for s being 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 ; ::_thesis: contradiction
then p = sup (compactbelow q) by WAYBEL_8:def_3
.= q by WAYBEL_8:def_3 ;
hence contradiction by A3; ::_thesis: verum
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, XBOOLE_0:def_10;
then consider k1 being set such that
A6: k1 in compactbelow q and
A7: not k1 in compactbelow p by TARSKI:def_3;
k1 in { y where y is Element of L : ( q >= y & y is compact ) } by A6, WAYBEL_8:def_2;
then consider k being Element of L such that
A8: k = k1 and
A9: q >= k and
A10: k is compact ;
A11: for y being Element of L holds
( not y in the carrier of L \ (uparrow k) or not p < y )
proof
given y being Element of L such that A12: y in the carrier of L \ (uparrow k) and
A13: p < y ; ::_thesis: contradiction
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; ::_thesis: verum
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 { x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } by A1, A14;
then for u being Element of L st u is_<=_than { x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } holds
p >= u by LATTICE3:def_8;
hence p = "/\" ( { x where x is Element of L : ( x in uparrow p & ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } ,L) by A2, YELLOW_0:33; ::_thesis: verum
end;
theorem :: WAYBEL16:36
for L being complete algebraic LATTICE
for p being Element of L holds
( ex k being 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; ::_thesis: for p being Element of L holds
( ex k being 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 )
let p be Element of L; ::_thesis: ( ex k being 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 )
thus ( ex k being 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; ::_thesis: ( p is completely-irreducible implies ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) )
thus ( p is completely-irreducible implies ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) ) ::_thesis: verum
proof
defpred S1[ Element of L] means ( $1 in uparrow p & ex k being 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 : S1[x] } as Subset of L from DOMAIN_1:sch_7();
assume A1: p is completely-irreducible ; ::_thesis: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
then p = inf A by Th35;
then p in A by A1, Th34;
then consider x being Element of L such that
A2: x = p and
x in uparrow p and
A3: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ;
consider k being 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 ; ::_thesis: ( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) )
thus k in the carrier of (CompactSublatt L) by A4; ::_thesis: p is_maximal_in the carrier of L \ (uparrow k)
thus p is_maximal_in the carrier of L \ (uparrow k) by A2, A5; ::_thesis: verum
end;
end;