:: WAYBEL_8 semantic presentation
begin
definition
let L be non empty reflexive RelStr ;
func CompactSublatt L -> strict full SubRelStr of L means :Def1: :: WAYBEL_8:def 1
for x being Element of L holds
( x in the carrier of it iff x is compact );
existence
ex b1 being strict full SubRelStr of L st
for x being Element of L holds
( x in the carrier of b1 iff x is compact )
proof
defpred S1[ set ] means ex y being Element of L st
( y = $1 & y is compact );
consider X being Subset of L such that
A1: for x being set holds
( x in X iff ( x in the carrier of L & S1[x] ) ) from SUBSET_1:sch_1();
reconsider S = RelStr(# X,( the InternalRel of L |_2 X) #) as strict full SubRelStr of L by YELLOW_0:56;
take S ; ::_thesis: for x being Element of L holds
( x in the carrier of S iff x is compact )
let x be Element of L; ::_thesis: ( x in the carrier of S iff x is compact )
thus ( x in the carrier of S implies x is compact ) ::_thesis: ( x is compact implies x in the carrier of S )
proof
assume x in the carrier of S ; ::_thesis: x is compact
then ex y being Element of L st
( y = x & y is compact ) by A1;
hence x is compact ; ::_thesis: verum
end;
thus ( x is compact implies x in the carrier of S ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict full SubRelStr of L st ( for x being Element of L holds
( x in the carrier of b1 iff x is compact ) ) & ( for x being Element of L holds
( x in the carrier of b2 iff x is compact ) ) holds
b1 = b2
proof
let K1, K2 be strict full SubRelStr of L; ::_thesis: ( ( for x being Element of L holds
( x in the carrier of K1 iff x is compact ) ) & ( for x being Element of L holds
( x in the carrier of K2 iff x is compact ) ) implies K1 = K2 )
assume that
A2: for x being Element of L holds
( x in the carrier of K1 iff x is compact ) and
A3: for x being Element of L holds
( x in the carrier of K2 iff x is compact ) ; ::_thesis: K1 = K2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_the_carrier_of_K1_implies_x_in_the_carrier_of_K2_)_&_(_x_in_the_carrier_of_K2_implies_x_in_the_carrier_of_K1_)_)
let x be set ; ::_thesis: ( ( x in the carrier of K1 implies x in the carrier of K2 ) & ( x in the carrier of K2 implies x in the carrier of K1 ) )
thus ( x in the carrier of K1 implies x in the carrier of K2 ) ::_thesis: ( x in the carrier of K2 implies x in the carrier of K1 )
proof
assume A4: x in the carrier of K1 ; ::_thesis: x in the carrier of K2
the carrier of K1 c= the carrier of L by YELLOW_0:def_13;
then reconsider x9 = x as Element of L by A4;
x9 is compact by A2, A4;
hence x in the carrier of K2 by A3; ::_thesis: verum
end;
thus ( x in the carrier of K2 implies x in the carrier of K1 ) ::_thesis: verum
proof
assume A5: x in the carrier of K2 ; ::_thesis: x in the carrier of K1
the carrier of K2 c= the carrier of L by YELLOW_0:def_13;
then reconsider x9 = x as Element of L by A5;
x9 is compact by A3, A5;
hence x in the carrier of K1 by A2; ::_thesis: verum
end;
end;
then the carrier of K1 = the carrier of K2 by TARSKI:1;
hence K1 = K2 by YELLOW_0:57; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines CompactSublatt WAYBEL_8:def_1_:_
for L being non empty reflexive RelStr
for b2 being strict full SubRelStr of L holds
( b2 = CompactSublatt L iff for x being Element of L holds
( x in the carrier of b2 iff x is compact ) );
registration
let L be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster CompactSublatt L -> non empty strict full ;
coherence
not CompactSublatt L is empty
proof
Bottom L is compact by WAYBEL_3:15;
hence not CompactSublatt L is empty by Def1; ::_thesis: verum
end;
end;
theorem :: WAYBEL_8:1
for L being complete LATTICE
for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds
x << y
proof
let L be complete LATTICE; ::_thesis: for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds
x << y
let x, y, k be Element of L; ::_thesis: ( x <= k & k <= y & k in the carrier of (CompactSublatt L) implies x << y )
assume that
A1: ( x <= k & k <= y ) and
A2: k in the carrier of (CompactSublatt L) ; ::_thesis: x << y
k is compact by A2, Def1;
then k << k by WAYBEL_3:def_2;
hence x << y by A1, WAYBEL_3:2; ::_thesis: verum
end;
theorem :: WAYBEL_8:2
for L being complete LATTICE
for x being Element of L holds
( uparrow x is Open Filter of L iff x is compact )
proof
let L be complete LATTICE; ::_thesis: for x being Element of L holds
( uparrow x is Open Filter of L iff x is compact )
let x be Element of L; ::_thesis: ( uparrow x is Open Filter of L iff x is compact )
thus ( uparrow x is Open Filter of L implies x is compact ) ::_thesis: ( x is compact implies uparrow x is Open Filter of L )
proof
x <= x ;
then A1: x in uparrow x by WAYBEL_0:18;
assume uparrow x is Open Filter of L ; ::_thesis: x is compact
then consider y being Element of L such that
A2: y in uparrow x and
A3: y << x by A1, WAYBEL_6:def_1;
x <= y by A2, WAYBEL_0:18;
then x << x by A3, WAYBEL_3:2;
hence x is compact by WAYBEL_3:def_2; ::_thesis: verum
end;
assume A4: x is compact ; ::_thesis: uparrow x is Open Filter of L
now__::_thesis:_for_u_being_Element_of_L_st_u_in_uparrow_x_holds_
ex_x2_being_Element_of_L_st_
(_x2_in_uparrow_x_&_x2_<<_u_)
let u be Element of L; ::_thesis: ( u in uparrow x implies ex x2 being Element of L st
( x2 in uparrow x & x2 << u ) )
assume u in uparrow x ; ::_thesis: ex x2 being Element of L st
( x2 in uparrow x & x2 << u )
then A5: x <= u by WAYBEL_0:18;
take x2 = x; ::_thesis: ( x2 in uparrow x & x2 << u )
x <= x2 ;
hence x2 in uparrow x by WAYBEL_0:18; ::_thesis: x2 << u
x << x by A4, WAYBEL_3:def_2;
hence x2 << u by A5, WAYBEL_3:2; ::_thesis: verum
end;
hence uparrow x is Open Filter of L by WAYBEL_6:def_1; ::_thesis: verum
end;
theorem :: WAYBEL_8:3
for L being non empty with_suprema lower-bounded Poset holds
( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) )
proof
let L be non empty with_suprema lower-bounded Poset; ::_thesis: ( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) )
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_sup_of_{x,y},L_holds_
sup_{x,y}_in_the_carrier_of_(CompactSublatt_L)
let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_sup_of {x,y},L implies sup {x,y} in the carrier of (CompactSublatt L) )
assume that
A1: x in the carrier of (CompactSublatt L) and
A2: y in the carrier of (CompactSublatt L) and
A3: ex_sup_of {x,y},L ; ::_thesis: sup {x,y} in the carrier of (CompactSublatt L)
y is compact by A2, Def1;
then A4: y << y by WAYBEL_3:def_2;
x is compact by A1, Def1;
then A5: x << x by WAYBEL_3:def_2;
y <= x "\/" y by A3, YELLOW_0:18;
then A6: y << x "\/" y by A4, WAYBEL_3:2;
x <= x "\/" y by A3, YELLOW_0:18;
then x << x "\/" y by A5, WAYBEL_3:2;
then x "\/" y << x "\/" y by A6, WAYBEL_3:3;
then x "\/" y is compact by WAYBEL_3:def_2;
then sup {x,y} is compact by YELLOW_0:41;
hence sup {x,y} in the carrier of (CompactSublatt L) by Def1; ::_thesis: verum
end;
hence CompactSublatt L is join-inheriting by YELLOW_0:def_17; ::_thesis: Bottom L in the carrier of (CompactSublatt L)
Bottom L is compact by WAYBEL_3:15;
hence Bottom L in the carrier of (CompactSublatt L) by Def1; ::_thesis: verum
end;
definition
let L be non empty reflexive RelStr ;
let x be Element of L;
func compactbelow x -> Subset of L equals :: WAYBEL_8:def 2
{ y where y is Element of L : ( x >= y & y is compact ) } ;
coherence
{ y where y is Element of L : ( x >= y & y is compact ) } is Subset of L
proof
set Z = { y where y is Element of L : ( x >= y & y is compact ) } ;
defpred S1[ Element of L] means ( x >= $1 & $1 is compact );
consider X being Subset of L such that
A1: for y being Element of L holds
( y in X iff S1[y] ) from SUBSET_1:sch_3();
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_X_implies_z_in__{__y_where_y_is_Element_of_L_:_(_x_>=_y_&_y_is_compact_)__}__)_&_(_z_in__{__y_where_y_is_Element_of_L_:_(_x_>=_y_&_y_is_compact_)__}__implies_z_in_X_)_)
let z be set ; ::_thesis: ( ( z in X implies z in { y where y is Element of L : ( x >= y & y is compact ) } ) & ( z in { y where y is Element of L : ( x >= y & y is compact ) } implies z in X ) )
thus ( z in X implies z in { y where y is Element of L : ( x >= y & y is compact ) } ) ::_thesis: ( z in { y where y is Element of L : ( x >= y & y is compact ) } implies z in X )
proof
assume A2: z in X ; ::_thesis: z in { y where y is Element of L : ( x >= y & y is compact ) }
then reconsider z1 = z as Element of L ;
( x >= z1 & z1 is compact ) by A1, A2;
hence z in { y where y is Element of L : ( x >= y & y is compact ) } ; ::_thesis: verum
end;
thus ( z in { y where y is Element of L : ( x >= y & y is compact ) } implies z in X ) ::_thesis: verum
proof
assume z in { y where y is Element of L : ( x >= y & y is compact ) } ; ::_thesis: z in X
then ex v being Element of L st
( v = z & x >= v & v is compact ) ;
hence z in X by A1; ::_thesis: verum
end;
end;
hence { y where y is Element of L : ( x >= y & y is compact ) } is Subset of L by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem defines compactbelow WAYBEL_8:def_2_:_
for L being non empty reflexive RelStr
for x being Element of L holds compactbelow x = { y where y is Element of L : ( x >= y & y is compact ) } ;
theorem Th4: :: WAYBEL_8:4
for L being non empty reflexive RelStr
for x, y being Element of L holds
( y in compactbelow x iff ( x >= y & y is compact ) )
proof
let L be non empty reflexive RelStr ; ::_thesis: for x, y being Element of L holds
( y in compactbelow x iff ( x >= y & y is compact ) )
let x, y be Element of L; ::_thesis: ( y in compactbelow x iff ( x >= y & y is compact ) )
thus ( y in compactbelow x implies ( x >= y & y is compact ) ) ::_thesis: ( x >= y & y is compact implies y in compactbelow x )
proof
assume y in compactbelow x ; ::_thesis: ( x >= y & y is compact )
then ex z being Element of L st
( z = y & x >= z & z is compact ) ;
hence ( x >= y & y is compact ) ; ::_thesis: verum
end;
assume ( x >= y & y is compact ) ; ::_thesis: y in compactbelow x
hence y in compactbelow x ; ::_thesis: verum
end;
theorem Th5: :: WAYBEL_8:5
for L being non empty reflexive RelStr
for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)
proof
let L be non empty reflexive RelStr ; ::_thesis: for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)
let x be Element of L; ::_thesis: compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)
now__::_thesis:_for_y_being_set_st_y_in_(downarrow_x)_/\_the_carrier_of_(CompactSublatt_L)_holds_
y_in_compactbelow_x
let y be set ; ::_thesis: ( y in (downarrow x) /\ the carrier of (CompactSublatt L) implies y in compactbelow x )
assume A1: y in (downarrow x) /\ the carrier of (CompactSublatt L) ; ::_thesis: y in compactbelow x
then reconsider y9 = y as Element of L ;
y in downarrow x by A1, XBOOLE_0:def_4;
then A2: y9 <= x by WAYBEL_0:17;
y in the carrier of (CompactSublatt L) by A1, XBOOLE_0:def_4;
then y9 is compact by Def1;
hence y in compactbelow x by A2; ::_thesis: verum
end;
then A3: (downarrow x) /\ the carrier of (CompactSublatt L) c= compactbelow x by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_compactbelow_x_holds_
y_in_(downarrow_x)_/\_the_carrier_of_(CompactSublatt_L)
let y be set ; ::_thesis: ( y in compactbelow x implies y in (downarrow x) /\ the carrier of (CompactSublatt L) )
assume y in compactbelow x ; ::_thesis: y in (downarrow x) /\ the carrier of (CompactSublatt L)
then consider y9 being Element of L such that
A4: y9 = y and
A5: ( y9 <= x & y9 is compact ) ;
( y9 in downarrow x & y9 in the carrier of (CompactSublatt L) ) by A5, Def1, WAYBEL_0:17;
hence y in (downarrow x) /\ the carrier of (CompactSublatt L) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
then compactbelow x c= (downarrow x) /\ the carrier of (CompactSublatt L) by TARSKI:def_3;
hence compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th6: :: WAYBEL_8:6
for L being non empty reflexive transitive RelStr
for x being Element of L holds compactbelow x c= waybelow x
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for x being Element of L holds compactbelow x c= waybelow x
let x be Element of L; ::_thesis: compactbelow x c= waybelow x
now__::_thesis:_for_z_being_set_st_z_in_compactbelow_x_holds_
z_in_waybelow_x
let z be set ; ::_thesis: ( z in compactbelow x implies z in waybelow x )
assume z in compactbelow x ; ::_thesis: z in waybelow x
then consider z9 being Element of L such that
A1: z9 = z and
A2: x >= z9 and
A3: z9 is compact ;
z9 << z9 by A3, WAYBEL_3:def_2;
then z9 << x by A2, WAYBEL_3:2;
hence z in waybelow x by A1, WAYBEL_3:7; ::_thesis: verum
end;
hence compactbelow x c= waybelow x by TARSKI:def_3; ::_thesis: verum
end;
registration
let L be non empty reflexive antisymmetric lower-bounded RelStr ;
let x be Element of L;
cluster compactbelow x -> non empty ;
coherence
not compactbelow x is empty
proof
( x >= Bottom L & Bottom L is compact ) by WAYBEL_3:15, YELLOW_0:44;
then Bottom L in { y where y is Element of L : ( x >= y & y is compact ) } ;
hence not compactbelow x is empty ; ::_thesis: verum
end;
end;
begin
definition
let L be non empty reflexive RelStr ;
attrL is satisfying_axiom_K means :Def3: :: WAYBEL_8:def 3
for x being Element of L holds x = sup (compactbelow x);
end;
:: deftheorem Def3 defines satisfying_axiom_K WAYBEL_8:def_3_:_
for L being non empty reflexive RelStr holds
( L is satisfying_axiom_K iff for x being Element of L holds x = sup (compactbelow x) );
definition
let L be non empty reflexive RelStr ;
attrL is algebraic means :Def4: :: WAYBEL_8:def 4
( ( for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K );
end;
:: deftheorem Def4 defines algebraic WAYBEL_8:def_4_:_
for L being non empty reflexive RelStr holds
( L is algebraic iff ( ( for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K ) );
theorem Th7: :: WAYBEL_8:7
for L being LATTICE holds
( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) )
proof
let L be LATTICE; ::_thesis: ( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) )
thus ( L is algebraic implies ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) ) ::_thesis: ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) implies L is algebraic )
proof
assume A1: L is algebraic ; ::_thesis: ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) )
then A2: ( L is up-complete & L is satisfying_axiom_K ) by Def4;
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(waybelow_x)
let x be Element of L; ::_thesis: x = sup (waybelow x)
A3: ( not compactbelow x is empty & compactbelow x is directed ) by A1, Def4;
then A4: ex s being set st s in compactbelow x by XBOOLE_0:def_1;
compactbelow x c= waybelow x by Th6;
then A5: ex_sup_of waybelow x,L by A2, A4, WAYBEL_0:75;
ex_sup_of compactbelow x,L by A2, A3, WAYBEL_0:75;
then sup (compactbelow x) <= sup (waybelow x) by A5, Th6, YELLOW_0:34;
then A6: x <= sup (waybelow x) by A2, Def3;
waybelow x is_<=_than x by WAYBEL_3:9;
then sup (waybelow x) <= x by A5, YELLOW_0:def_9;
hence x = sup (waybelow x) by A6, ORDERS_2:2; ::_thesis: verum
end;
then A7: L is satisfying_axiom_of_approximation by WAYBEL_3:def_5;
for x being Element of L holds
( not waybelow x is empty & waybelow x is directed )
proof
let x be Element of L; ::_thesis: ( not waybelow x is empty & waybelow x is directed )
compactbelow x c= waybelow x by Th6;
hence ( not waybelow x is empty & waybelow x is directed ) by A1, Def4; ::_thesis: verum
end;
hence L is continuous by A2, A7, WAYBEL_3:def_6; ::_thesis: for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y )
let x, y be Element of L; ::_thesis: ( x << y implies ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) )
reconsider D = compactbelow y as non empty directed Subset of L by A1, Def4;
assume A8: x << y ; ::_thesis: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y )
y = sup D by A2, Def3;
then consider d being Element of L such that
A9: d in D and
A10: x <= d by A8, WAYBEL_3:def_1;
take d ; ::_thesis: ( d in the carrier of (CompactSublatt L) & x <= d & d <= y )
d is compact by A9, Th4;
hence d in the carrier of (CompactSublatt L) by Def1; ::_thesis: ( x <= d & d <= y )
thus ( x <= d & d <= y ) by A9, A10, Th4; ::_thesis: verum
end;
assume that
A11: L is continuous and
A12: for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ; ::_thesis: L is algebraic
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(compactbelow_x)
let x be Element of L; ::_thesis: x = sup (compactbelow x)
A13: now__::_thesis:_for_z_being_Element_of_L_holds_
(_(_z_is_>=_than_waybelow_x_implies_z_is_>=_than_compactbelow_x_)_&_(_z_is_>=_than_compactbelow_x_implies_z_is_>=_than_waybelow_x_)_)
let z be Element of L; ::_thesis: ( ( z is_>=_than waybelow x implies z is_>=_than compactbelow x ) & ( z is_>=_than compactbelow x implies z is_>=_than waybelow x ) )
thus ( z is_>=_than waybelow x implies z is_>=_than compactbelow x ) ::_thesis: ( z is_>=_than compactbelow x implies z is_>=_than waybelow x )
proof
assume A14: z is_>=_than waybelow x ; ::_thesis: z is_>=_than compactbelow x
now__::_thesis:_for_d_being_Element_of_L_st_d_in_compactbelow_x_holds_
d_<=_z
let d be Element of L; ::_thesis: ( d in compactbelow x implies d <= z )
assume A15: d in compactbelow x ; ::_thesis: d <= z
then d is compact by Th4;
then A16: d << d by WAYBEL_3:def_2;
d <= x by A15, Th4;
then d << x by A16, WAYBEL_3:2;
then d in waybelow x by WAYBEL_3:7;
hence d <= z by A14, LATTICE3:def_9; ::_thesis: verum
end;
hence z is_>=_than compactbelow x by LATTICE3:def_9; ::_thesis: verum
end;
thus ( z is_>=_than compactbelow x implies z is_>=_than waybelow x ) ::_thesis: verum
proof
assume A17: z is_>=_than compactbelow x ; ::_thesis: z is_>=_than waybelow x
now__::_thesis:_for_d_being_Element_of_L_st_d_in_waybelow_x_holds_
d_<=_z
let d be Element of L; ::_thesis: ( d in waybelow x implies d <= z )
assume d in waybelow x ; ::_thesis: d <= z
then d << x by WAYBEL_3:7;
then consider k being Element of L such that
A18: k in the carrier of (CompactSublatt L) and
A19: d <= k and
A20: k <= x by A12;
k is compact by A18, Def1;
then k in compactbelow x by A20;
then k <= z by A17, LATTICE3:def_9;
hence d <= z by A19, ORDERS_2:3; ::_thesis: verum
end;
hence z is_>=_than waybelow x by LATTICE3:def_9; ::_thesis: verum
end;
end;
( x = sup (waybelow x) & ex_sup_of waybelow x,L ) by A11, WAYBEL_0:75, WAYBEL_3:def_5;
hence x = sup (compactbelow x) by A13, YELLOW_0:47; ::_thesis: verum
end;
then A21: L is satisfying_axiom_K by Def3;
for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed )
proof
let x be Element of L; ::_thesis: ( not compactbelow x is empty & compactbelow x is directed )
now__::_thesis:_for_Y_being_finite_Subset_of_(compactbelow_x)_ex_c_being_Element_of_L_st_
(_c_in_compactbelow_x_&_c_is_>=_than_Y_)
let Y be finite Subset of (compactbelow x); ::_thesis: ex c being Element of L st
( c in compactbelow x & c is_>=_than Y )
compactbelow x c= waybelow x by Th6;
then Y is finite Subset of (waybelow x) by XBOOLE_1:1;
then consider b being Element of L such that
A22: b in waybelow x and
A23: b is_>=_than Y by A11, WAYBEL_0:1;
b << x by A22, WAYBEL_3:7;
then consider c being Element of L such that
A24: c in the carrier of (CompactSublatt L) and
A25: b <= c and
A26: c <= x by A12;
take c = c; ::_thesis: ( c in compactbelow x & c is_>=_than Y )
c is compact by A24, Def1;
hence c in compactbelow x by A26; ::_thesis: c is_>=_than Y
thus c is_>=_than Y by A23, A25, YELLOW_0:4; ::_thesis: verum
end;
hence ( not compactbelow x is empty & compactbelow x is directed ) by WAYBEL_0:1; ::_thesis: verum
end;
hence L is algebraic by A11, A21, Def4; ::_thesis: verum
end;
registration
cluster reflexive transitive antisymmetric with_suprema with_infima algebraic -> continuous for RelStr ;
coherence
for b1 being LATTICE st b1 is algebraic holds
b1 is continuous by Th7;
end;
registration
cluster non empty reflexive algebraic -> non empty reflexive up-complete satisfying_axiom_K for RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is algebraic holds
( b1 is up-complete & b1 is satisfying_axiom_K ) by Def4;
end;
registration
let L be non empty with_suprema Poset;
cluster CompactSublatt L -> strict full join-inheriting ;
coherence
CompactSublatt L is join-inheriting
proof
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_sup_of_{x,y},L_holds_
sup_{x,y}_in_the_carrier_of_(CompactSublatt_L)
let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_sup_of {x,y},L implies sup {x,y} in the carrier of (CompactSublatt L) )
assume that
A1: x in the carrier of (CompactSublatt L) and
A2: y in the carrier of (CompactSublatt L) and
A3: ex_sup_of {x,y},L ; ::_thesis: sup {x,y} in the carrier of (CompactSublatt L)
y is compact by A2, Def1;
then A4: y << y by WAYBEL_3:def_2;
x is compact by A1, Def1;
then A5: x << x by WAYBEL_3:def_2;
y <= x "\/" y by A3, YELLOW_0:18;
then A6: y << x "\/" y by A4, WAYBEL_3:2;
x <= x "\/" y by A3, YELLOW_0:18;
then x << x "\/" y by A5, WAYBEL_3:2;
then x "\/" y << x "\/" y by A6, WAYBEL_3:3;
then x "\/" y is compact by WAYBEL_3:def_2;
then sup {x,y} is compact by YELLOW_0:41;
hence sup {x,y} in the carrier of (CompactSublatt L) by Def1; ::_thesis: verum
end;
hence CompactSublatt L is join-inheriting by YELLOW_0:def_17; ::_thesis: verum
end;
end;
definition
let L be non empty reflexive RelStr ;
attrL is arithmetic means :Def5: :: WAYBEL_8:def 5
( L is algebraic & CompactSublatt L is meet-inheriting );
end;
:: deftheorem Def5 defines arithmetic WAYBEL_8:def_5_:_
for L being non empty reflexive RelStr holds
( L is arithmetic iff ( L is algebraic & CompactSublatt L is meet-inheriting ) );
begin
registration
cluster reflexive transitive antisymmetric with_suprema with_infima arithmetic -> algebraic for RelStr ;
coherence
for b1 being LATTICE st b1 is arithmetic holds
b1 is algebraic by Def5;
end;
registration
cluster trivial reflexive transitive antisymmetric with_suprema with_infima -> arithmetic for RelStr ;
coherence
for b1 being LATTICE st b1 is trivial holds
b1 is arithmetic
proof
let L be LATTICE; ::_thesis: ( L is trivial implies L is arithmetic )
assume A1: L is trivial ; ::_thesis: L is arithmetic
reconsider L9 = L as 1 -element LATTICE by A1;
A2: for x, y being Element of L9 st x << y holds
ex k being Element of L9 st
( k in the carrier of (CompactSublatt L9) & x <= k & k <= y )
proof
let x, y be Element of L9; ::_thesis: ( x << y implies ex k being Element of L9 st
( k in the carrier of (CompactSublatt L9) & x <= k & k <= y ) )
assume A3: x << y ; ::_thesis: ex k being Element of L9 st
( k in the carrier of (CompactSublatt L9) & x <= k & k <= y )
take k = x; ::_thesis: ( k in the carrier of (CompactSublatt L9) & x <= k & k <= y )
x = y by STRUCT_0:def_10;
then k is compact by A3, WAYBEL_3:def_2;
hence k in the carrier of (CompactSublatt L9) by Def1; ::_thesis: ( x <= k & k <= y )
thus ( x <= k & k <= y ) by STRUCT_0:def_10; ::_thesis: verum
end;
A4: L9 is algebraic by Th7, A2;
for z, v being Element of L9 st z in the carrier of (CompactSublatt L9) & v in the carrier of (CompactSublatt L9) & ex_inf_of {z,v},L9 holds
inf {z,v} in the carrier of (CompactSublatt L9) by STRUCT_0:def_10;
then CompactSublatt L9 is meet-inheriting by YELLOW_0:def_16;
hence L is arithmetic by A4, Def5; ::_thesis: verum
end;
end;
registration
cluster non empty 1 -element strict reflexive transitive antisymmetric with_suprema with_infima for RelStr ;
existence
ex b1 being LATTICE st
( b1 is 1 -element & b1 is strict )
proof
set B = the 1 -element strict reflexive RelStr ;
take the 1 -element strict reflexive RelStr ; ::_thesis: ( the 1 -element strict reflexive RelStr is 1 -element & the 1 -element strict reflexive RelStr is strict )
thus ( the 1 -element strict reflexive RelStr is 1 -element & the 1 -element strict reflexive RelStr is strict ) ; ::_thesis: verum
end;
end;
theorem Th8: :: WAYBEL_8:8
for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
for x1, y1 being Element of L1
for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2
proof
let L1, L2 be non empty reflexive antisymmetric RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete implies for x1, y1 being Element of L1
for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2 )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is up-complete ; ::_thesis: for x1, y1 being Element of L1
for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2
let x1, y1 be Element of L1; ::_thesis: for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2
let x2, y2 be Element of L2; ::_thesis: ( x1 = x2 & y1 = y2 & x1 << y1 implies x2 << y2 )
assume that
A3: x1 = x2 and
A4: y1 = y2 and
A5: x1 << y1 ; ::_thesis: x2 << y2
now__::_thesis:_for_D2_being_non_empty_directed_Subset_of_L2_st_y2_<=_sup_D2_holds_
ex_d2_being_Element_of_L2_st_
(_d2_in_D2_&_x2_<=_d2_)
let D2 be non empty directed Subset of L2; ::_thesis: ( y2 <= sup D2 implies ex d2 being Element of L2 st
( d2 in D2 & x2 <= d2 ) )
reconsider D1 = D2 as Subset of L1 by A1;
reconsider D1 = D1 as non empty directed Subset of L1 by A1, WAYBEL_0:3;
ex_sup_of D1,L1 by A2, WAYBEL_0:75;
then A6: sup D1 = sup D2 by A1, YELLOW_0:26;
assume y2 <= sup D2 ; ::_thesis: ex d2 being Element of L2 st
( d2 in D2 & x2 <= d2 )
then y1 <= sup D1 by A1, A4, A6, YELLOW_0:1;
then consider d1 being Element of L1 such that
A7: d1 in D1 and
A8: x1 <= d1 by A5, WAYBEL_3:def_1;
reconsider d2 = d1 as Element of L2 by A1;
take d2 = d2; ::_thesis: ( d2 in D2 & x2 <= d2 )
thus d2 in D2 by A7; ::_thesis: x2 <= d2
thus x2 <= d2 by A1, A3, A8, YELLOW_0:1; ::_thesis: verum
end;
hence x2 << y2 by WAYBEL_3:def_1; ::_thesis: verum
end;
theorem Th9: :: WAYBEL_8:9
for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
for x being Element of L1
for y being Element of L2 st x = y & x is compact holds
y is compact
proof
let L1, L2 be non empty reflexive antisymmetric RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete implies for x being Element of L1
for y being Element of L2 st x = y & x is compact holds
y is compact )
assume A1: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete ) ; ::_thesis: for x being Element of L1
for y being Element of L2 st x = y & x is compact holds
y is compact
let x be Element of L1; ::_thesis: for y being Element of L2 st x = y & x is compact holds
y is compact
let y be Element of L2; ::_thesis: ( x = y & x is compact implies y is compact )
assume that
A2: x = y and
A3: x is compact ; ::_thesis: y is compact
x << x by A3, WAYBEL_3:def_2;
then y << y by A1, A2, Th8;
hence y is compact by WAYBEL_3:def_2; ::_thesis: verum
end;
theorem Th10: :: WAYBEL_8:10
for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for x being Element of L1
for y being Element of L2 st x = y holds
compactbelow x = compactbelow y
proof
let L1, L2 be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for x being Element of L1
for y being Element of L2 st x = y holds
compactbelow x = compactbelow y )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for x being Element of L1
for y being Element of L2 st x = y holds
compactbelow x = compactbelow y
let x be Element of L1; ::_thesis: for y being Element of L2 st x = y holds
compactbelow x = compactbelow y
let y be Element of L2; ::_thesis: ( x = y implies compactbelow x = compactbelow y )
assume A2: x = y ; ::_thesis: compactbelow x = compactbelow y
now__::_thesis:_for_z_being_set_st_z_in_compactbelow_y_holds_
z_in_compactbelow_x
let z be set ; ::_thesis: ( z in compactbelow y implies z in compactbelow x )
assume A3: z in compactbelow y ; ::_thesis: z in compactbelow x
then reconsider z2 = z as Element of L2 ;
reconsider z1 = z2 as Element of L1 by A1;
z2 is compact by A3, Th4;
then A4: z1 is compact by A1, Th9;
z2 <= y by A3, Th4;
then z1 <= x by A1, A2, YELLOW_0:1;
hence z in compactbelow x by A4; ::_thesis: verum
end;
then A5: compactbelow y c= compactbelow x by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_compactbelow_x_holds_
z_in_compactbelow_y
let z be set ; ::_thesis: ( z in compactbelow x implies z in compactbelow y )
assume A6: z in compactbelow x ; ::_thesis: z in compactbelow y
then reconsider z1 = z as Element of L1 ;
reconsider z2 = z1 as Element of L2 by A1;
z1 is compact by A6, Th4;
then A7: z2 is compact by A1, Th9;
z1 <= x by A6, Th4;
then z2 <= y by A1, A2, YELLOW_0:1;
hence z in compactbelow y by A7; ::_thesis: verum
end;
then compactbelow x c= compactbelow y by TARSKI:def_3;
hence compactbelow x = compactbelow y by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: WAYBEL_8:11
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & not L1 is empty holds
not L2 is empty ;
theorem Th12: :: WAYBEL_8:12
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is reflexive holds
L2 is reflexive
proof
let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is reflexive implies L2 is reflexive )
assume A1: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & the InternalRel of L1 is_reflexive_in the carrier of L1 ) ; :: according to ORDERS_2:def_2 ::_thesis: L2 is reflexive
let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of L2 or [x,x] in the InternalRel of L2 )
assume x in the carrier of L2 ; ::_thesis: [x,x] in the InternalRel of L2
hence [x,x] in the InternalRel of L2 by A1, RELAT_2:def_1; ::_thesis: verum
end;
theorem Th13: :: WAYBEL_8:13
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is transitive holds
L2 is transitive
proof
let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is transitive implies L2 is transitive )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is transitive ; ::_thesis: L2 is transitive
now__::_thesis:_for_x,_y,_z_being_Element_of_L2_st_x_<=_y_&_y_<=_z_holds_
x_<=_z
let x, y, z be Element of L2; ::_thesis: ( x <= y & y <= z implies x <= z )
reconsider x9 = x, y9 = y, z9 = z as Element of L1 by A1;
assume ( x <= y & y <= z ) ; ::_thesis: x <= z
then ( x9 <= y9 & y9 <= z9 ) by A1, YELLOW_0:1;
then x9 <= z9 by A2, YELLOW_0:def_2;
hence x <= z by A1, YELLOW_0:1; ::_thesis: verum
end;
hence L2 is transitive by YELLOW_0:def_2; ::_thesis: verum
end;
theorem Th14: :: WAYBEL_8:14
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is antisymmetric holds
L2 is antisymmetric
proof
let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is antisymmetric implies L2 is antisymmetric )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is antisymmetric ; ::_thesis: L2 is antisymmetric
now__::_thesis:_for_x,_y_being_Element_of_L2_st_x_<=_y_&_y_<=_x_holds_
x_=_y
let x, y be Element of L2; ::_thesis: ( x <= y & y <= x implies x = y )
reconsider x9 = x, y9 = y as Element of L1 by A1;
assume ( x <= y & y <= x ) ; ::_thesis: x = y
then ( x9 <= y9 & y9 <= x9 ) by A1, YELLOW_0:1;
hence x = y by A2, YELLOW_0:def_3; ::_thesis: verum
end;
hence L2 is antisymmetric by YELLOW_0:def_3; ::_thesis: verum
end;
theorem Th15: :: WAYBEL_8:15
for L1, L2 being non empty reflexive RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
L2 is up-complete
proof
let L1, L2 be non empty reflexive RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete implies L2 is up-complete )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is up-complete ; ::_thesis: L2 is up-complete
now__::_thesis:_for_X_being_non_empty_directed_Subset_of_L2_ex_x_being_Element_of_L2_st_
(_x_is_>=_than_X_&_(_for_y_being_Element_of_L2_st_y_is_>=_than_X_holds_
x_<=_y_)_)
let X be non empty directed Subset of L2; ::_thesis: ex x being Element of L2 st
( x is_>=_than X & ( for y being Element of L2 st y is_>=_than X holds
x <= y ) )
reconsider X9 = X as Subset of L1 by A1;
reconsider X9 = X9 as non empty directed Subset of L1 by A1, WAYBEL_0:3;
consider x9 being Element of L1 such that
A3: x9 is_>=_than X9 and
A4: for y9 being Element of L1 st y9 is_>=_than X9 holds
x9 <= y9 by A2, WAYBEL_0:def_39;
reconsider x = x9 as Element of L2 by A1;
take x = x; ::_thesis: ( x is_>=_than X & ( for y being Element of L2 st y is_>=_than X holds
x <= y ) )
thus x is_>=_than X by A1, A3, YELLOW_0:2; ::_thesis: for y being Element of L2 st y is_>=_than X holds
x <= y
let y be Element of L2; ::_thesis: ( y is_>=_than X implies x <= y )
assume A5: y is_>=_than X ; ::_thesis: x <= y
reconsider y9 = y as Element of L1 by A1;
x9 <= y9 by A1, A4, A5, YELLOW_0:2;
hence x <= y by A1, YELLOW_0:1; ::_thesis: verum
end;
hence L2 is up-complete by WAYBEL_0:def_39; ::_thesis: verum
end;
theorem Th16: :: WAYBEL_8:16
for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is satisfying_axiom_K & ( for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ) holds
L2 is satisfying_axiom_K
proof
let L1, L2 be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is satisfying_axiom_K & ( for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ) implies L2 is satisfying_axiom_K )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is satisfying_axiom_K and
A3: for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ; ::_thesis: L2 is satisfying_axiom_K
now__::_thesis:_for_x_being_Element_of_L2_holds_x_=_sup_(compactbelow_x)
let x be Element of L2; ::_thesis: x = sup (compactbelow x)
reconsider x9 = x as Element of L1 by A1;
( not compactbelow x9 is empty & compactbelow x9 is directed ) by A3;
then A4: ex_sup_of compactbelow x9,L1 by WAYBEL_0:75;
( x9 = sup (compactbelow x9) & compactbelow x = compactbelow x9 ) by A1, A2, Def3, Th10;
hence x = sup (compactbelow x) by A1, A4, YELLOW_0:26; ::_thesis: verum
end;
hence L2 is satisfying_axiom_K by Def3; ::_thesis: verum
end;
theorem Th17: :: WAYBEL_8:17
for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is algebraic holds
L2 is algebraic
proof
let L1, L2 be non empty reflexive antisymmetric RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is algebraic implies L2 is algebraic )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is algebraic ; ::_thesis: L2 is algebraic
A3: L2 is up-complete by A1, A2, Th15;
A4: for x being Element of L2 holds
( not compactbelow x is empty & compactbelow x is directed )
proof
let x be Element of L2; ::_thesis: ( not compactbelow x is empty & compactbelow x is directed )
reconsider x9 = x as Element of L1 by A1;
( not compactbelow x9 is empty & compactbelow x9 is directed ) by A2, Def4;
hence ( not compactbelow x is empty & compactbelow x is directed ) by A1, A2, A3, Th10, WAYBEL_0:3; ::_thesis: verum
end;
for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) by A2, Def4;
then L2 is satisfying_axiom_K by A1, A2, A3, Th16;
hence L2 is algebraic by A3, A4, Def4; ::_thesis: verum
end;
theorem Th18: :: WAYBEL_8:18
for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is arithmetic holds
L2 is arithmetic
proof
let L1, L2 be LATTICE; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is arithmetic implies L2 is arithmetic )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is arithmetic ; ::_thesis: L2 is arithmetic
A3: L2 is algebraic by A1, A2, Th17;
A4: CompactSublatt L1 is meet-inheriting by A2, Def5;
now__::_thesis:_for_x2,_y2_being_Element_of_L2_st_x2_in_the_carrier_of_(CompactSublatt_L2)_&_y2_in_the_carrier_of_(CompactSublatt_L2)_&_ex_inf_of_{x2,y2},L2_holds_
inf_{x2,y2}_in_the_carrier_of_(CompactSublatt_L2)
let x2, y2 be Element of L2; ::_thesis: ( x2 in the carrier of (CompactSublatt L2) & y2 in the carrier of (CompactSublatt L2) & ex_inf_of {x2,y2},L2 implies inf {x2,y2} in the carrier of (CompactSublatt L2) )
reconsider x1 = x2, y1 = y2 as Element of L1 by A1;
assume that
A5: x2 in the carrier of (CompactSublatt L2) and
A6: y2 in the carrier of (CompactSublatt L2) and
A7: ex_inf_of {x2,y2},L2 ; ::_thesis: inf {x2,y2} in the carrier of (CompactSublatt L2)
x2 is compact by A5, Def1;
then x1 is compact by A1, A3, Th9;
then A8: x1 in the carrier of (CompactSublatt L1) by Def1;
y2 is compact by A6, Def1;
then y1 is compact by A1, A3, Th9;
then A9: y1 in the carrier of (CompactSublatt L1) by Def1;
ex_inf_of {x1,y1},L1 by A1, A7, YELLOW_0:14;
then inf {x1,y1} in the carrier of (CompactSublatt L1) by A4, A8, A9, YELLOW_0:def_16;
then A10: inf {x1,y1} is compact by Def1;
inf {x1,y1} = inf {x2,y2} by A1, A7, YELLOW_0:27;
then inf {x2,y2} is compact by A1, A2, A10, Th9;
hence inf {x2,y2} in the carrier of (CompactSublatt L2) by Def1; ::_thesis: verum
end;
then CompactSublatt L2 is meet-inheriting by YELLOW_0:def_16;
hence L2 is arithmetic by A3, Def5; ::_thesis: verum
end;
registration
let L be non empty RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> non empty ;
coherence
not RelStr(# the carrier of L, the InternalRel of L #) is empty ;
end;
registration
let L be non empty reflexive RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> reflexive ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is reflexive by Th12;
end;
registration
let L be transitive RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> transitive ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is transitive by Th13;
end;
registration
let L be antisymmetric RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> antisymmetric ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is antisymmetric by Th14;
end;
registration
let L be with_infima RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> with_infima ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is with_infima by YELLOW_7:14;
end;
registration
let L be with_suprema RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> with_suprema ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is with_suprema by YELLOW_7:15;
end;
registration
let L be non empty reflexive up-complete RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> up-complete ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is up-complete by Th15;
end;
registration
let L be non empty reflexive antisymmetric algebraic RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> algebraic ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is algebraic by Th17;
end;
registration
let L be arithmetic LATTICE;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> arithmetic ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is arithmetic by Th18;
end;
theorem :: WAYBEL_8:19
for L being algebraic LATTICE holds
( L is arithmetic iff CompactSublatt L is LATTICE )
proof
let L be algebraic LATTICE; ::_thesis: ( L is arithmetic iff CompactSublatt L is LATTICE )
thus ( L is arithmetic implies CompactSublatt L is LATTICE ) ::_thesis: ( CompactSublatt L is LATTICE implies L is arithmetic )
proof
set x = the Element of L;
assume A1: L is arithmetic ; ::_thesis: CompactSublatt L is LATTICE
not compactbelow the Element of L is empty by Def4;
then consider z being set such that
A2: z in compactbelow the Element of L by XBOOLE_0:def_1;
ex z9 being Element of L st
( z9 = z & the Element of L >= z9 & z9 is compact ) by A2;
then CompactSublatt L is non empty full meet-inheriting join-inheriting SubRelStr of L by A1, Def1, Def5;
hence CompactSublatt L is LATTICE ; ::_thesis: verum
end;
assume A3: CompactSublatt L is LATTICE ; ::_thesis: L is arithmetic
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_inf_of_{x,y},L_holds_
inf_{x,y}_in_the_carrier_of_(CompactSublatt_L)
let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (CompactSublatt L) )
assume that
A4: x in the carrier of (CompactSublatt L) and
A5: y in the carrier of (CompactSublatt L) and
ex_inf_of {x,y},L ; ::_thesis: inf {x,y} in the carrier of (CompactSublatt L)
reconsider L9 = CompactSublatt L as non empty full SubRelStr of L by A4;
reconsider x9 = x, y9 = y as Element of L9 by A4, A5;
set X = compactbelow (inf {x,y});
reconsider c = "/\" ({x,y},L9) as Element of L by YELLOW_0:58;
A6: inf {x,y} = sup (compactbelow (inf {x,y})) by Def3;
( not compactbelow (inf {x,y}) is empty & compactbelow (inf {x,y}) is directed ) by Def4;
then A7: ex_sup_of compactbelow (inf {x,y}),L by WAYBEL_0:75;
A8: ex_inf_of {x9,y9},L9 by A3, YELLOW_0:21;
then A9: "/\" ({x,y},L9) is_<=_than {x,y} by YELLOW_0:31;
now__::_thesis:_for_z_being_set_st_z_in_compactbelow_(inf_{x,y})_holds_
z_in_(compactbelow_x)_/\_(compactbelow_y)
let z be set ; ::_thesis: ( z in compactbelow (inf {x,y}) implies z in (compactbelow x) /\ (compactbelow y) )
assume z in compactbelow (inf {x,y}) ; ::_thesis: z in (compactbelow x) /\ (compactbelow y)
then consider z1 being Element of L such that
A10: z = z1 and
A11: inf {x,y} >= z1 and
A12: z1 is compact ;
A13: z1 <= x "/\" y by A11, YELLOW_0:40;
x "/\" y <= y by YELLOW_0:23;
then z1 <= y by A13, ORDERS_2:3;
then A14: z in compactbelow y by A10, A12;
x "/\" y <= x by YELLOW_0:23;
then z1 <= x by A13, ORDERS_2:3;
then z in compactbelow x by A10, A12;
hence z in (compactbelow x) /\ (compactbelow y) by A14, XBOOLE_0:def_4; ::_thesis: verum
end;
then A15: compactbelow (inf {x,y}) c= (compactbelow x) /\ (compactbelow y) by TARSKI:def_3;
now__::_thesis:_for_b9_being_Element_of_L9_st_b9_in_compactbelow_(inf_{x,y})_holds_
b9_<=_"/\"_({x,y},L9)
let b9 be Element of L9; ::_thesis: ( b9 in compactbelow (inf {x,y}) implies b9 <= "/\" ({x,y},L9) )
reconsider b = b9 as Element of L by YELLOW_0:58;
assume A16: b9 in compactbelow (inf {x,y}) ; ::_thesis: b9 <= "/\" ({x,y},L9)
then b9 in compactbelow y by A15, XBOOLE_0:def_4;
then b <= y by Th4;
then A17: b9 <= y9 by YELLOW_0:60;
b9 in compactbelow x by A15, A16, XBOOLE_0:def_4;
then b <= x by Th4;
then b9 <= x9 by YELLOW_0:60;
then b9 <= x9 "/\" y9 by A8, A17, YELLOW_0:19;
hence b9 <= "/\" ({x,y},L9) by A3, YELLOW_0:40; ::_thesis: verum
end;
then A18: compactbelow (inf {x,y}) is_<=_than "/\" ({x,y},L9) by LATTICE3:def_9;
now__::_thesis:_for_d_being_set_st_d_in_compactbelow_(inf_{x,y})_holds_
d_in_the_carrier_of_L9
let d be set ; ::_thesis: ( d in compactbelow (inf {x,y}) implies d in the carrier of L9 )
assume d in compactbelow (inf {x,y}) ; ::_thesis: d in the carrier of L9
then ex d9 being Element of L st
( d9 = d & inf {x,y} >= d9 & d9 is compact ) ;
hence d in the carrier of L9 by Def1; ::_thesis: verum
end;
then compactbelow (inf {x,y}) c= the carrier of L9 by TARSKI:def_3;
then compactbelow (inf {x,y}) is_<=_than c by A18, YELLOW_0:62;
then A19: sup (compactbelow (inf {x,y})) <= c by A7, YELLOW_0:30;
y9 in {x,y} by TARSKI:def_2;
then "/\" ({x,y},L9) <= y9 by A9, LATTICE3:def_8;
then A20: c <= y by YELLOW_0:59;
x9 in {x,y} by TARSKI:def_2;
then "/\" ({x,y},L9) <= x9 by A9, LATTICE3:def_8;
then c <= x by YELLOW_0:59;
then c <= x "/\" y by A20, YELLOW_0:23;
then c <= sup (compactbelow (inf {x,y})) by A6, YELLOW_0:40;
then c = sup (compactbelow (inf {x,y})) by A19, ORDERS_2:2;
hence inf {x,y} in the carrier of (CompactSublatt L) by A6; ::_thesis: verum
end;
then CompactSublatt L is meet-inheriting by YELLOW_0:def_16;
hence L is arithmetic by Def5; ::_thesis: verum
end;
theorem Th20: :: WAYBEL_8:20
for L being lower-bounded algebraic LATTICE holds
( L is arithmetic iff L -waybelow is multiplicative )
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: ( L is arithmetic iff L -waybelow is multiplicative )
thus ( L is arithmetic implies L -waybelow is multiplicative ) ::_thesis: ( L -waybelow is multiplicative implies L is arithmetic )
proof
assume A1: L is arithmetic ; ::_thesis: L -waybelow is multiplicative
now__::_thesis:_for_a,_x,_y_being_Element_of_L_st_[a,x]_in_L_-waybelow_&_[a,y]_in_L_-waybelow_holds_
[a,(x_"/\"_y)]_in_L_-waybelow
reconsider C = CompactSublatt L as non empty full meet-inheriting SubRelStr of L by A1, Def5;
let a, x, y be Element of L; ::_thesis: ( [a,x] in L -waybelow & [a,y] in L -waybelow implies [a,(x "/\" y)] in L -waybelow )
assume that
A2: [a,x] in L -waybelow and
A3: [a,y] in L -waybelow ; ::_thesis: [a,(x "/\" y)] in L -waybelow
a << x by A2, WAYBEL_4:def_1;
then consider c being Element of L such that
A4: c in the carrier of (CompactSublatt L) and
A5: a <= c and
A6: c <= x by Th7;
a << y by A3, WAYBEL_4:def_1;
then consider k being Element of L such that
A7: k in the carrier of (CompactSublatt L) and
A8: a <= k and
A9: k <= y by Th7;
A10: c "/\" k <= x "/\" y by A6, A9, YELLOW_3:2;
reconsider c9 = c, k9 = k as Element of C by A4, A7;
c9 "/\" k9 in the carrier of (CompactSublatt L) ;
then c "/\" k in the carrier of (CompactSublatt L) by YELLOW_0:69;
then c "/\" k is compact by Def1;
then A11: c "/\" k << c "/\" k by WAYBEL_3:def_2;
a "/\" a = a by YELLOW_5:2;
then a <= c "/\" k by A5, A8, YELLOW_3:2;
then a << x "/\" y by A10, A11, WAYBEL_3:2;
hence [a,(x "/\" y)] in L -waybelow by WAYBEL_4:def_1; ::_thesis: verum
end;
hence L -waybelow is multiplicative by WAYBEL_7:def_7; ::_thesis: verum
end;
assume A12: L -waybelow is multiplicative ; ::_thesis: L is arithmetic
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_inf_of_{x,y},L_holds_
inf_{x,y}_in_the_carrier_of_(CompactSublatt_L)
let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (CompactSublatt L) )
assume that
A13: x in the carrier of (CompactSublatt L) and
A14: y in the carrier of (CompactSublatt L) and
ex_inf_of {x,y},L ; ::_thesis: inf {x,y} in the carrier of (CompactSublatt L)
y is compact by A14, Def1;
then y << y by WAYBEL_3:def_2;
then A15: [y,y] in L -waybelow by WAYBEL_4:def_1;
x is compact by A13, Def1;
then x << x by WAYBEL_3:def_2;
then [x,x] in L -waybelow by WAYBEL_4:def_1;
then [(x "/\" y),(x "/\" y)] in L -waybelow by A12, A15, WAYBEL_7:41;
then x "/\" y << x "/\" y by WAYBEL_4:def_1;
then x "/\" y is compact by WAYBEL_3:def_2;
then x "/\" y in the carrier of (CompactSublatt L) by Def1;
hence inf {x,y} in the carrier of (CompactSublatt L) by YELLOW_0:40; ::_thesis: verum
end;
then CompactSublatt L is meet-inheriting by YELLOW_0:def_16;
hence L is arithmetic by Def5; ::_thesis: verum
end;
theorem :: WAYBEL_8:21
for L being lower-bounded arithmetic LATTICE
for p being Element of L st p is pseudoprime holds
p is prime
proof
let L be lower-bounded arithmetic LATTICE; ::_thesis: for p being Element of L st p is pseudoprime holds
p is prime
let p be Element of L; ::_thesis: ( p is pseudoprime implies p is prime )
L -waybelow is multiplicative by Th20;
hence ( p is pseudoprime implies p is prime ) by WAYBEL_7:45; ::_thesis: verum
end;
theorem :: WAYBEL_8:22
for L being lower-bounded distributive algebraic LATTICE st ( for p being Element of L st p is pseudoprime holds
p is prime ) holds
L is arithmetic
proof
let L be lower-bounded distributive algebraic LATTICE; ::_thesis: ( ( for p being Element of L st p is pseudoprime holds
p is prime ) implies L is arithmetic )
assume for p being Element of L st p is pseudoprime holds
p is prime ; ::_thesis: L is arithmetic
then L -waybelow is multiplicative by WAYBEL_7:46;
hence L is arithmetic by Th20; ::_thesis: verum
end;
registration
let L be algebraic LATTICE;
let c be closure Function of L,L;
cluster non empty directed for Element of bool the carrier of (Image c);
existence
ex b1 being Subset of (Image c) st
( not b1 is empty & b1 is directed )
proof
set x = the Element of (Image c);
take downarrow the Element of (Image c) ; ::_thesis: ( not downarrow the Element of (Image c) is empty & downarrow the Element of (Image c) is directed )
thus ( not downarrow the Element of (Image c) is empty & downarrow the Element of (Image c) is directed ) ; ::_thesis: verum
end;
end;
theorem Th23: :: WAYBEL_8:23
for L being algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
proof
let L be algebraic LATTICE; ::_thesis: for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
let c be closure Function of L,L; ::_thesis: ( c is directed-sups-preserving implies c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) )
assume A1: c is directed-sups-preserving ; ::_thesis: c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in c .: ([#] (CompactSublatt L)) or x in [#] (CompactSublatt (Image c)) )
A2: ( c is idempotent & c is monotone ) by WAYBEL_1:def_13;
assume x in c .: ([#] (CompactSublatt L)) ; ::_thesis: x in [#] (CompactSublatt (Image c))
then consider y being set such that
A3: y in dom c and
A4: y in [#] (CompactSublatt L) and
A5: x = c . y by FUNCT_1:def_6;
A6: x in rng c by A3, A5, FUNCT_1:def_3;
then reconsider x9 = x as Element of (Image c) by YELLOW_0:def_15;
reconsider x1 = x9 as Element of L by A6;
reconsider y9 = y as Element of L by A3;
y9 is compact by A4, Def1;
then A7: y9 << y9 by WAYBEL_3:def_2;
now__::_thesis:_for_D_being_non_empty_directed_Subset_of_(Image_c)_st_x9_<=_sup_D_holds_
ex_d_being_Element_of_(Image_c)_st_
(_d_in_D_&_x9_<=_d_)
id L <= c by WAYBEL_1:def_14;
then (id L) . y9 <= c . y9 by YELLOW_2:9;
then A8: y9 <= x1 by A5, FUNCT_1:18;
let D be non empty directed Subset of (Image c); ::_thesis: ( x9 <= sup D implies ex d being Element of (Image c) st
( d in D & x9 <= d ) )
assume A9: x9 <= sup D ; ::_thesis: ex d being Element of (Image c) st
( d in D & x9 <= d )
D c= the carrier of (Image c) ;
then A10: D c= rng c by YELLOW_0:def_15;
then reconsider D9 = D as non empty Subset of L by XBOOLE_1:1;
reconsider D9 = D9 as non empty directed Subset of L by YELLOW_2:7;
A11: ex_sup_of D9,L by WAYBEL_0:75;
c preserves_sup_of D9 by A1, WAYBEL_0:def_37;
then A12: c . (sup D9) = sup (c .: D9) by A11, WAYBEL_0:def_31
.= sup D9 by A2, A10, YELLOW_2:20 ;
c . (sup D9) = sup D by A11, WAYBEL_1:55;
then x1 <= sup D9 by A9, A12, YELLOW_0:59;
then y9 <= sup D9 by A8, ORDERS_2:3;
then consider d9 being Element of L such that
A13: d9 in D9 and
A14: y9 <= d9 by A7, WAYBEL_3:def_1;
reconsider d = d9 as Element of (Image c) by A13;
take d = d; ::_thesis: ( d in D & x9 <= d )
thus d in D by A13; ::_thesis: x9 <= d
d in the carrier of (Image c) ;
then d in rng c by YELLOW_0:def_15;
then d9 in { z where z is Element of L : z = c . z } by A2, YELLOW_2:19;
then A15: ex z9 being Element of L st
( d9 = z9 & z9 = c . z9 ) ;
c . y9 <= c . d9 by A2, A14, WAYBEL_1:def_2;
hence x9 <= d by A5, A15, YELLOW_0:60; ::_thesis: verum
end;
then x9 << x9 by WAYBEL_3:def_1;
then x9 is compact by WAYBEL_3:def_2;
hence x in [#] (CompactSublatt (Image c)) by Def1; ::_thesis: verum
end;
theorem :: WAYBEL_8:24
for L being lower-bounded algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
Image c is algebraic LATTICE
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: for c being closure Function of L,L st c is directed-sups-preserving holds
Image c is algebraic LATTICE
let c be closure Function of L,L; ::_thesis: ( c is directed-sups-preserving implies Image c is algebraic LATTICE )
assume A1: c is directed-sups-preserving ; ::_thesis: Image c is algebraic LATTICE
c is idempotent by WAYBEL_1:def_13;
then reconsider Imc = Image c as complete LATTICE by A1, YELLOW_2:35;
A2: now__::_thesis:_for_x_being_Element_of_Imc_holds_
(_not_compactbelow_x_is_empty_&_compactbelow_x_is_directed_)
let x be Element of Imc; ::_thesis: ( not compactbelow x is empty & compactbelow x is directed )
now__::_thesis:_for_y,_z_being_Element_of_Imc_st_y_in_compactbelow_x_&_z_in_compactbelow_x_holds_
ex_v_being_Element_of_the_carrier_of_Imc_st_
(_v_in_compactbelow_x_&_y_<=_v_&_z_<=_v_)
let y, z be Element of Imc; ::_thesis: ( y in compactbelow x & z in compactbelow x implies ex v being Element of the carrier of Imc st
( v in compactbelow x & y <= v & z <= v ) )
assume that
A3: y in compactbelow x and
A4: z in compactbelow x ; ::_thesis: ex v being Element of the carrier of Imc st
( v in compactbelow x & y <= v & z <= v )
y is compact by A3, Th4;
then A5: y << y by WAYBEL_3:def_2;
z is compact by A4, Th4;
then A6: z << z by WAYBEL_3:def_2;
take v = y "\/" z; ::_thesis: ( v in compactbelow x & y <= v & z <= v )
z <= v by YELLOW_0:22;
then A7: z << v by A6, WAYBEL_3:2;
y <= v by YELLOW_0:22;
then y << v by A5, WAYBEL_3:2;
then v << v by A7, WAYBEL_3:3;
then A8: v is compact by WAYBEL_3:def_2;
( y <= x & z <= x ) by A3, A4, Th4;
then v <= x by YELLOW_0:22;
hence ( v in compactbelow x & y <= v & z <= v ) by A8, YELLOW_0:22; ::_thesis: verum
end;
hence ( not compactbelow x is empty & compactbelow x is directed ) by WAYBEL_0:def_1; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Element_of_Imc_holds_x_=_sup_(compactbelow_x)
let x be Element of Imc; ::_thesis: x = sup (compactbelow x)
consider y being Element of L such that
A9: c . y = x by YELLOW_2:10;
sup (compactbelow y) in the carrier of L ;
then A10: sup (compactbelow y) in dom c by FUNCT_2:def_1;
( not compactbelow y is empty & compactbelow y is directed ) by Def4;
then A11: ( c preserves_sup_of compactbelow y & ex_sup_of compactbelow y,L ) by A1, WAYBEL_0:75, WAYBEL_0:def_37;
then c . (sup (compactbelow y)) = sup (c .: (compactbelow y)) by WAYBEL_0:def_31;
then sup (c .: (compactbelow y)) in rng c by A10, FUNCT_1:def_3;
then A12: ( ex_sup_of c .: (compactbelow y),L & sup (c .: (compactbelow y)) in the carrier of (Image c) ) by YELLOW_0:17, YELLOW_0:def_15;
for b being Element of Imc st b in compactbelow x holds
b <= x by Th4;
then x is_>=_than compactbelow x by LATTICE3:def_9;
then A13: sup (compactbelow x) <= x by YELLOW_0:32;
A14: c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) by A1, Th23;
A15: c is monotone by A1, YELLOW_2:16;
compactbelow y = (downarrow y) /\ ([#] (CompactSublatt L)) by Th5;
then A16: c .: (compactbelow y) c= (c .: (downarrow y)) /\ (c .: ([#] (CompactSublatt L))) by RELAT_1:121;
now__::_thesis:_for_z_being_set_st_z_in_c_.:_(compactbelow_y)_holds_
z_in_compactbelow_x
let z be set ; ::_thesis: ( z in c .: (compactbelow y) implies z in compactbelow x )
assume A17: z in c .: (compactbelow y) ; ::_thesis: z in compactbelow x
then consider v being set such that
A18: v in dom c and
A19: v in compactbelow y and
A20: z = c . v by FUNCT_1:def_6;
z in rng c by A18, A20, FUNCT_1:def_3;
then reconsider z1 = z as Element of Imc by YELLOW_0:def_15;
reconsider v = v as Element of L by A18;
v <= y by A19, Th4;
then c . v <= c . y by A15, WAYBEL_1:def_2;
then A21: z1 <= x by A9, A20, YELLOW_0:60;
z in c .: ([#] (CompactSublatt L)) by A16, A17, XBOOLE_0:def_4;
then z1 is compact by A14, Def1;
hence z in compactbelow x by A21; ::_thesis: verum
end;
then A22: c .: (compactbelow y) c= compactbelow x by TARSKI:def_3;
compactbelow x is directed by A2;
then A23: ex_sup_of compactbelow x,Imc by WAYBEL_0:75;
c .: (compactbelow y) c= rng c by RELAT_1:111;
then c .: (compactbelow y) is Subset of Imc by YELLOW_0:def_15;
then A24: ( ex_sup_of c .: (compactbelow y),Imc & sup (c .: (compactbelow y)) = "\/" ((c .: (compactbelow y)),Imc) ) by A12, YELLOW_0:64;
c . y = c . (sup (compactbelow y)) by Def3
.= sup (c .: (compactbelow y)) by A11, WAYBEL_0:def_31 ;
then x <= sup (compactbelow x) by A9, A23, A24, A22, YELLOW_0:34;
hence x = sup (compactbelow x) by A13, ORDERS_2:2; ::_thesis: verum
end;
then Imc is satisfying_axiom_K by Def3;
hence Image c is algebraic LATTICE by A2, Def4; ::_thesis: verum
end;
theorem :: WAYBEL_8:25
for L being lower-bounded algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))
let c be closure Function of L,L; ::_thesis: ( c is directed-sups-preserving implies c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) )
assume A1: c is directed-sups-preserving ; ::_thesis: c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))
now__::_thesis:_for_a9_being_set_st_a9_in_[#]_(CompactSublatt_(Image_c))_holds_
a9_in_c_.:_([#]_(CompactSublatt_L))
c is idempotent by WAYBEL_1:def_13;
then A2: rng c = { x where x is Element of L : x = c . x } by YELLOW_2:19;
c is idempotent by WAYBEL_1:def_13;
then reconsider Imc = Image c as complete LATTICE by A1, YELLOW_2:35;
let a9 be set ; ::_thesis: ( a9 in [#] (CompactSublatt (Image c)) implies a9 in c .: ([#] (CompactSublatt L)) )
assume A3: a9 in [#] (CompactSublatt (Image c)) ; ::_thesis: a9 in c .: ([#] (CompactSublatt L))
A4: the carrier of (CompactSublatt Imc) c= the carrier of Imc by YELLOW_0:def_13;
then reconsider a = a9 as Element of Imc by A3;
a is compact by A3, Def1;
then A5: a << a by WAYBEL_3:def_2;
a9 in the carrier of Imc by A3, A4;
then a in rng c by YELLOW_0:def_15;
then consider a1 being Element of L such that
A6: a = a1 and
A7: a1 = c . a1 by A2;
compactbelow a1 is non empty directed Subset of L by Def4;
then A8: ( c preserves_sup_of compactbelow a1 & ex_sup_of compactbelow a1,L ) by A1, WAYBEL_0:75, WAYBEL_0:def_37;
A9: c is monotone by A1, YELLOW_2:16;
now__::_thesis:_for_z_being_set_st_z_in_c_.:_(compactbelow_a1)_holds_
z_in_(downarrow_a1)_/\_(c_.:_([#]_(CompactSublatt_L)))
let z be set ; ::_thesis: ( z in c .: (compactbelow a1) implies z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) )
assume z in c .: (compactbelow a1) ; ::_thesis: z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L)))
then consider v being set such that
A10: v in dom c and
A11: v in compactbelow a1 and
A12: z = c . v by FUNCT_1:def_6;
reconsider v9 = v as Element of L by A11;
A13: v in (downarrow a1) /\ the carrier of (CompactSublatt L) by A11, Th5;
then v in downarrow a1 by XBOOLE_0:def_4;
then v9 <= a1 by WAYBEL_0:17;
then c . v9 <= a1 by A7, A9, WAYBEL_1:def_2;
then A14: z in downarrow a1 by A12, WAYBEL_0:17;
v in [#] (CompactSublatt L) by A13, XBOOLE_0:def_4;
then z in c .: ([#] (CompactSublatt L)) by A10, A12, FUNCT_1:def_6;
hence z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) by A14, XBOOLE_0:def_4; ::_thesis: verum
end;
then A15: c .: (compactbelow a1) c= (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) by TARSKI:def_3;
a = sup (compactbelow a1) by A6, Def3;
then A16: a = sup (c .: (compactbelow a1)) by A6, A7, A8, WAYBEL_0:def_31;
c .: (compactbelow a1) c= rng c by RELAT_1:111;
then A17: c .: (compactbelow a1) c= the carrier of Imc by YELLOW_0:def_15;
A18: (downarrow a) /\ (c .: ([#] (CompactSublatt L))) is non empty directed Subset of Imc
proof
(c .: ([#] (CompactSublatt L))) /\ (downarrow a) is Subset of Imc ;
then reconsider D = (downarrow a) /\ (c .: ([#] (CompactSublatt L))) as Subset of Imc ;
A19: Bottom Imc <= a by YELLOW_0:44;
A20: now__::_thesis:_for_x,_y_being_Element_of_Imc_st_x_in_D_&_y_in_D_holds_
ex_z_being_Element_of_Imc_st_
(_z_in_D_&_x_<=_z_&_y_<=_z_)
let x, y be Element of Imc; ::_thesis: ( x in D & y in D implies ex z being Element of Imc st
( z in D & x <= z & y <= z ) )
assume that
A21: x in D and
A22: y in D ; ::_thesis: ex z being Element of Imc st
( z in D & x <= z & y <= z )
x in c .: ([#] (CompactSublatt L)) by A21, XBOOLE_0:def_4;
then consider d being set such that
A23: d in dom c and
A24: d in [#] (CompactSublatt L) and
A25: x = c . d by FUNCT_1:def_6;
y in c .: ([#] (CompactSublatt L)) by A22, XBOOLE_0:def_4;
then consider e being set such that
A26: e in dom c and
A27: e in [#] (CompactSublatt L) and
A28: y = c . e by FUNCT_1:def_6;
reconsider e = e as Element of L by A26;
y in downarrow a by A22, XBOOLE_0:def_4;
then y <= a by WAYBEL_0:17;
then A29: c . e <= a1 by A6, A28, YELLOW_0:59;
reconsider d = d as Element of L by A23;
A30: d <= d "\/" e by YELLOW_0:22;
x in downarrow a by A21, XBOOLE_0:def_4;
then x <= a by WAYBEL_0:17;
then c . d <= a1 by A6, A25, YELLOW_0:59;
then A31: (c . d) "\/" (c . e) <= a1 by A29, YELLOW_0:22;
d "\/" e in the carrier of L ;
then d "\/" e in dom c by FUNCT_2:def_1;
then c . (d "\/" e) in rng c by FUNCT_1:def_3;
then reconsider z = c . (d "\/" e) as Element of Imc by YELLOW_0:def_15;
take z = z; ::_thesis: ( z in D & x <= z & y <= z )
A32: id L <= c by WAYBEL_1:def_14;
then (id L) . e <= c . e by YELLOW_2:9;
then A33: e <= c . e by FUNCT_1:18;
(id L) . d <= c . d by A32, YELLOW_2:9;
then d <= c . d by FUNCT_1:18;
then d "\/" e <= (c . d) "\/" (c . e) by A33, YELLOW_3:3;
then d "\/" e <= a1 by A31, ORDERS_2:3;
then c . (d "\/" e) <= a1 by A7, A9, WAYBEL_1:def_2;
then z <= a by A6, YELLOW_0:60;
then A34: z in downarrow a by WAYBEL_0:17;
A35: e <= d "\/" e by YELLOW_0:22;
then A36: c . e <= c . (d "\/" e) by A9, WAYBEL_1:def_2;
e is compact by A27, Def1;
then e << e by WAYBEL_3:def_2;
then A37: e << d "\/" e by A35, WAYBEL_3:2;
d is compact by A24, Def1;
then d << d by WAYBEL_3:def_2;
then d << d "\/" e by A30, WAYBEL_3:2;
then d "\/" e << d "\/" e by A37, WAYBEL_3:3;
then d "\/" e is compact by WAYBEL_3:def_2;
then A38: d "\/" e in [#] (CompactSublatt L) by Def1;
d "\/" e in the carrier of L ;
then d "\/" e in dom c by FUNCT_2:def_1;
then z in c .: ([#] (CompactSublatt L)) by A38, FUNCT_1:def_6;
hence z in D by A34, XBOOLE_0:def_4; ::_thesis: ( x <= z & y <= z )
c . d <= c . (d "\/" e) by A9, A30, WAYBEL_1:def_2;
hence ( x <= z & y <= z ) by A25, A28, A36, YELLOW_0:60; ::_thesis: verum
end;
Bottom L is compact by WAYBEL_3:15;
then ( dom c = the carrier of L & Bottom L in [#] (CompactSublatt L) ) by Def1, FUNCT_2:def_1;
then A39: c . (Bottom L) in c .: ([#] (CompactSublatt L)) by FUNCT_1:def_6;
A40: ( ex_sup_of {} ,L & {} c= the carrier of L ) by XBOOLE_1:2, YELLOW_0:42;
A41: {} c= the carrier of Imc by XBOOLE_1:2;
c . (Bottom L) = c . ("\/" ({},L)) by YELLOW_0:def_11
.= "\/" ({},Imc) by A40, A41, WAYBEL_1:55
.= Bottom Imc by YELLOW_0:def_11 ;
then c . (Bottom L) in downarrow a by A19, WAYBEL_0:17;
hence (downarrow a) /\ (c .: ([#] (CompactSublatt L))) is non empty directed Subset of Imc by A39, A20, WAYBEL_0:def_1, XBOOLE_0:def_4; ::_thesis: verum
end;
A42: c .: ([#] (CompactSublatt L)) c= rng c by RELAT_1:111;
now__::_thesis:_for_z_being_set_st_z_in_(downarrow_a1)_/\_(c_.:_([#]_(CompactSublatt_L)))_holds_
z_in_(downarrow_a)_/\_(c_.:_([#]_(CompactSublatt_L)))
let z be set ; ::_thesis: ( z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) implies z in (downarrow a) /\ (c .: ([#] (CompactSublatt L))) )
assume A43: z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) ; ::_thesis: z in (downarrow a) /\ (c .: ([#] (CompactSublatt L)))
then reconsider z1 = z as Element of L ;
A44: z in c .: ([#] (CompactSublatt L)) by A43, XBOOLE_0:def_4;
then reconsider z2 = z1 as Element of Imc by A42, YELLOW_0:def_15;
z in downarrow a1 by A43, XBOOLE_0:def_4;
then z1 <= a1 by WAYBEL_0:17;
then z2 <= a by A6, YELLOW_0:60;
then z in downarrow a by WAYBEL_0:17;
hence z in (downarrow a) /\ (c .: ([#] (CompactSublatt L))) by A44, XBOOLE_0:def_4; ::_thesis: verum
end;
then A45: (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) c= (downarrow a) /\ (c .: ([#] (CompactSublatt L))) by TARSKI:def_3;
ex_sup_of c .: (compactbelow a1),L by A8, WAYBEL_0:def_31;
then A46: a = "\/" ((c .: (compactbelow a1)),Imc) by A6, A7, A17, A16, WAYBEL_1:55;
( ex_sup_of c .: (compactbelow a1),Imc & ex_sup_of (downarrow a) /\ (c .: ([#] (CompactSublatt L))),Imc ) by YELLOW_0:17;
then a <= "\/" (((downarrow a) /\ (c .: ([#] (CompactSublatt L)))),Imc) by A46, A15, A45, XBOOLE_1:1, YELLOW_0:34;
then consider k being Element of Imc such that
A47: k in (downarrow a) /\ (c .: ([#] (CompactSublatt L))) and
A48: a <= k by A5, A18, WAYBEL_3:def_1;
k in downarrow a by A47, XBOOLE_0:def_4;
then A49: k <= a by WAYBEL_0:17;
k in c .: ([#] (CompactSublatt L)) by A47, XBOOLE_0:def_4;
hence a9 in c .: ([#] (CompactSublatt L)) by A48, A49, ORDERS_2:2; ::_thesis: verum
end;
then A50: [#] (CompactSublatt (Image c)) c= c .: ([#] (CompactSublatt L)) by TARSKI:def_3;
c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) by A1, Th23;
hence c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) by A50, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
theorem Th26: :: WAYBEL_8:26
for X, x being set holds
( x is Element of (BoolePoset X) iff x c= X )
proof
let X, x be set ; ::_thesis: ( x is Element of (BoolePoset X) iff x c= X )
LattPOSet (BooleLatt X) = RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) by LATTICE3:def_2;
then A1: the carrier of (BoolePoset X) = the carrier of (BooleLatt X) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
hence ( x is Element of (BoolePoset X) implies x c= X ) ; ::_thesis: ( x c= X implies x is Element of (BoolePoset X) )
thus ( x c= X implies x is Element of (BoolePoset X) ) by A1; ::_thesis: verum
end;
theorem Th27: :: WAYBEL_8:27
for X being set
for x, y being Element of (BoolePoset X) holds
( x << y iff for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z )
proof
let X be set ; ::_thesis: for x, y being Element of (BoolePoset X) holds
( x << y iff for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z )
let x, y be Element of (BoolePoset X); ::_thesis: ( x << y iff for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z )
LattPOSet (BooleLatt X) = RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) by LATTICE3:def_2;
then A1: the carrier of (BoolePoset X) = the carrier of (BooleLatt X) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
thus ( x << y implies for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ) ::_thesis: ( ( for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ) implies x << y )
proof
assume A2: x << y ; ::_thesis: for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z
let Y be Subset-Family of X; ::_thesis: ( y c= union Y implies ex Z being finite Subset of Y st x c= union Z )
reconsider Y9 = Y as Subset of (BoolePoset X) by A1;
assume y c= union Y ; ::_thesis: ex Z being finite Subset of Y st x c= union Z
then y c= sup Y9 by YELLOW_1:21;
then y <= sup Y9 by YELLOW_1:2;
then consider Z being finite Subset of (BoolePoset X) such that
A3: Z c= Y and
A4: x <= sup Z by A2, WAYBEL_3:18;
reconsider Z9 = Z as finite Subset of Y by A3;
take Z9 ; ::_thesis: x c= union Z9
x c= sup Z by A4, YELLOW_1:2;
hence x c= union Z9 by YELLOW_1:21; ::_thesis: verum
end;
thus ( ( for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ) implies x << y ) ::_thesis: verum
proof
assume A5: for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ; ::_thesis: x << y
now__::_thesis:_for_Y_being_Subset_of_(BoolePoset_X)_st_y_<=_sup_Y_holds_
ex_Z_being_finite_Subset_of_(BoolePoset_X)_st_
(_Z_c=_Y_&_x_<=_sup_Z_)
let Y be Subset of (BoolePoset X); ::_thesis: ( y <= sup Y implies ex Z being finite Subset of (BoolePoset X) st
( Z c= Y & x <= sup Z ) )
reconsider Y9 = Y as Subset-Family of X by A1;
assume y <= sup Y ; ::_thesis: ex Z being finite Subset of (BoolePoset X) st
( Z c= Y & x <= sup Z )
then y c= sup Y by YELLOW_1:2;
then y c= union Y9 by YELLOW_1:21;
then consider Z9 being finite Subset of Y9 such that
A6: x c= union Z9 by A5;
reconsider Z = Z9 as finite Subset of (BoolePoset X) by XBOOLE_1:1;
take Z = Z; ::_thesis: ( Z c= Y & x <= sup Z )
thus Z c= Y ; ::_thesis: x <= sup Z
x c= sup Z by A6, YELLOW_1:21;
hence x <= sup Z by YELLOW_1:2; ::_thesis: verum
end;
hence x << y by WAYBEL_3:19; ::_thesis: verum
end;
end;
theorem Th28: :: WAYBEL_8:28
for X being set
for x being Element of (BoolePoset X) holds
( x is finite iff x is compact )
proof
let X be set ; ::_thesis: for x being Element of (BoolePoset X) holds
( x is finite iff x is compact )
let x be Element of (BoolePoset X); ::_thesis: ( x is finite iff x is compact )
percases ( x is empty or not x is empty ) ;
supposeA1: x is empty ; ::_thesis: ( x is finite iff x is compact )
then x = Bottom (BoolePoset X) by YELLOW_1:18;
hence ( x is finite iff x is compact ) by A1, WAYBEL_3:15; ::_thesis: verum
end;
supposeA2: not x is empty ; ::_thesis: ( x is finite iff x is compact )
thus ( x is finite implies x is compact ) ::_thesis: ( x is compact implies x is finite )
proof
assume A3: x is finite ; ::_thesis: x is compact
now__::_thesis:_for_Y_being_Subset-Family_of_X_st_x_c=_union_Y_holds_
ex_Z_being_finite_Subset_of_Y_st_x_c=_union_Z
defpred S1[ set , set ] means $1 in $2;
let Y be Subset-Family of X; ::_thesis: ( x c= union Y implies ex Z being finite Subset of Y st x c= union Z )
assume A4: x c= union Y ; ::_thesis: ex Z being finite Subset of Y st x c= union Z
A5: for e being set st e in x holds
ex u being set st
( u in Y & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in x implies ex u being set st
( u in Y & S1[e,u] ) )
assume e in x ; ::_thesis: ex u being set st
( u in Y & S1[e,u] )
then ex u being set st
( e in u & u in Y ) by A4, TARSKI:def_4;
hence ex u being set st
( u in Y & S1[e,u] ) ; ::_thesis: verum
end;
consider f being Function such that
A6: dom f = x and
A7: rng f c= Y and
A8: for e being set st e in x holds
S1[e,f . e] from FUNCT_1:sch_5(A5);
reconsider Z = rng f as Subset of Y by A7;
reconsider Z = Z as finite Subset of Y by A3, A6, FINSET_1:8;
take Z = Z; ::_thesis: x c= union Z
now__::_thesis:_for_z_being_set_st_z_in_x_holds_
z_in_union_Z
let z be set ; ::_thesis: ( z in x implies z in union Z )
assume z in x ; ::_thesis: z in union Z
then ( z in f . z & f . z in Z ) by A6, A8, FUNCT_1:def_3;
hence z in union Z by TARSKI:def_4; ::_thesis: verum
end;
hence x c= union Z by TARSKI:def_3; ::_thesis: verum
end;
then x << x by Th27;
hence x is compact by WAYBEL_3:def_2; ::_thesis: verum
end;
thus ( x is compact implies x is finite ) ::_thesis: verum
proof
reconsider x9 = x as non empty set by A2;
set Y = { {y} where y is Element of x9 : verum } ;
{ {y} where y is Element of x9 : verum } c= bool X
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { {y} where y is Element of x9 : verum } or t in bool X )
assume t in { {y} where y is Element of x9 : verum } ; ::_thesis: t in bool X
then A9: ex y9 being Element of x9 st t = {y9} ;
now__::_thesis:_for_k_being_set_st_k_in_t_holds_
k_in_X
let k be set ; ::_thesis: ( k in t implies k in X )
assume A10: k in t ; ::_thesis: k in X
x c= X by Th26;
hence k in X by A9, A10, TARSKI:def_3; ::_thesis: verum
end;
then t c= X by TARSKI:def_3;
hence t in bool X ; ::_thesis: verum
end;
then reconsider Y = { {y} where y is Element of x9 : verum } as Subset-Family of X ;
now__::_thesis:_for_y_being_set_st_y_in_x_holds_
y_in_union_Y
let y be set ; ::_thesis: ( y in x implies y in union Y )
assume y in x ; ::_thesis: y in union Y
then A11: {y} in Y ;
y in {y} by TARSKI:def_1;
hence y in union Y by A11, TARSKI:def_4; ::_thesis: verum
end;
then A12: x c= union Y by TARSKI:def_3;
assume x is compact ; ::_thesis: x is finite
then x << x by WAYBEL_3:def_2;
then consider Z being finite Subset of Y such that
A13: x c= union Z by A12, Th27;
now__::_thesis:_for_k_being_set_st_k_in_Z_holds_
k_is_finite
let k be set ; ::_thesis: ( k in Z implies k is finite )
assume k in Z ; ::_thesis: k is finite
then k in Y ;
then ex y9 being Element of x9 st k = {y9} ;
hence k is finite ; ::_thesis: verum
end;
then union Z is finite by FINSET_1:7;
hence x is finite by A13; ::_thesis: verum
end;
end;
end;
end;
theorem Th29: :: WAYBEL_8:29
for X being set
for x being Element of (BoolePoset X) holds compactbelow x = { y where y is finite Subset of x : verum }
proof
let X be set ; ::_thesis: for x being Element of (BoolePoset X) holds compactbelow x = { y where y is finite Subset of x : verum }
let x be Element of (BoolePoset X); ::_thesis: compactbelow x = { y where y is finite Subset of x : verum }
now__::_thesis:_for_z_being_set_st_z_in__{__y_where_y_is_finite_Subset_of_x_:_verum__}__holds_
z_in_compactbelow_x
let z be set ; ::_thesis: ( z in { y where y is finite Subset of x : verum } implies z in compactbelow x )
assume z in { y where y is finite Subset of x : verum } ; ::_thesis: z in compactbelow x
then consider z9 being finite Subset of x such that
A1: z9 = z ;
x c= X by Th26;
then z9 c= X by XBOOLE_1:1;
then reconsider z1 = z9 as Element of (BoolePoset X) by Th26;
( z1 is compact & z1 <= x ) by Th28, YELLOW_1:2;
hence z in compactbelow x by A1; ::_thesis: verum
end;
then A2: { y where y is finite Subset of x : verum } c= compactbelow x by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_compactbelow_x_holds_
z_in__{__y_where_y_is_finite_Subset_of_x_:_verum__}_
let z be set ; ::_thesis: ( z in compactbelow x implies z in { y where y is finite Subset of x : verum } )
assume z in compactbelow x ; ::_thesis: z in { y where y is finite Subset of x : verum }
then consider z9 being Element of (BoolePoset X) such that
A3: z9 = z and
A4: ( x >= z9 & z9 is compact ) ;
( z is finite & z9 c= x ) by A3, A4, Th28, YELLOW_1:2;
hence z in { y where y is finite Subset of x : verum } by A3; ::_thesis: verum
end;
then compactbelow x c= { y where y is finite Subset of x : verum } by TARSKI:def_3;
hence compactbelow x = { y where y is finite Subset of x : verum } by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: WAYBEL_8:30
for X being set
for F being Subset of X holds
( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )
proof
let X be set ; ::_thesis: for F being Subset of X holds
( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )
let F be Subset of X; ::_thesis: ( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )
reconsider F9 = F as Element of (BoolePoset X) by Th26;
A1: F c= F ;
thus ( F in the carrier of (CompactSublatt (BoolePoset X)) implies F is finite ) ::_thesis: ( F is finite implies F in the carrier of (CompactSublatt (BoolePoset X)) )
proof
assume A2: F in the carrier of (CompactSublatt (BoolePoset X)) ; ::_thesis: F is finite
the carrier of (CompactSublatt (BoolePoset X)) c= the carrier of (BoolePoset X) by YELLOW_0:def_13;
then reconsider F9 = F as Element of (BoolePoset X) by A2;
( F9 <= F9 & F9 is compact ) by A2, Def1;
then F9 in compactbelow F9 ;
then F9 in { y where y is finite Subset of F9 : verum } by Th29;
then ex F1 being finite Subset of F9 st F1 = F9 ;
hence F is finite ; ::_thesis: verum
end;
assume F is finite ; ::_thesis: F in the carrier of (CompactSublatt (BoolePoset X))
then F in { y where y is finite Subset of F9 : verum } by A1;
then F9 in compactbelow F9 by Th29;
then F9 is compact by Th4;
hence F in the carrier of (CompactSublatt (BoolePoset X)) by Def1; ::_thesis: verum
end;
registration
let X be set ;
let x be Element of (BoolePoset X);
cluster compactbelow x -> directed lower ;
coherence
( compactbelow x is lower & compactbelow x is directed )
proof
now__::_thesis:_for_a,_b_being_set_st_a_c=_b_&_b_in_compactbelow_x_holds_
a_in_compactbelow_x
let a, b be set ; ::_thesis: ( a c= b & b in compactbelow x implies a in compactbelow x )
assume that
A1: a c= b and
A2: b in compactbelow x ; ::_thesis: a in compactbelow x
b in { y where y is finite Subset of x : verum } by A2, Th29;
then ex b1 being finite Subset of x st b = b1 ;
then a is finite Subset of x by A1, XBOOLE_1:1;
then a in { y where y is finite Subset of x : verum } ;
hence a in compactbelow x by Th29; ::_thesis: verum
end;
hence A3: compactbelow x is lower by WAYBEL_7:6; ::_thesis: compactbelow x is directed
now__::_thesis:_for_a,_b_being_set_st_a_in_compactbelow_x_&_b_in_compactbelow_x_holds_
a_\/_b_in_compactbelow_x
let a, b be set ; ::_thesis: ( a in compactbelow x & b in compactbelow x implies a \/ b in compactbelow x )
assume that
A4: a in compactbelow x and
A5: b in compactbelow x ; ::_thesis: a \/ b in compactbelow x
b in { y where y is finite Subset of x : verum } by A5, Th29;
then A6: ex b1 being finite Subset of x st b = b1 ;
a in { y where y is finite Subset of x : verum } by A4, Th29;
then ex a1 being finite Subset of x st a = a1 ;
then a \/ b is finite Subset of x by A6, XBOOLE_1:8;
then a \/ b in { y where y is finite Subset of x : verum } ;
hence a \/ b in compactbelow x by Th29; ::_thesis: verum
end;
hence compactbelow x is directed by A3, WAYBEL_7:8; ::_thesis: verum
end;
end;
theorem Th31: :: WAYBEL_8:31
for X being set holds BoolePoset X is algebraic
proof
let X be set ; ::_thesis: BoolePoset X is algebraic
now__::_thesis:_for_x_being_Element_of_(BoolePoset_X)_holds_x_=_sup_(compactbelow_x)
let x be Element of (BoolePoset X); ::_thesis: x = sup (compactbelow x)
A1: now__::_thesis:_for_a_being_Element_of_(BoolePoset_X)_st_a_is_>=_than_compactbelow_x_holds_
x_<=_a
let a be Element of (BoolePoset X); ::_thesis: ( a is_>=_than compactbelow x implies x <= a )
assume A2: a is_>=_than compactbelow x ; ::_thesis: x <= a
now__::_thesis:_for_t_being_set_st_t_in_x_holds_
t_in_a
let t be set ; ::_thesis: ( t in x implies t in a )
assume A3: t in x ; ::_thesis: t in a
A4: x c= X by Th26;
now__::_thesis:_for_k_being_set_st_k_in_{t}_holds_
k_in_X
let k be set ; ::_thesis: ( k in {t} implies k in X )
assume k in {t} ; ::_thesis: k in X
then k = t by TARSKI:def_1;
hence k in X by A3, A4; ::_thesis: verum
end;
then {t} c= X by TARSKI:def_3;
then reconsider t1 = {t} as Element of (BoolePoset X) by Th26;
for k being set st k in {t} holds
k in x by A3, TARSKI:def_1;
then {t} is finite Subset of x by TARSKI:def_3;
then {t} in { y where y is finite Subset of x : verum } ;
then {t} in compactbelow x by Th29;
then t1 <= a by A2, LATTICE3:def_9;
then ( t in {t} & {t} c= a ) by TARSKI:def_1, YELLOW_1:2;
hence t in a ; ::_thesis: verum
end;
then x c= a by TARSKI:def_3;
hence x <= a by YELLOW_1:2; ::_thesis: verum
end;
for b being Element of (BoolePoset X) st b in compactbelow x holds
b <= x by Th4;
then x is_>=_than compactbelow x by LATTICE3:def_9;
hence x = sup (compactbelow x) by A1, YELLOW_0:32; ::_thesis: verum
end;
then ( ( for x being Element of (BoolePoset X) holds
( not compactbelow x is empty & compactbelow x is directed ) ) & BoolePoset X is satisfying_axiom_K ) by Def3;
hence BoolePoset X is algebraic by Def4; ::_thesis: verum
end;
registration
let X be set ;
cluster BoolePoset X -> algebraic ;
coherence
BoolePoset X is algebraic by Th31;
end;