:: WAYBEL31 semantic presentation
begin
scheme :: WAYBEL31:sch 1
UparrowUnion{ F1() -> RelStr , P1[ set ] } :
for S being Subset-Family of F1() st S = { X where X is Subset of F1() : P1[X] } holds
uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] }
proof
let S be Subset-Family of F1(); ::_thesis: ( S = { X where X is Subset of F1() : P1[X] } implies uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] } )
assume A1: S = { X where X is Subset of F1() : P1[X] } ; ::_thesis: uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] }
A2: union { (uparrow X) where X is Subset of F1() : P1[X] } c= uparrow (union S)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union { (uparrow X) where X is Subset of F1() : P1[X] } or z in uparrow (union S) )
assume z in union { (uparrow X) where X is Subset of F1() : P1[X] } ; ::_thesis: z in uparrow (union S)
then consider Z being set such that
A3: z in Z and
A4: Z in { (uparrow X) where X is Subset of F1() : P1[X] } by TARSKI:def_4;
consider X1 being Subset of F1() such that
A5: Z = uparrow X1 and
A6: P1[X1] by A4;
reconsider z1 = z as Element of F1() by A3, A5;
consider y1 being Element of F1() such that
A7: y1 <= z1 and
A8: y1 in X1 by A3, A5, WAYBEL_0:def_16;
X1 in S by A1, A6;
then y1 in union S by A8, TARSKI:def_4;
hence z in uparrow (union S) by A7, WAYBEL_0:def_16; ::_thesis: verum
end;
uparrow (union S) c= union { (uparrow X) where X is Subset of F1() : P1[X] }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in uparrow (union S) or z in union { (uparrow X) where X is Subset of F1() : P1[X] } )
assume A9: z in uparrow (union S) ; ::_thesis: z in union { (uparrow X) where X is Subset of F1() : P1[X] }
then reconsider z1 = z as Element of F1() ;
consider y1 being Element of F1() such that
A10: y1 <= z1 and
A11: y1 in union S by A9, WAYBEL_0:def_16;
consider Z being set such that
A12: y1 in Z and
A13: Z in S by A11, TARSKI:def_4;
consider X1 being Subset of F1() such that
A14: Z = X1 and
A15: P1[X1] by A1, A13;
A16: uparrow X1 in { (uparrow X) where X is Subset of F1() : P1[X] } by A15;
z in uparrow X1 by A10, A12, A14, WAYBEL_0:def_16;
hence z in union { (uparrow X) where X is Subset of F1() : P1[X] } by A16, TARSKI:def_4; ::_thesis: verum
end;
hence uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] } by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
scheme :: WAYBEL31:sch 2
DownarrowUnion{ F1() -> RelStr , P1[ set ] } :
for S being Subset-Family of F1() st S = { X where X is Subset of F1() : P1[X] } holds
downarrow (union S) = union { (downarrow X) where X is Subset of F1() : P1[X] }
proof
let S be Subset-Family of F1(); ::_thesis: ( S = { X where X is Subset of F1() : P1[X] } implies downarrow (union S) = union { (downarrow X) where X is Subset of F1() : P1[X] } )
assume A1: S = { X where X is Subset of F1() : P1[X] } ; ::_thesis: downarrow (union S) = union { (downarrow X) where X is Subset of F1() : P1[X] }
A2: union { (downarrow X) where X is Subset of F1() : P1[X] } c= downarrow (union S)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union { (downarrow X) where X is Subset of F1() : P1[X] } or z in downarrow (union S) )
assume z in union { (downarrow X) where X is Subset of F1() : P1[X] } ; ::_thesis: z in downarrow (union S)
then consider Z being set such that
A3: z in Z and
A4: Z in { (downarrow X) where X is Subset of F1() : P1[X] } by TARSKI:def_4;
consider X1 being Subset of F1() such that
A5: Z = downarrow X1 and
A6: P1[X1] by A4;
reconsider z1 = z as Element of F1() by A3, A5;
consider y1 being Element of F1() such that
A7: y1 >= z1 and
A8: y1 in X1 by A3, A5, WAYBEL_0:def_15;
X1 in S by A1, A6;
then y1 in union S by A8, TARSKI:def_4;
hence z in downarrow (union S) by A7, WAYBEL_0:def_15; ::_thesis: verum
end;
downarrow (union S) c= union { (downarrow X) where X is Subset of F1() : P1[X] }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in downarrow (union S) or z in union { (downarrow X) where X is Subset of F1() : P1[X] } )
assume A9: z in downarrow (union S) ; ::_thesis: z in union { (downarrow X) where X is Subset of F1() : P1[X] }
then reconsider z1 = z as Element of F1() ;
consider y1 being Element of F1() such that
A10: y1 >= z1 and
A11: y1 in union S by A9, WAYBEL_0:def_15;
consider Z being set such that
A12: y1 in Z and
A13: Z in S by A11, TARSKI:def_4;
consider X1 being Subset of F1() such that
A14: Z = X1 and
A15: P1[X1] by A1, A13;
A16: downarrow X1 in { (downarrow X) where X is Subset of F1() : P1[X] } by A15;
z in downarrow X1 by A10, A12, A14, WAYBEL_0:def_15;
hence z in union { (downarrow X) where X is Subset of F1() : P1[X] } by A16, TARSKI:def_4; ::_thesis: verum
end;
hence downarrow (union S) = union { (downarrow X) where X is Subset of F1() : P1[X] } by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
registration
let L1 be lower-bounded continuous sup-Semilattice;
let B1 be with_bottom CLbasis of L1;
cluster InclPoset (Ids (subrelstr B1)) -> algebraic ;
coherence
InclPoset (Ids (subrelstr B1)) is algebraic by WAYBEL13:10;
end;
definition
let L1 be continuous sup-Semilattice;
func CLweight L1 -> Cardinal equals :: WAYBEL31:def 1
meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
coherence
meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } is Cardinal
proof
set X = { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ;
defpred S1[ Ordinal] means $1 in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
A1: ex A being Ordinal st S1[A]
proof
take card ([#] L1) ; ::_thesis: S1[ card ([#] L1)]
[#] L1 is CLbasis of L1 by YELLOW15:25;
hence S1[ card ([#] L1)] ; ::_thesis: verum
end;
consider A being Ordinal such that
A2: S1[A] and
A3: for C being Ordinal st S1[C] holds
A c= C from ORDINAL1:sch_1(A1);
ex B1 being with_bottom CLbasis of L1 st A = card B1 by A2;
then reconsider A = A as Cardinal ;
A4: now__::_thesis:_for_x_being_set_holds_
(_(_(_for_y_being_set_st_y_in__{__(card_B2)_where_B2_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_
x_in_y_)_implies_x_in_A_)_&_(_x_in_A_implies_for_y_being_set_st_y_in__{__(card_B2)_where_B2_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_
x_in_y_)_)
let x be set ; ::_thesis: ( ( ( for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y ) implies x in A ) & ( x in A implies for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y ) )
thus ( ( for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y ) implies x in A ) by A2; ::_thesis: ( x in A implies for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y )
assume A5: x in A ; ::_thesis: for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y
let y be set ; ::_thesis: ( y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } implies x in y )
assume A6: y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ; ::_thesis: x in y
then ex B2 being with_bottom CLbasis of L1 st y = card B2 ;
then reconsider y1 = y as Cardinal ;
A c= y1 by A3, A6;
hence x in y by A5; ::_thesis: verum
end;
[#] L1 is CLbasis of L1 by YELLOW15:25;
then card ([#] L1) in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ;
hence meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } is Cardinal by A4, SETFAM_1:def_1; ::_thesis: verum
end;
end;
:: deftheorem defines CLweight WAYBEL31:def_1_:_
for L1 being continuous sup-Semilattice holds CLweight L1 = meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
theorem Th1: :: WAYBEL31:1
for L1 being continuous sup-Semilattice
for B1 being with_bottom CLbasis of L1 holds CLweight L1 c= card B1
proof
let L1 be continuous sup-Semilattice; ::_thesis: for B1 being with_bottom CLbasis of L1 holds CLweight L1 c= card B1
let B1 be with_bottom CLbasis of L1; ::_thesis: CLweight L1 c= card B1
card B1 in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ;
hence CLweight L1 c= card B1 by SETFAM_1:3; ::_thesis: verum
end;
theorem Th2: :: WAYBEL31:2
for L1 being continuous sup-Semilattice ex B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1
proof
let L1 be continuous sup-Semilattice; ::_thesis: ex B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1
defpred S1[ Ordinal] means $1 in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
set X = { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ;
A1: ex A being Ordinal st S1[A]
proof
take card ([#] L1) ; ::_thesis: S1[ card ([#] L1)]
[#] L1 is CLbasis of L1 by YELLOW15:25;
hence S1[ card ([#] L1)] ; ::_thesis: verum
end;
consider A being Ordinal such that
A2: S1[A] and
A3: for C being Ordinal st S1[C] holds
A c= C from ORDINAL1:sch_1(A1);
consider B1 being with_bottom CLbasis of L1 such that
A4: A = card B1 by A2;
A5: now__::_thesis:_for_x_being_set_holds_
(_(_(_for_y_being_set_st_y_in__{__(card_B2)_where_B2_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_
x_in_y_)_implies_x_in_A_)_&_(_x_in_A_implies_for_y_being_set_st_y_in__{__(card_B2)_where_B2_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_
x_in_y_)_)
let x be set ; ::_thesis: ( ( ( for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y ) implies x in A ) & ( x in A implies for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y ) )
thus ( ( for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y ) implies x in A ) by A2; ::_thesis: ( x in A implies for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y )
assume A6: x in A ; ::_thesis: for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y
let y be set ; ::_thesis: ( y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } implies x in y )
assume A7: y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ; ::_thesis: x in y
then ex B2 being with_bottom CLbasis of L1 st y = card B2 ;
then reconsider y1 = y as Cardinal ;
A c= y1 by A3, A7;
hence x in y by A6; ::_thesis: verum
end;
take B1 ; ::_thesis: card B1 = CLweight L1
[#] L1 is CLbasis of L1 by YELLOW15:25;
then card ([#] L1) in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ;
hence card B1 = CLweight L1 by A4, A5, SETFAM_1:def_1; ::_thesis: verum
end;
theorem Th3: :: WAYBEL31:3
for L1 being lower-bounded algebraic LATTICE holds CLweight L1 = card the carrier of (CompactSublatt L1)
proof
let L1 be lower-bounded algebraic LATTICE; ::_thesis: CLweight L1 = card the carrier of (CompactSublatt L1)
set CB = { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
the carrier of (CompactSublatt L1) is with_bottom CLbasis of L1 by WAYBEL23:71;
then A1: card the carrier of (CompactSublatt L1) in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
then A2: meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } c= card the carrier of (CompactSublatt L1) by SETFAM_1:3;
now__::_thesis:_for_X_being_set_st_X_in__{__(card_B1)_where_B1_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_
card_the_carrier_of_(CompactSublatt_L1)_c=_X
let X be set ; ::_thesis: ( X in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } implies card the carrier of (CompactSublatt L1) c= X )
assume X in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; ::_thesis: card the carrier of (CompactSublatt L1) c= X
then consider B1 being with_bottom CLbasis of L1 such that
A3: X = card B1 ;
the carrier of (CompactSublatt L1) c= B1 by WAYBEL23:71;
hence card the carrier of (CompactSublatt L1) c= X by A3, CARD_1:11; ::_thesis: verum
end;
then card the carrier of (CompactSublatt L1) c= meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } by A1, SETFAM_1:5;
hence CLweight L1 = card the carrier of (CompactSublatt L1) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th4: :: WAYBEL31:4
for T being non empty TopSpace
for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds
for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T
proof
let T be non empty TopSpace; ::_thesis: for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds
for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T
let L1 be continuous sup-Semilattice; ::_thesis: ( InclPoset the topology of T = L1 implies for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T )
assume A1: InclPoset the topology of T = L1 ; ::_thesis: for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T
let B1 be with_bottom CLbasis of L1; ::_thesis: B1 is Basis of T
B1 c= the carrier of L1 ;
then B1 c= the topology of T by A1, YELLOW_1:1;
then reconsider B2 = B1 as Subset-Family of T by XBOOLE_1:1;
A2: for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B2 & p in a & a c= A )
proof
let A be Subset of T; ::_thesis: ( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in B2 & p in a & a c= A ) )
assume A is open ; ::_thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in B2 & p in a & a c= A )
then A in the topology of T by PRE_TOPC:def_2;
then reconsider A1 = A as Element of L1 by A1, YELLOW_1:1;
let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st
( a in B2 & p in a & a c= A ) )
assume A3: p in A ; ::_thesis: ex a being Subset of T st
( a in B2 & p in a & a c= A )
A1 = sup ((waybelow A1) /\ B1) by WAYBEL23:def_7
.= union ((waybelow A1) /\ B1) by A1, YELLOW_1:22 ;
then consider a being set such that
A4: p in a and
A5: a in (waybelow A1) /\ B1 by A3, TARSKI:def_4;
a in the carrier of L1 by A5;
then a in the topology of T by A1, YELLOW_1:1;
then reconsider a = a as Subset of T ;
take a ; ::_thesis: ( a in B2 & p in a & a c= A )
thus a in B2 by A5, XBOOLE_0:def_4; ::_thesis: ( p in a & a c= A )
thus p in a by A4; ::_thesis: a c= A
reconsider a1 = a as Element of L1 by A5;
a1 in waybelow A1 by A5, XBOOLE_0:def_4;
then a1 << A1 by WAYBEL_3:7;
then a1 <= A1 by WAYBEL_3:1;
hence a c= A by A1, YELLOW_1:3; ::_thesis: verum
end;
B2 c= the topology of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B2 or x in the topology of T )
assume x in B2 ; ::_thesis: x in the topology of T
then reconsider x1 = x as Element of L1 ;
x1 in the carrier of L1 ;
hence x in the topology of T by A1, YELLOW_1:1; ::_thesis: verum
end;
hence B1 is Basis of T by A2, YELLOW_9:32; ::_thesis: verum
end;
theorem Th5: :: WAYBEL31:5
for T being non empty TopSpace
for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 holds
for B1 being Basis of T
for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
proof
let T be non empty TopSpace; ::_thesis: for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 holds
for B1 being Basis of T
for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
let L1 be lower-bounded continuous LATTICE; ::_thesis: ( InclPoset the topology of T = L1 implies for B1 being Basis of T
for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1 )
assume A1: InclPoset the topology of T = L1 ; ::_thesis: for B1 being Basis of T
for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
let B1 be Basis of T; ::_thesis: for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
let B2 be Subset of L1; ::_thesis: ( B1 = B2 implies finsups B2 is with_bottom CLbasis of L1 )
assume A2: B1 = B2 ; ::_thesis: finsups B2 is with_bottom CLbasis of L1
A3: for x, y being Element of L1 st not y <= x holds
ex b being Element of L1 st
( b in finsups B2 & not b <= x & b <= y )
proof
let x, y be Element of L1; ::_thesis: ( not y <= x implies ex b being Element of L1 st
( b in finsups B2 & not b <= x & b <= y ) )
y in the carrier of L1 ;
then A4: y in the topology of T by A1, YELLOW_1:1;
then reconsider y1 = y as Subset of T ;
assume not y <= x ; ::_thesis: ex b being Element of L1 st
( b in finsups B2 & not b <= x & b <= y )
then not y c= x by A1, YELLOW_1:3;
then consider v being set such that
A5: v in y and
A6: not v in x by TARSKI:def_3;
v in y1 by A5;
then reconsider v = v as Point of T ;
y1 is open by A4, PRE_TOPC:def_2;
then consider b being Subset of T such that
A7: b in B1 and
A8: v in b and
A9: b c= y1 by A5, YELLOW_9:31;
reconsider b = b as Element of L1 by A2, A7;
for z being set st z in {b} holds
z in B2 by A2, A7, TARSKI:def_1;
then A10: {b} is finite Subset of B2 by TARSKI:def_3;
take b ; ::_thesis: ( b in finsups B2 & not b <= x & b <= y )
( ex_sup_of {b},L1 & b = "\/" ({b},L1) ) by YELLOW_0:38, YELLOW_0:39;
then b in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } by A10;
hence b in finsups B2 by WAYBEL_0:def_27; ::_thesis: ( not b <= x & b <= y )
not b c= x by A6, A8;
hence not b <= x by A1, YELLOW_1:3; ::_thesis: b <= y
thus b <= y by A1, A9, YELLOW_1:3; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Element_of_L1_st_x_in_finsups_B2_&_y_in_finsups_B2_holds_
sup_{x,y}_in_finsups_B2
let x, y be Element of L1; ::_thesis: ( x in finsups B2 & y in finsups B2 implies sup {x,y} in finsups B2 )
assume that
A11: x in finsups B2 and
A12: y in finsups B2 ; ::_thesis: sup {x,y} in finsups B2
y in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } by A12, WAYBEL_0:def_27;
then consider Y2 being finite Subset of B2 such that
A13: y = "\/" (Y2,L1) and
A14: ex_sup_of Y2,L1 ;
x in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } by A11, WAYBEL_0:def_27;
then consider Y1 being finite Subset of B2 such that
A15: x = "\/" (Y1,L1) and
A16: ex_sup_of Y1,L1 ;
( ex_sup_of Y1 \/ Y2,L1 & "\/" ((Y1 \/ Y2),L1) = ("\/" (Y1,L1)) "\/" ("\/" (Y2,L1)) ) by A16, A14, YELLOW_2:3;
then x "\/" y in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } by A15, A13;
then x "\/" y in finsups B2 by WAYBEL_0:def_27;
hence sup {x,y} in finsups B2 by YELLOW_0:41; ::_thesis: verum
end;
then A17: finsups B2 is join-closed by WAYBEL23:18;
( {} c= B2 & ex_sup_of {} ,L1 ) by XBOOLE_1:2, YELLOW_0:42;
then "\/" ({},L1) in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } ;
then Bottom L1 in finsups B2 by WAYBEL_0:def_27;
hence finsups B2 is with_bottom CLbasis of L1 by A17, A3, WAYBEL23:49, WAYBEL23:def_8; ::_thesis: verum
end;
theorem Th6: :: WAYBEL31:6
for T being non empty T_0 TopSpace
for L1 being lower-bounded continuous sup-Semilattice st InclPoset the topology of T = L1 & T is infinite holds
weight T = CLweight L1
proof
let T be non empty T_0 TopSpace; ::_thesis: for L1 being lower-bounded continuous sup-Semilattice st InclPoset the topology of T = L1 & T is infinite holds
weight T = CLweight L1
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: ( InclPoset the topology of T = L1 & T is infinite implies weight T = CLweight L1 )
assume that
A1: InclPoset the topology of T = L1 and
A2: T is infinite ; ::_thesis: weight T = CLweight L1
A3: { (card B1) where B1 is Basis of T : verum } c= { (card B1) where B1 is with_bottom CLbasis of L1 : verum }
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (card B1) where B1 is Basis of T : verum } or b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } )
assume b in { (card B1) where B1 is Basis of T : verum } ; ::_thesis: b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum }
then consider B2 being Basis of T such that
A4: b = card B2 ;
B2 c= the topology of T by TOPS_2:64;
then reconsider B3 = B2 as Subset of L1 by A1, YELLOW_1:1;
B2 is infinite by A2, YELLOW15:30;
then A5: card B2 = card (finsups B3) by YELLOW15:27;
finsups B3 is with_bottom CLbasis of L1 by A1, Th5;
hence b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } by A4, A5; ::_thesis: verum
end;
{ (card B1) where B1 is with_bottom CLbasis of L1 : verum } c= { (card B1) where B1 is Basis of T : verum }
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } or b in { (card B1) where B1 is Basis of T : verum } )
assume b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; ::_thesis: b in { (card B1) where B1 is Basis of T : verum }
then consider B2 being with_bottom CLbasis of L1 such that
A6: b = card B2 ;
B2 is Basis of T by A1, Th4;
hence b in { (card B1) where B1 is Basis of T : verum } by A6; ::_thesis: verum
end;
then { (card B1) where B1 is Basis of T : verum } = { (card B1) where B1 is with_bottom CLbasis of L1 : verum } by A3, XBOOLE_0:def_10;
hence weight T = CLweight L1 by WAYBEL23:def_5; ::_thesis: verum
end;
theorem Th7: :: WAYBEL31:7
for T being non empty T_0 TopSpace
for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds
card the carrier of T c= card the carrier of L1
proof
let T be non empty T_0 TopSpace; ::_thesis: for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds
card the carrier of T c= card the carrier of L1
let L1 be continuous sup-Semilattice; ::_thesis: ( InclPoset the topology of T = L1 implies card the carrier of T c= card the carrier of L1 )
A1: card the carrier of T c= card the topology of T by YELLOW15:28;
assume InclPoset the topology of T = L1 ; ::_thesis: card the carrier of T c= card the carrier of L1
hence card the carrier of T c= card the carrier of L1 by A1, YELLOW_1:1; ::_thesis: verum
end;
theorem Th8: :: WAYBEL31:8
for T being non empty T_0 TopSpace st T is finite holds
weight T = card the carrier of T
proof
let T be non empty T_0 TopSpace; ::_thesis: ( T is finite implies weight T = card the carrier of T )
deffunc H1( set ) -> set = meet { A where A is Element of the topology of T : $1 in A } ;
A1: for x being set st x in the carrier of T holds
H1(x) in the carrier of (BoolePoset the carrier of T)
proof
let x be set ; ::_thesis: ( x in the carrier of T implies H1(x) in the carrier of (BoolePoset the carrier of T) )
assume A2: x in the carrier of T ; ::_thesis: H1(x) in the carrier of (BoolePoset the carrier of T)
the carrier of T in the topology of T by PRE_TOPC:def_1;
then the carrier of T in { A where A is Element of the topology of T : x in A } by A2;
then meet { A where A is Element of the topology of T : x in A } c= the carrier of T by SETFAM_1:3;
then meet { A where A is Element of the topology of T : x in A } in bool the carrier of T ;
hence H1(x) in the carrier of (BoolePoset the carrier of T) by WAYBEL_7:2; ::_thesis: verum
end;
consider f being Function of the carrier of T, the carrier of (BoolePoset the carrier of T) such that
A3: for x being set st x in the carrier of T holds
f . x = H1(x) from FUNCT_2:sch_2(A1);
reconsider rf = rng f as Subset-Family of T by WAYBEL_7:2;
A4: for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in rf & p in a & a c= A )
proof
let A be Subset of T; ::_thesis: ( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in rf & p in a & a c= A ) )
assume A is open ; ::_thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in rf & p in a & a c= A )
then A5: A in the topology of T by PRE_TOPC:def_2;
let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st
( a in rf & p in a & a c= A ) )
assume p in A ; ::_thesis: ex a being Subset of T st
( a in rf & p in a & a c= A )
then A6: A in { C where C is Element of the topology of T : p in C } by A5;
meet { C where C is Element of the topology of T : p in C } c= the carrier of T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet { C where C is Element of the topology of T : p in C } or z in the carrier of T )
assume z in meet { C where C is Element of the topology of T : p in C } ; ::_thesis: z in the carrier of T
then z in A by A6, SETFAM_1:def_1;
hence z in the carrier of T ; ::_thesis: verum
end;
then reconsider a = meet { C where C is Element of the topology of T : p in C } as Subset of T ;
take a ; ::_thesis: ( a in rf & p in a & a c= A )
p in the carrier of T ;
then A7: p in dom f by FUNCT_2:def_1;
a = f . p by A3;
hence a in rf by A7, FUNCT_1:def_3; ::_thesis: ( p in a & a c= A )
now__::_thesis:_for_Y_being_set_st_Y_in__{__C_where_C_is_Element_of_the_topology_of_T_:_p_in_C__}__holds_
p_in_Y
let Y be set ; ::_thesis: ( Y in { C where C is Element of the topology of T : p in C } implies p in Y )
assume Y in { C where C is Element of the topology of T : p in C } ; ::_thesis: p in Y
then ex C being Element of the topology of T st
( Y = C & p in C ) ;
hence p in Y ; ::_thesis: verum
end;
hence p in a by A6, SETFAM_1:def_1; ::_thesis: a c= A
thus a c= A ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in a or z in A )
assume z in a ; ::_thesis: z in A
hence z in A by A6, SETFAM_1:def_1; ::_thesis: verum
end;
end;
assume A8: T is finite ; ::_thesis: weight T = card the carrier of T
rf c= the topology of T
proof
reconsider tT = the topology of T as non empty finite set by A8;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rf or z in the topology of T )
deffunc H2( set ) -> set = $1;
assume z in rf ; ::_thesis: z in the topology of T
then consider y being set such that
A9: ( y in dom f & z = f . y ) by FUNCT_1:def_3;
{ A where A is Element of the topology of T : y in A } c= bool the carrier of T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { A where A is Element of the topology of T : y in A } or z in bool the carrier of T )
assume z in { A where A is Element of the topology of T : y in A } ; ::_thesis: z in bool the carrier of T
then ex A being Element of the topology of T st
( z = A & y in A ) ;
hence z in bool the carrier of T ; ::_thesis: verum
end;
then reconsider sfA = { A where A is Element of the topology of T : y in A } as Subset-Family of T ;
defpred S1[ set ] means y in $1;
reconsider sfA = sfA as Subset-Family of T ;
now__::_thesis:_for_P_being_Subset_of_T_st_P_in_sfA_holds_
P_is_open
let P be Subset of T; ::_thesis: ( P in sfA implies P is open )
assume P in sfA ; ::_thesis: P is open
then ex A being Element of the topology of T st
( P = A & y in A ) ;
hence P is open by PRE_TOPC:def_2; ::_thesis: verum
end;
then A10: sfA is open by TOPS_2:def_1;
{ H2(A) where A is Element of tT : S1[A] } is finite from PRE_CIRC:sch_1();
then A11: meet sfA is open by A10, TOPS_2:20;
z = meet { A where A is Element of the topology of T : y in A } by A3, A9;
hence z in the topology of T by A11, PRE_TOPC:def_2; ::_thesis: verum
end;
then rng f is Basis of T by A4, YELLOW_9:32;
then A12: card (rng f) in { (card B1) where B1 is Basis of T : verum } ;
then A13: meet { (card B1) where B1 is Basis of T : verum } c= card (rng f) by SETFAM_1:3;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_
not_x1_<>_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies not x1 <> x2 )
assume that
A14: ( x1 in dom f & x2 in dom f ) and
A15: f . x1 = f . x2 ; ::_thesis: not x1 <> x2
reconsider x3 = x1, x4 = x2 as Point of T by A14;
assume x1 <> x2 ; ::_thesis: contradiction
then consider V being Subset of T such that
A16: V is open and
A17: ( ( x3 in V & not x4 in V ) or ( x4 in V & not x3 in V ) ) by T_0TOPSP:def_7;
A18: ( f . x3 = meet { A where A is Element of the topology of T : x3 in A } & f . x4 = meet { A where A is Element of the topology of T : x4 in A } ) by A3;
now__::_thesis:_contradiction
percases ( ( x3 in V & not x4 in V ) or ( x4 in V & not x3 in V ) ) by A17;
supposeA19: ( x3 in V & not x4 in V ) ; ::_thesis: contradiction
V in the topology of T by A16, PRE_TOPC:def_2;
then A20: V in { A where A is Element of the topology of T : x3 in A } by A19;
A21: meet { A where A is Element of the topology of T : x3 in A } c= V
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet { A where A is Element of the topology of T : x3 in A } or z in V )
assume z in meet { A where A is Element of the topology of T : x3 in A } ; ::_thesis: z in V
hence z in V by A20, SETFAM_1:def_1; ::_thesis: verum
end;
A22: now__::_thesis:_for_Y_being_set_st_Y_in__{__A_where_A_is_Element_of_the_topology_of_T_:_x4_in_A__}__holds_
x4_in_Y
let Y be set ; ::_thesis: ( Y in { A where A is Element of the topology of T : x4 in A } implies x4 in Y )
assume Y in { A where A is Element of the topology of T : x4 in A } ; ::_thesis: x4 in Y
then ex A being Element of the topology of T st
( Y = A & x4 in A ) ;
hence x4 in Y ; ::_thesis: verum
end;
the carrier of T in the topology of T by PRE_TOPC:def_1;
then the carrier of T in { A where A is Element of the topology of T : x4 in A } ;
then x4 in meet { A where A is Element of the topology of T : x3 in A } by A15, A18, A22, SETFAM_1:def_1;
hence contradiction by A19, A21; ::_thesis: verum
end;
supposeA23: ( x4 in V & not x3 in V ) ; ::_thesis: contradiction
V in the topology of T by A16, PRE_TOPC:def_2;
then A24: V in { A where A is Element of the topology of T : x4 in A } by A23;
A25: meet { A where A is Element of the topology of T : x4 in A } c= V
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet { A where A is Element of the topology of T : x4 in A } or z in V )
assume z in meet { A where A is Element of the topology of T : x4 in A } ; ::_thesis: z in V
hence z in V by A24, SETFAM_1:def_1; ::_thesis: verum
end;
A26: now__::_thesis:_for_Y_being_set_st_Y_in__{__A_where_A_is_Element_of_the_topology_of_T_:_x3_in_A__}__holds_
x3_in_Y
let Y be set ; ::_thesis: ( Y in { A where A is Element of the topology of T : x3 in A } implies x3 in Y )
assume Y in { A where A is Element of the topology of T : x3 in A } ; ::_thesis: x3 in Y
then ex A being Element of the topology of T st
( Y = A & x3 in A ) ;
hence x3 in Y ; ::_thesis: verum
end;
the carrier of T in the topology of T by PRE_TOPC:def_1;
then the carrier of T in { A where A is Element of the topology of T : x3 in A } ;
then x3 in meet { A where A is Element of the topology of T : x4 in A } by A15, A18, A26, SETFAM_1:def_1;
hence contradiction by A23, A25; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
then ( dom f = the carrier of T & f is V13() ) by FUNCT_1:def_4, FUNCT_2:def_1;
then A27: the carrier of T, rng f are_equipotent by WELLORD2:def_4;
for X being set st X in { (card B1) where B1 is Basis of T : verum } holds
card (rng f) c= X
proof
let X be set ; ::_thesis: ( X in { (card B1) where B1 is Basis of T : verum } implies card (rng f) c= X )
assume X in { (card B1) where B1 is Basis of T : verum } ; ::_thesis: card (rng f) c= X
then consider B2 being Basis of T such that
A28: X = card B2 ;
rng f c= B2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in B2 )
assume y in rng f ; ::_thesis: y in B2
then consider x being set such that
A29: x in dom f and
A30: y = f . x by FUNCT_1:def_3;
reconsider x1 = x as Element of T by A29;
y = meet { A where A is Element of the topology of T : x1 in A } by A3, A30;
hence y in B2 by A8, YELLOW15:31; ::_thesis: verum
end;
hence card (rng f) c= X by A28, CARD_1:11; ::_thesis: verum
end;
then card (rng f) c= meet { (card B1) where B1 is Basis of T : verum } by A12, SETFAM_1:5;
then card (rng f) = meet { (card B1) where B1 is Basis of T : verum } by A13, XBOOLE_0:def_10
.= weight T by WAYBEL23:def_5 ;
hence weight T = card the carrier of T by A27, CARD_1:5; ::_thesis: verum
end;
theorem Th9: :: WAYBEL31:9
for T being TopStruct
for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 & T is finite holds
CLweight L1 = card the carrier of L1
proof
let T be TopStruct ; ::_thesis: for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 & T is finite holds
CLweight L1 = card the carrier of L1
let L1 be lower-bounded continuous LATTICE; ::_thesis: ( InclPoset the topology of T = L1 & T is finite implies CLweight L1 = card the carrier of L1 )
assume A1: InclPoset the topology of T = L1 ; ::_thesis: ( not T is finite or CLweight L1 = card the carrier of L1 )
[#] L1 is with_bottom CLbasis of L1 by YELLOW15:25;
then A2: card the carrier of L1 in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
A3: CLweight L1 c= card the carrier of L1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in CLweight L1 or z in card the carrier of L1 )
assume z in CLweight L1 ; ::_thesis: z in card the carrier of L1
hence z in card the carrier of L1 by A2, SETFAM_1:def_1; ::_thesis: verum
end;
assume A4: T is finite ; ::_thesis: CLweight L1 = card the carrier of L1
now__::_thesis:_for_Z_being_set_st_Z_in__{__(card_B1)_where_B1_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_
card_the_carrier_of_L1_c=_Z
let Z be set ; ::_thesis: ( Z in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } implies card the carrier of L1 c= Z )
assume Z in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; ::_thesis: card the carrier of L1 c= Z
then consider B1 being with_bottom CLbasis of L1 such that
A5: Z = card B1 ;
Bottom L1 in B1 by WAYBEL23:def_8;
then the carrier of (CompactSublatt L1) c= B1 by WAYBEL23:48;
then A6: card the carrier of (CompactSublatt L1) c= card B1 by CARD_1:11;
L1 is finite by A1, A4, YELLOW_1:1;
hence card the carrier of L1 c= Z by A5, A6, YELLOW15:26; ::_thesis: verum
end;
then card the carrier of L1 c= meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } by A2, SETFAM_1:5;
hence CLweight L1 = card the carrier of L1 by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th10: :: WAYBEL31:10
for L1 being lower-bounded continuous sup-Semilattice
for T1 being Scott TopAugmentation of L1
for T2 being correct Lawson TopAugmentation of L1
for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T1 being Scott TopAugmentation of L1
for T2 being correct Lawson TopAugmentation of L1
for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1
let T1 be Scott TopAugmentation of L1; ::_thesis: for T2 being correct Lawson TopAugmentation of L1
for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1
let T2 be correct Lawson TopAugmentation of L1; ::_thesis: for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1
let B2 be Basis of T2; ::_thesis: { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1
A1: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of L1, the InternalRel of L1 #) & RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of L1, the InternalRel of L1 #) ) by YELLOW_9:def_4;
{ (uparrow V) where V is Subset of T2 : V in B2 } c= bool the carrier of T1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (uparrow V) where V is Subset of T2 : V in B2 } or z in bool the carrier of T1 )
assume z in { (uparrow V) where V is Subset of T2 : V in B2 } ; ::_thesis: z in bool the carrier of T1
then ex V being Subset of T2 st
( z = uparrow V & V in B2 ) ;
hence z in bool the carrier of T1 by A1; ::_thesis: verum
end;
then reconsider upV = { (uparrow V) where V is Subset of T2 : V in B2 } as Subset-Family of T1 ;
reconsider upV = upV as Subset-Family of T1 ;
A2: the topology of T1 c= UniCl upV
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the topology of T1 or z in UniCl upV )
assume A3: z in the topology of T1 ; ::_thesis: z in UniCl upV
then reconsider z2 = z as Subset of T1 ;
z2 is open by A3, PRE_TOPC:def_2;
then z2 is upper by WAYBEL11:def_4;
then A4: uparrow z2 c= z2 by WAYBEL_0:24;
reconsider z1 = z as Subset of T2 by A1, A3;
z in sigma T1 by A3, WAYBEL14:23;
then ( sigma T2 c= lambda T2 & z in sigma T2 ) by A1, WAYBEL30:10, YELLOW_9:52;
then z in lambda T2 ;
then z in the topology of T2 by WAYBEL30:9;
then A5: z1 is open by PRE_TOPC:def_2;
{ (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } c= bool the carrier of T1
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } or v in bool the carrier of T1 )
assume v in { (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } ; ::_thesis: v in bool the carrier of T1
then ex G being Subset of T2 st
( v = uparrow G & G in B2 & G c= z1 ) ;
hence v in bool the carrier of T1 by A1; ::_thesis: verum
end;
then reconsider Y = { (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } as Subset-Family of T1 ;
{ G where G is Subset of T2 : ( G in B2 & G c= z1 ) } c= bool the carrier of T1
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { G where G is Subset of T2 : ( G in B2 & G c= z1 ) } or v in bool the carrier of T1 )
assume v in { G where G is Subset of T2 : ( G in B2 & G c= z1 ) } ; ::_thesis: v in bool the carrier of T1
then ex G being Subset of T2 st
( v = G & G in B2 & G c= z1 ) ;
hence v in bool the carrier of T1 by A1; ::_thesis: verum
end;
then reconsider Y1 = { G where G is Subset of T2 : ( G in B2 & G c= z1 ) } as Subset-Family of T1 ;
defpred S1[ set ] means ( $1 in B2 & $1 c= z1 );
reconsider Y = Y as Subset-Family of T1 ;
reconsider Y1 = Y1 as Subset-Family of T1 ;
reconsider Y3 = Y1 as Subset-Family of T2 by A1;
A6: Y c= upV
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in Y or v in upV )
assume v in Y ; ::_thesis: v in upV
then ex G being Subset of T2 st
( v = uparrow G & G in B2 & G c= z1 ) ;
hence v in upV ; ::_thesis: verum
end;
A7: for S being Subset-Family of T2 st S = { X where X is Subset of T2 : S1[X] } holds
uparrow (union S) = union { (uparrow X) where X is Subset of T2 : S1[X] } from WAYBEL31:sch_1();
z2 c= uparrow z2 by WAYBEL_0:16;
then z1 = uparrow z2 by A4, XBOOLE_0:def_10
.= uparrow (union Y1) by A5, YELLOW_8:9
.= uparrow (union Y3) by A1, WAYBEL_0:13
.= union Y by A7 ;
hence z in UniCl upV by A6, CANTOR_1:def_1; ::_thesis: verum
end;
upV c= the topology of T1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in upV or z in the topology of T1 )
assume z in upV ; ::_thesis: z in the topology of T1
then consider V being Subset of T2 such that
A8: z = uparrow V and
A9: V in B2 ;
A10: T1 is Scott TopAugmentation of T2 by A1, YELLOW_9:def_4;
B2 c= the topology of T2 by TOPS_2:64;
then V in the topology of T2 by A9;
then V in lambda T2 by WAYBEL30:9;
then uparrow V in sigma T1 by A10, WAYBEL30:14;
hence z in the topology of T1 by A8, WAYBEL14:23; ::_thesis: verum
end;
hence { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1 by A2, CANTOR_1:def_2, TOPS_2:64; ::_thesis: verum
end;
Lm1: for L1 being lower-bounded continuous sup-Semilattice
for T1 being Scott TopAugmentation of L1
for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T1 being Scott TopAugmentation of L1
for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2
let T1 be Scott TopAugmentation of L1; ::_thesis: for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2
let T2 be correct Lawson TopAugmentation of L1; ::_thesis: weight T1 c= weight T2
consider B1 being Basis of T2 such that
A1: card B1 = weight T2 by WAYBEL23:74;
defpred S1[ set , set ] means ex y being Subset of T2 st
( y = $1 & $2 = uparrow y );
A2: for x being set st x in B1 holds
ex z being set st S1[x,z]
proof
let x be set ; ::_thesis: ( x in B1 implies ex z being set st S1[x,z] )
assume x in B1 ; ::_thesis: ex z being set st S1[x,z]
then reconsider y = x as Subset of T2 ;
take uparrow y ; ::_thesis: S1[x, uparrow y]
take y ; ::_thesis: ( y = x & uparrow y = uparrow y )
thus ( y = x & uparrow y = uparrow y ) ; ::_thesis: verum
end;
consider f being Function such that
A3: dom f = B1 and
A4: for x being set st x in B1 holds
S1[x,f . x] from CLASSES1:sch_1(A2);
{ (uparrow V) where V is Subset of T2 : V in B1 } c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (uparrow V) where V is Subset of T2 : V in B1 } or z in rng f )
assume z in { (uparrow V) where V is Subset of T2 : V in B1 } ; ::_thesis: z in rng f
then consider V being Subset of T2 such that
A5: z = uparrow V and
A6: V in B1 ;
ex V1 being Subset of T2 st
( V1 = V & f . V = uparrow V1 ) by A4, A6;
hence z in rng f by A3, A5, A6, FUNCT_1:def_3; ::_thesis: verum
end;
then A7: card { (uparrow V) where V is Subset of T2 : V in B1 } c= card B1 by A3, CARD_1:12;
{ (uparrow V) where V is Subset of T2 : V in B1 } is Basis of T1 by Th10;
then card { (uparrow V) where V is Subset of T2 : V in B1 } in { (card B2) where B2 is Basis of T1 : verum } ;
then meet { (card B2) where B2 is Basis of T1 : verum } c= card { (uparrow V) where V is Subset of T2 : V in B1 } by SETFAM_1:3;
then meet { (card B2) where B2 is Basis of T1 : verum } c= card B1 by A7, XBOOLE_1:1;
hence weight T1 c= weight T2 by A1, WAYBEL23:def_5; ::_thesis: verum
end;
theorem Th11: :: WAYBEL31:11
for L1 being non empty up-complete Poset st L1 is finite holds
for x being Element of L1 holds x in compactbelow x
proof
let L1 be non empty up-complete Poset; ::_thesis: ( L1 is finite implies for x being Element of L1 holds x in compactbelow x )
assume A1: L1 is finite ; ::_thesis: for x being Element of L1 holds x in compactbelow x
let x be Element of L1; ::_thesis: x in compactbelow x
A2: x <= x ;
x is compact by A1, WAYBEL_3:17;
hence x in compactbelow x by A2; ::_thesis: verum
end;
theorem Th12: :: WAYBEL31:12
for L1 being finite LATTICE holds L1 is arithmetic
proof
let L1 be finite LATTICE; ::_thesis: L1 is arithmetic
thus for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ; :: according to WAYBEL_8:def_4,WAYBEL_8:def_5 ::_thesis: ( L1 is up-complete & L1 is satisfying_axiom_K & CompactSublatt L1 is meet-inheriting )
thus L1 is up-complete ; ::_thesis: ( L1 is satisfying_axiom_K & CompactSublatt L1 is meet-inheriting )
thus L1 is satisfying_axiom_K ::_thesis: CompactSublatt L1 is meet-inheriting
proof
let x be Element of L1; :: according to WAYBEL_8:def_3 ::_thesis: x = "\/" ((compactbelow x),L1)
A1: now__::_thesis:_for_y_being_Element_of_L1_st_y_is_>=_than_compactbelow_x_holds_
x_<=_y
let y be Element of L1; ::_thesis: ( y is_>=_than compactbelow x implies x <= y )
assume A2: y is_>=_than compactbelow x ; ::_thesis: x <= y
x in compactbelow x by Th11;
hence x <= y by A2, LATTICE3:def_9; ::_thesis: verum
end;
for y being Element of L1 st y in compactbelow x holds
y <= x by WAYBEL_8:4;
then x is_>=_than compactbelow x by LATTICE3:def_9;
hence x = "\/" ((compactbelow x),L1) by A1, YELLOW_0:30; ::_thesis: verum
end;
thus CompactSublatt L1 is meet-inheriting ::_thesis: verum
proof
let x, y be Element of L1; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of (CompactSublatt L1) or not y in the carrier of (CompactSublatt L1) or not ex_inf_of {x,y},L1 or "/\" ({x,y},L1) in the carrier of (CompactSublatt L1) )
assume that
x in the carrier of (CompactSublatt L1) and
y in the carrier of (CompactSublatt L1) and
ex_inf_of {x,y},L1 ; ::_thesis: "/\" ({x,y},L1) in the carrier of (CompactSublatt L1)
x "/\" y is compact by WAYBEL_3:17;
then x "/\" y in the carrier of (CompactSublatt L1) by WAYBEL_8:def_1;
hence "/\" ({x,y},L1) in the carrier of (CompactSublatt L1) by YELLOW_0:40; ::_thesis: verum
end;
end;
registration
cluster finite reflexive transitive antisymmetric with_suprema with_infima -> arithmetic for RelStr ;
coherence
for b1 being LATTICE st b1 is finite holds
b1 is arithmetic by Th12;
end;
registration
cluster finite 1 -element strict reflexive transitive antisymmetric lower-bounded with_suprema with_infima for RelStr ;
existence
ex b1 being RelStr st
( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_suprema & b1 is with_infima & b1 is lower-bounded & b1 is 1 -element & b1 is finite & b1 is strict )
proof
0 in {0} by TARSKI:def_1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3;
reconsider T = RelStr(# {0},r #) as non empty RelStr ;
take T ; ::_thesis: ( T is reflexive & T is transitive & T is antisymmetric & T is with_suprema & T is with_infima & T is lower-bounded & T is 1 -element & T is finite & T is strict )
thus T is reflexive ::_thesis: ( T is transitive & T is antisymmetric & T is with_suprema & T is with_infima & T is lower-bounded & T is 1 -element & T is finite & T is strict )
proof
let x be Element of T; :: according to YELLOW_0:def_1 ::_thesis: x <= x
x = 0 by TARSKI:def_1;
then [x,x] in {[0,0]} by TARSKI:def_1;
hence x <= x by ORDERS_2:def_5; ::_thesis: verum
end;
then reconsider T9 = T as 1 -element reflexive RelStr ;
reconsider T99 = T9 as LATTICE ;
T9 is transitive ;
hence T is transitive ; ::_thesis: ( T is antisymmetric & T is with_suprema & T is with_infima & T is lower-bounded & T is 1 -element & T is finite & T is strict )
T9 is antisymmetric ;
hence T is antisymmetric ; ::_thesis: ( T is with_suprema & T is with_infima & T is lower-bounded & T is 1 -element & T is finite & T is strict )
T9 is with_suprema ;
hence T is with_suprema ; ::_thesis: ( T is with_infima & T is lower-bounded & T is 1 -element & T is finite & T is strict )
T9 is with_infima ;
hence T is with_infima ; ::_thesis: ( T is lower-bounded & T is 1 -element & T is finite & T is strict )
T99 is lower-bounded ;
hence T is lower-bounded ; ::_thesis: ( T is 1 -element & T is finite & T is strict )
thus T is 1 -element ; ::_thesis: ( T is finite & T is strict )
thus T is finite ; ::_thesis: T is strict
thus T is strict ; ::_thesis: verum
end;
end;
theorem Th13: :: WAYBEL31:13
for L1 being finite LATTICE
for B1 being with_bottom CLbasis of L1 holds
( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) )
proof
let L1 be finite LATTICE; ::_thesis: for B1 being with_bottom CLbasis of L1 holds
( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) )
let B1 be with_bottom CLbasis of L1; ::_thesis: ( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) )
thus ( card B1 = CLweight L1 implies B1 = the carrier of (CompactSublatt L1) ) ::_thesis: ( B1 = the carrier of (CompactSublatt L1) implies card B1 = CLweight L1 )
proof
assume card B1 = CLweight L1 ; ::_thesis: B1 = the carrier of (CompactSublatt L1)
then A1: card the carrier of (CompactSublatt L1) = card B1 by Th3;
the carrier of (CompactSublatt L1) c= B1 by WAYBEL23:71;
hence B1 = the carrier of (CompactSublatt L1) by A1, PRE_POLY:8; ::_thesis: verum
end;
assume B1 = the carrier of (CompactSublatt L1) ; ::_thesis: card B1 = CLweight L1
hence card B1 = CLweight L1 by Th3; ::_thesis: verum
end;
definition
let L1 be non empty reflexive RelStr ;
let A be Subset of L1;
let a be Element of L1;
func Way_Up (a,A) -> Subset of L1 equals :: WAYBEL31:def 2
(wayabove a) \ (uparrow A);
coherence
(wayabove a) \ (uparrow A) is Subset of L1 ;
end;
:: deftheorem defines Way_Up WAYBEL31:def_2_:_
for L1 being non empty reflexive RelStr
for A being Subset of L1
for a being Element of L1 holds Way_Up (a,A) = (wayabove a) \ (uparrow A);
theorem :: WAYBEL31:14
for L1 being non empty reflexive RelStr
for a being Element of L1 holds Way_Up (a,({} L1)) = wayabove a ;
theorem :: WAYBEL31:15
for L1 being non empty Poset
for A being Subset of L1
for a being Element of L1 st a in uparrow A holds
Way_Up (a,A) = {}
proof
let L1 be non empty Poset; ::_thesis: for A being Subset of L1
for a being Element of L1 st a in uparrow A holds
Way_Up (a,A) = {}
let A be Subset of L1; ::_thesis: for a being Element of L1 st a in uparrow A holds
Way_Up (a,A) = {}
let a be Element of L1; ::_thesis: ( a in uparrow A implies Way_Up (a,A) = {} )
assume A1: a in uparrow A ; ::_thesis: Way_Up (a,A) = {}
wayabove a c= uparrow A
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in wayabove a or z in uparrow A )
assume A2: z in wayabove a ; ::_thesis: z in uparrow A
then reconsider z1 = z as Element of L1 ;
a << z1 by A2, WAYBEL_3:8;
then a <= z1 by WAYBEL_3:1;
hence z in uparrow A by A1, WAYBEL_0:def_20; ::_thesis: verum
end;
hence Way_Up (a,A) = {} by XBOOLE_1:37; ::_thesis: verum
end;
theorem Th16: :: WAYBEL31:16
for L1 being non empty finite reflexive transitive RelStr holds Ids L1 is finite
proof
deffunc H1( set ) -> set = $1;
let L1 be non empty finite reflexive transitive RelStr ; ::_thesis: Ids L1 is finite
reconsider Y = bool the carrier of L1 as non empty finite set ;
A1: { X where X is Ideal of L1 : verum } c= { X where X is Element of Y : X is Ideal of L1 }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { X where X is Ideal of L1 : verum } or z in { X where X is Element of Y : X is Ideal of L1 } )
assume z in { X where X is Ideal of L1 : verum } ; ::_thesis: z in { X where X is Element of Y : X is Ideal of L1 }
then ex X1 being Ideal of L1 st z = X1 ;
hence z in { X where X is Element of Y : X is Ideal of L1 } ; ::_thesis: verum
end;
defpred S1[ set ] means $1 is Ideal of L1;
A2: { X where X is Element of Y : X is Ideal of L1 } c= { X where X is Ideal of L1 : verum }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { X where X is Element of Y : X is Ideal of L1 } or z in { X where X is Ideal of L1 : verum } )
assume z in { X where X is Element of Y : X is Ideal of L1 } ; ::_thesis: z in { X where X is Ideal of L1 : verum }
then ex X1 being Element of Y st
( z = X1 & X1 is Ideal of L1 ) ;
hence z in { X where X is Ideal of L1 : verum } ; ::_thesis: verum
end;
A3: { H1(X) where X is Element of Y : S1[X] } is finite from PRE_CIRC:sch_1();
Ids L1 = { X where X is Ideal of L1 : verum } by WAYBEL_0:def_23
.= { X where X is Element of Y : X is Ideal of L1 } by A1, A2, XBOOLE_0:def_10 ;
hence Ids L1 is finite by A3; ::_thesis: verum
end;
theorem Th17: :: WAYBEL31:17
for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds
for B1 being with_bottom CLbasis of L1 holds B1 is infinite
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: ( L1 is infinite implies for B1 being with_bottom CLbasis of L1 holds B1 is infinite )
assume A1: L1 is infinite ; ::_thesis: for B1 being with_bottom CLbasis of L1 holds B1 is infinite
let B1 be with_bottom CLbasis of L1; ::_thesis: B1 is infinite
( dom (supMap (subrelstr B1)) = Ids (subrelstr B1) & rng (supMap (subrelstr B1)) = the carrier of L1 ) by WAYBEL23:51, WAYBEL23:65;
then card the carrier of L1 c= card (Ids (subrelstr B1)) by CARD_1:12;
then Ids (subrelstr B1) is infinite by A1;
then subrelstr B1 is infinite by Th16;
hence B1 is infinite by YELLOW_0:def_15; ::_thesis: verum
end;
theorem :: WAYBEL31:18
for L1 being non empty complete Poset
for x being Element of L1 st x is compact holds
x = inf (wayabove x)
proof
let L1 be non empty complete Poset; ::_thesis: for x being Element of L1 st x is compact holds
x = inf (wayabove x)
let x be Element of L1; ::_thesis: ( x is compact implies x = inf (wayabove x) )
assume x is compact ; ::_thesis: x = inf (wayabove x)
then x << x by WAYBEL_3:def_2;
then x in wayabove x by WAYBEL_3:8;
then A1: inf (wayabove x) <= x by YELLOW_2:22;
x <= inf (wayabove x) by WAYBEL14:9;
hence x = inf (wayabove x) by A1, YELLOW_0:def_3; ::_thesis: verum
end;
theorem Th19: :: WAYBEL31:19
for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds
for B1 being with_bottom CLbasis of L1 holds card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: ( L1 is infinite implies for B1 being with_bottom CLbasis of L1 holds card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1 )
assume A1: L1 is infinite ; ::_thesis: for B1 being with_bottom CLbasis of L1 holds card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1
let B1 be with_bottom CLbasis of L1; ::_thesis: card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1
consider a1 being set such that
A2: a1 in B1 by XBOOLE_0:def_1;
reconsider a1 = a1 as Element of L1 by A2;
{} L1 c= B1 by XBOOLE_1:2;
then Way_Up (a1,({} L1)) in { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } by A2;
then reconsider WU = { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } as non empty set ;
defpred S1[ Element of B1 * , set ] means ex y being Element of L1 ex z being Subset of L1 st
( y = $1 /. 1 & z = rng (Del ($1,1)) & $2 = Way_Up (y,z) );
A3: for x being Element of B1 * ex u being Element of WU st S1[x,u]
proof
let x be Element of B1 * ; ::_thesis: ex u being Element of WU st S1[x,u]
reconsider y = x /. 1 as Element of L1 by TARSKI:def_3;
rng (Del (x,1)) c= rng x by FINSEQ_3:106;
then A4: rng (Del (x,1)) c= B1 by XBOOLE_1:1;
then reconsider z = rng (Del (x,1)) as Subset of L1 by XBOOLE_1:1;
Way_Up (y,z) in { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } by A4;
then reconsider u = Way_Up (y,z) as Element of WU ;
take u ; ::_thesis: S1[x,u]
take y ; ::_thesis: ex z being Subset of L1 st
( y = x /. 1 & z = rng (Del (x,1)) & u = Way_Up (y,z) )
take z ; ::_thesis: ( y = x /. 1 & z = rng (Del (x,1)) & u = Way_Up (y,z) )
thus ( y = x /. 1 & z = rng (Del (x,1)) & u = Way_Up (y,z) ) ; ::_thesis: verum
end;
consider f being Function of (B1 *),WU such that
A5: for x being Element of B1 * holds S1[x,f . x] from FUNCT_2:sch_3(A3);
A6: dom f = B1 * by FUNCT_2:def_1;
A7: WU c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in WU or z in rng f )
assume z in WU ; ::_thesis: z in rng f
then consider a being Element of L1, A being finite Subset of L1 such that
A8: z = Way_Up (a,A) and
A9: a in B1 and
A10: A c= B1 ;
reconsider a1 = a as Element of B1 by A9;
consider p being FinSequence such that
A11: A = rng p by FINSEQ_1:52;
reconsider p = p as FinSequence of B1 by A10, A11, FINSEQ_1:def_4;
set q = <*a1*> ^ p;
A12: <*a1*> ^ p in B1 * by FINSEQ_1:def_11;
then consider y being Element of L1, v being Subset of L1 such that
A13: y = (<*a1*> ^ p) /. 1 and
A14: v = rng (Del ((<*a1*> ^ p),1)) and
A15: f . (<*a1*> ^ p) = Way_Up (y,v) by A5;
A16: a = y by A13, FINSEQ_5:15;
A = v by A11, A14, WSIERP_1:40;
hence z in rng f by A6, A8, A12, A15, A16, FUNCT_1:def_3; ::_thesis: verum
end;
B1 is infinite by A1, Th17;
then card B1 = card (B1 *) by CARD_4:24;
hence card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1 by A6, A7, CARD_1:12; ::_thesis: verum
end;
theorem Th20: :: WAYBEL31:20
for T being complete Lawson TopLattice
for X being finite Subset of T holds
( (uparrow X) ` is open & (downarrow X) ` is open )
proof
let T be complete Lawson TopLattice; ::_thesis: for X being finite Subset of T holds
( (uparrow X) ` is open & (downarrow X) ` is open )
let X be finite Subset of T; ::_thesis: ( (uparrow X) ` is open & (downarrow X) ` is open )
deffunc H1( Element of T) -> Element of K32( the carrier of T) = uparrow $1;
{ (uparrow x) where x is Element of T : x in X } c= bool the carrier of T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (uparrow x) where x is Element of T : x in X } or z in bool the carrier of T )
assume z in { (uparrow x) where x is Element of T : x in X } ; ::_thesis: z in bool the carrier of T
then ex x being Element of T st
( z = uparrow x & x in X ) ;
hence z in bool the carrier of T ; ::_thesis: verum
end;
then reconsider upx = { (uparrow x) where x is Element of T : x in X } as Subset-Family of T ;
{ (downarrow x) where x is Element of T : x in X } c= bool the carrier of T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (downarrow x) where x is Element of T : x in X } or z in bool the carrier of T )
assume z in { (downarrow x) where x is Element of T : x in X } ; ::_thesis: z in bool the carrier of T
then ex x being Element of T st
( z = downarrow x & x in X ) ;
hence z in bool the carrier of T ; ::_thesis: verum
end;
then reconsider dox = { (downarrow x) where x is Element of T : x in X } as Subset-Family of T ;
reconsider dox = dox as Subset-Family of T ;
reconsider upx = upx as Subset-Family of T ;
A1: uparrow X = union upx by YELLOW_9:4;
now__::_thesis:_for_P_being_Subset_of_T_st_P_in_upx_holds_
P_is_closed
let P be Subset of T; ::_thesis: ( P in upx implies P is closed )
assume P in upx ; ::_thesis: P is closed
then ex x being Element of T st
( P = uparrow x & x in X ) ;
hence P is closed by WAYBEL19:38; ::_thesis: verum
end;
then A2: upx is closed by TOPS_2:def_2;
A3: X is finite ;
{ H1(x) where x is Element of T : x in X } is finite from FRAENKEL:sch_21(A3);
then uparrow X is closed by A2, A1, TOPS_2:21;
hence (uparrow X) ` is open by TOPS_1:3; ::_thesis: (downarrow X) ` is open
deffunc H2( Element of T) -> Element of K32( the carrier of T) = downarrow $1;
A4: downarrow X = union dox by YELLOW_9:4;
now__::_thesis:_for_P_being_Subset_of_T_st_P_in_dox_holds_
P_is_closed
let P be Subset of T; ::_thesis: ( P in dox implies P is closed )
assume P in dox ; ::_thesis: P is closed
then ex x being Element of T st
( P = downarrow x & x in X ) ;
hence P is closed by WAYBEL19:38; ::_thesis: verum
end;
then A5: dox is closed by TOPS_2:def_2;
{ H2(x) where x is Element of T : x in X } is finite from FRAENKEL:sch_21(A3);
then downarrow X is closed by A5, A4, TOPS_2:21;
hence (downarrow X) ` is open by TOPS_1:3; ::_thesis: verum
end;
theorem Th21: :: WAYBEL31:21
for L1 being lower-bounded continuous sup-Semilattice
for T being correct Lawson TopAugmentation of L1
for B1 being with_bottom CLbasis of L1 holds { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being correct Lawson TopAugmentation of L1
for B1 being with_bottom CLbasis of L1 holds { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
let T be correct Lawson TopAugmentation of L1; ::_thesis: for B1 being with_bottom CLbasis of L1 holds { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
let B1 be with_bottom CLbasis of L1; ::_thesis: { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
{ (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= bool the carrier of T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } or z in bool the carrier of T )
assume z in { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } ; ::_thesis: z in bool the carrier of T
then ex a being Element of L1 ex A being finite Subset of L1 st
( z = Way_Up (a,A) & a in B1 & A c= B1 ) ;
hence z in bool the carrier of T by A1; ::_thesis: verum
end;
then reconsider WU = { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } as Subset-Family of T ;
reconsider WU = WU as Subset-Family of T ;
A2: now__::_thesis:_for_A_being_Subset_of_T_st_A_is_open_holds_
for_pT_being_Point_of_T_st_pT_in_A_holds_
ex_cT_being_Subset_of_T_st_
(_cT_in_WU_&_pT_in_cT_&_cT_c=_A_)
reconsider BL = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } as Basis of T by WAYBEL19:32;
set S = the Scott TopAugmentation of T;
let A be Subset of T; ::_thesis: ( A is open implies for pT being Point of T st pT in A holds
ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A ) )
assume A3: A is open ; ::_thesis: for pT being Point of T st pT in A holds
ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A )
let pT be Point of T; ::_thesis: ( pT in A implies ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A ) )
assume pT in A ; ::_thesis: ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A )
then consider a being Subset of T such that
A4: a in BL and
A5: pT in a and
A6: a c= A by A3, YELLOW_9:31;
consider W, FT being Subset of T such that
A7: a = W \ (uparrow FT) and
A8: W in sigma T and
A9: FT is finite by A4;
A10: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
then reconsider pS = pT as Element of the Scott TopAugmentation of T ;
reconsider W1 = W as Subset of the Scott TopAugmentation of T by A10;
sigma the Scott TopAugmentation of T = sigma T by A10, YELLOW_9:52;
then A11: W = union { (wayabove x) where x is Element of the Scott TopAugmentation of T : x in W1 } by A8, WAYBEL14:33;
reconsider pL = pS as Element of L1 by A1;
defpred S1[ set , set ] means ex b1, y1 being Element of L1 st
( y1 = $1 & b1 = $2 & b1 in B1 & not b1 <= pL & b1 << y1 );
A12: Bottom L1 in B1 by WAYBEL23:def_8;
pT in W by A5, A7, XBOOLE_0:def_5;
then consider k being set such that
A13: pT in k and
A14: k in { (wayabove x) where x is Element of the Scott TopAugmentation of T : x in W1 } by A11, TARSKI:def_4;
consider xS being Element of the Scott TopAugmentation of T such that
A15: k = wayabove xS and
A16: xS in W1 by A14;
reconsider xL = xS as Element of L1 by A1, A10;
xS << pS by A13, A15, WAYBEL_3:8;
then xL << pL by A1, A10, WAYBEL_8:8;
then consider bL being Element of L1 such that
A17: bL in B1 and
A18: xL <= bL and
A19: bL << pL by A12, WAYBEL23:47;
reconsider FL = FT as Subset of L1 by A1;
A20: uparrow FT = uparrow FL by A1, WAYBEL_0:13;
A21: not pT in uparrow FT by A5, A7, XBOOLE_0:def_5;
A22: for y being set st y in FL holds
ex b being set st S1[y,b]
proof
let y be set ; ::_thesis: ( y in FL implies ex b being set st S1[y,b] )
assume A23: y in FL ; ::_thesis: ex b being set st S1[y,b]
then reconsider y1 = y as Element of L1 ;
not y1 <= pL by A21, A20, A23, WAYBEL_0:def_16;
then consider b1 being Element of L1 such that
A24: ( b1 in B1 & not b1 <= pL & b1 << y1 ) by WAYBEL23:46;
reconsider b = b1 as set ;
take b ; ::_thesis: S1[y,b]
take b1 ; ::_thesis: ex y1 being Element of L1 st
( y1 = y & b1 = b & b1 in B1 & not b1 <= pL & b1 << y1 )
take y1 ; ::_thesis: ( y1 = y & b1 = b & b1 in B1 & not b1 <= pL & b1 << y1 )
thus ( y1 = y & b1 = b & b1 in B1 & not b1 <= pL & b1 << y1 ) by A24; ::_thesis: verum
end;
consider f being Function such that
A25: dom f = FL and
A26: for y being set st y in FL holds
S1[y,f . y] from CLASSES1:sch_1(A22);
rng f c= the carrier of L1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in the carrier of L1 )
assume z in rng f ; ::_thesis: z in the carrier of L1
then consider v being set such that
A27: v in dom f and
A28: z = f . v by FUNCT_1:def_3;
ex b1, y1 being Element of L1 st
( y1 = v & b1 = f . v & b1 in B1 & not b1 <= pL & b1 << y1 ) by A25, A26, A27;
hence z in the carrier of L1 by A28; ::_thesis: verum
end;
then reconsider FFL = rng f as Subset of L1 ;
A29: FFL c= B1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in FFL or z in B1 )
assume z in FFL ; ::_thesis: z in B1
then consider v being set such that
A30: v in dom f and
A31: z = f . v by FUNCT_1:def_3;
ex b1, y1 being Element of L1 st
( y1 = v & b1 = f . v & b1 in B1 & not b1 <= pL & b1 << y1 ) by A25, A26, A30;
hence z in B1 by A31; ::_thesis: verum
end;
A32: uparrow FL c= uparrow FFL
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in uparrow FL or z in uparrow FFL )
assume A33: z in uparrow FL ; ::_thesis: z in uparrow FFL
then reconsider z1 = z as Element of L1 ;
consider v1 being Element of L1 such that
A34: v1 <= z1 and
A35: v1 in FL by A33, WAYBEL_0:def_16;
consider b1, y1 being Element of L1 such that
A36: y1 = v1 and
A37: b1 = f . v1 and
b1 in B1 and
not b1 <= pL and
A38: b1 << y1 by A26, A35;
b1 << z1 by A34, A36, A38, WAYBEL_3:2;
then A39: b1 <= z1 by WAYBEL_3:1;
b1 in FFL by A25, A35, A37, FUNCT_1:def_3;
hence z in uparrow FFL by A39, WAYBEL_0:def_16; ::_thesis: verum
end;
reconsider cT = (wayabove bL) \ (uparrow FFL) as Subset of T by A1;
take cT = cT; ::_thesis: ( cT in WU & pT in cT & cT c= A )
( cT = Way_Up (bL,FFL) & FFL is finite ) by A9, A25, FINSET_1:8;
hence cT in WU by A17, A29; ::_thesis: ( pT in cT & cT c= A )
wayabove bL c= wayabove xL by A18, WAYBEL_3:12;
then A40: (wayabove bL) \ (uparrow FFL) c= (wayabove xL) \ (uparrow FL) by A32, XBOOLE_1:35;
for z being Element of L1 holds
( not z in FFL or not z <= pL )
proof
let z be Element of L1; ::_thesis: ( not z in FFL or not z <= pL )
assume z in FFL ; ::_thesis: not z <= pL
then consider v being set such that
A41: v in dom f and
A42: z = f . v by FUNCT_1:def_3;
ex b1, y1 being Element of L1 st
( y1 = v & b1 = f . v & b1 in B1 & not b1 <= pL & b1 << y1 ) by A25, A26, A41;
hence not z <= pL by A42; ::_thesis: verum
end;
then for z being Element of L1 holds
( not z <= pL or not z in FFL ) ;
then A43: not pL in uparrow FFL by WAYBEL_0:def_16;
pL in wayabove bL by A19, WAYBEL_3:8;
hence pT in cT by A43, XBOOLE_0:def_5; ::_thesis: cT c= A
wayabove xL c= W
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in wayabove xL or z in W )
wayabove xL = wayabove xS by A1, A10, YELLOW12:13;
then A44: wayabove xL in { (wayabove x) where x is Element of the Scott TopAugmentation of T : x in W1 } by A16;
assume z in wayabove xL ; ::_thesis: z in W
hence z in W by A11, A44, TARSKI:def_4; ::_thesis: verum
end;
then (wayabove xL) \ (uparrow FL) c= a by A7, A20, XBOOLE_1:33;
then (wayabove bL) \ (uparrow FFL) c= a by A40, XBOOLE_1:1;
hence cT c= A by A6, XBOOLE_1:1; ::_thesis: verum
end;
WU c= the topology of T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in WU or z in the topology of T )
assume z in WU ; ::_thesis: z in the topology of T
then consider a being Element of L1, A being finite Subset of L1 such that
A45: z = Way_Up (a,A) and
a in B1 and
A c= B1 ;
reconsider A1 = A as finite Subset of T by A1;
reconsider a1 = a as Element of T by A1;
( wayabove a1 is open & (uparrow A1) ` is open ) by Th20, WAYBEL19:40;
then A46: (wayabove a1) /\ ((uparrow A1) `) is open by TOPS_1:11;
z = (wayabove a1) \ (uparrow A) by A1, A45, YELLOW12:13
.= (wayabove a1) \ (uparrow A1) by A1, WAYBEL_0:13
.= (wayabove a1) /\ ((uparrow A1) `) by SUBSET_1:13 ;
hence z in the topology of T by A46, PRE_TOPC:def_2; ::_thesis: verum
end;
hence { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T by A2, YELLOW_9:32; ::_thesis: verum
end;
Lm2: for L1 being lower-bounded continuous sup-Semilattice
for T being correct Lawson TopAugmentation of L1 holds weight T c= CLweight L1
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being correct Lawson TopAugmentation of L1 holds weight T c= CLweight L1
let T be correct Lawson TopAugmentation of L1; ::_thesis: weight T c= CLweight L1
consider B1 being with_bottom CLbasis of L1 such that
A1: card B1 = CLweight L1 by Th2;
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def_4;
now__::_thesis:_weight_T_c=_CLweight_L1
percases ( L1 is finite or L1 is infinite ) ;
supposeA3: L1 is finite ; ::_thesis: weight T c= CLweight L1
then A4: T is finite by A2;
B1 = the carrier of (CompactSublatt L1) by A1, A3, Th13
.= the carrier of L1 by A3, YELLOW15:26 ;
hence weight T c= CLweight L1 by A2, A1, A4, Th8; ::_thesis: verum
end;
supposeA5: L1 is infinite ; ::_thesis: weight T c= CLweight L1
set WU = { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } ;
{ (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T by Th21;
then A6: weight T c= card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } by WAYBEL23:73;
card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= CLweight L1 by A1, A5, Th19;
hence weight T c= CLweight L1 by A6, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
hence weight T c= CLweight L1 ; ::_thesis: verum
end;
theorem Th22: :: WAYBEL31:22
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1
for b being Basis of T holds { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being Scott TopAugmentation of L1
for b being Basis of T holds { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T
let T be Scott TopAugmentation of L1; ::_thesis: for b being Basis of T holds { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T
let b be Basis of T; ::_thesis: { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T
set b2 = { (wayabove (inf u)) where u is Subset of T : u in b } ;
{ (wayabove (inf u)) where u is Subset of T : u in b } c= bool the carrier of T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (wayabove (inf u)) where u is Subset of T : u in b } or z in bool the carrier of T )
assume z in { (wayabove (inf u)) where u is Subset of T : u in b } ; ::_thesis: z in bool the carrier of T
then ex u being Subset of T st
( z = wayabove (inf u) & u in b ) ;
hence z in bool the carrier of T ; ::_thesis: verum
end;
then reconsider b2 = { (wayabove (inf u)) where u is Subset of T : u in b } as Subset-Family of T ;
reconsider b1 = { (wayabove x) where x is Element of T : verum } as Basis of T by WAYBEL11:45;
A1: now__::_thesis:_for_A_being_Subset_of_T_st_A_is_open_holds_
for_a_being_Point_of_T_st_a_in_A_holds_
ex_u_being_Element_of_K32(_the_carrier_of_T)_st_
(_u_in_b2_&_a_in_u_&_u_c=_A_)
let A be Subset of T; ::_thesis: ( A is open implies for a being Point of T st a in A holds
ex u being Element of K32( the carrier of T) st
( u in b2 & a in u & u c= A ) )
assume A2: A is open ; ::_thesis: for a being Point of T st a in A holds
ex u being Element of K32( the carrier of T) st
( u in b2 & a in u & u c= A )
let a be Point of T; ::_thesis: ( a in A implies ex u being Element of K32( the carrier of T) st
( u in b2 & a in u & u c= A ) )
assume a in A ; ::_thesis: ex u being Element of K32( the carrier of T) st
( u in b2 & a in u & u c= A )
then consider C being Subset of T such that
A3: C in b1 and
A4: a in C and
A5: C c= A by A2, YELLOW_9:31;
C is open by A3, YELLOW_8:10;
then consider D being Subset of T such that
A6: D in b and
A7: a in D and
A8: D c= C by A4, YELLOW_9:31;
D is open by A6, YELLOW_8:10;
then consider E being Subset of T such that
A9: E in b1 and
A10: a in E and
A11: E c= D by A7, YELLOW_9:31;
consider z being Element of T such that
A12: E = wayabove z by A9;
take u = wayabove (inf D); ::_thesis: ( u in b2 & a in u & u c= A )
thus u in b2 by A6; ::_thesis: ( a in u & u c= A )
reconsider a1 = a as Element of T ;
consider x being Element of T such that
A13: C = wayabove x by A3;
z << a1 by A10, A12, WAYBEL_3:8;
then consider y being Element of T such that
A14: z << y and
A15: y << a1 by WAYBEL_4:52;
( inf D is_<=_than D & y in wayabove z ) by A14, WAYBEL_3:8, YELLOW_0:33;
then inf D <= y by A11, A12, LATTICE3:def_8;
then inf D << a1 by A15, WAYBEL_3:2;
hence a in u by WAYBEL_3:8; ::_thesis: u c= A
A16: wayabove x c= uparrow x by WAYBEL_3:11;
( ex_inf_of uparrow x,T & ex_inf_of D,T ) by YELLOW_0:17;
then inf (uparrow x) <= inf D by A13, A8, A16, XBOOLE_1:1, YELLOW_0:35;
then x <= inf D by WAYBEL_0:39;
then wayabove (inf D) c= C by A13, WAYBEL_3:12;
hence u c= A by A5, XBOOLE_1:1; ::_thesis: verum
end;
b2 c= the topology of T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in b2 or z in the topology of T )
assume z in b2 ; ::_thesis: z in the topology of T
then consider u being Subset of T such that
A17: z = wayabove (inf u) and
u in b ;
wayabove (inf u) is open by WAYBEL11:36;
hence z in the topology of T by A17, PRE_TOPC:def_2; ::_thesis: verum
end;
hence { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T by A1, YELLOW_9:32; ::_thesis: verum
end;
theorem Th23: :: WAYBEL31:23
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1
for B1 being Basis of T st B1 is infinite holds
{ (inf u) where u is Subset of T : u in B1 } is infinite
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being Scott TopAugmentation of L1
for B1 being Basis of T st B1 is infinite holds
{ (inf u) where u is Subset of T : u in B1 } is infinite
let T be Scott TopAugmentation of L1; ::_thesis: for B1 being Basis of T st B1 is infinite holds
{ (inf u) where u is Subset of T : u in B1 } is infinite
let B1 be Basis of T; ::_thesis: ( B1 is infinite implies { (inf u) where u is Subset of T : u in B1 } is infinite )
reconsider B2 = { (inf u) where u is Subset of T : u in B1 } as set ;
defpred S1[ set , set ] means ex y being Element of T st
( $1 = y & $2 = wayabove y );
reconsider B3 = { (wayabove (inf u)) where u is Subset of T : u in B1 } as Basis of T by Th22;
assume that
A1: B1 is infinite and
A2: { (inf u) where u is Subset of T : u in B1 } is finite ; ::_thesis: contradiction
A3: for x being set st x in B2 holds
ex y being set st
( y in B3 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in B2 implies ex y being set st
( y in B3 & S1[x,y] ) )
assume x in B2 ; ::_thesis: ex y being set st
( y in B3 & S1[x,y] )
then A4: ex u1 being Subset of T st
( x = inf u1 & u1 in B1 ) ;
then reconsider z = x as Element of T ;
take y = wayabove z; ::_thesis: ( y in B3 & S1[x,y] )
thus y in B3 by A4; ::_thesis: S1[x,y]
take z ; ::_thesis: ( x = z & y = wayabove z )
thus ( x = z & y = wayabove z ) ; ::_thesis: verum
end;
consider f being Function such that
A5: dom f = B2 and
A6: rng f c= B3 and
A7: for x being set st x in B2 holds
S1[x,f . x] from FUNCT_1:sch_5(A3);
B3 c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in B3 or z in rng f )
assume z in B3 ; ::_thesis: z in rng f
then consider u1 being Subset of T such that
A8: z = wayabove (inf u1) and
A9: u1 in B1 ;
inf u1 in B2 by A9;
then A10: ex y being Element of T st
( inf u1 = y & f . (inf u1) = wayabove y ) by A7;
inf u1 in B2 by A9;
hence z in rng f by A5, A8, A10, FUNCT_1:def_3; ::_thesis: verum
end;
then rng f = B3 by A6, XBOOLE_0:def_10;
then B3 is finite by A2, A5, FINSET_1:8;
then T is finite by YELLOW15:30;
hence contradiction by A1; ::_thesis: verum
end;
Lm3: for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1 holds CLweight L1 c= weight T
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being Scott TopAugmentation of L1 holds CLweight L1 c= weight T
let T be Scott TopAugmentation of L1; ::_thesis: CLweight L1 c= weight T
consider B1 being Basis of T such that
A1: card B1 = weight T by WAYBEL23:74;
{ (inf u) where u is Subset of T : u in B1 } c= the carrier of T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (inf u) where u is Subset of T : u in B1 } or z in the carrier of T )
assume z in { (inf u) where u is Subset of T : u in B1 } ; ::_thesis: z in the carrier of T
then ex u being Subset of T st
( z = inf u & u in B1 ) ;
hence z in the carrier of T ; ::_thesis: verum
end;
then reconsider B0 = { (inf u) where u is Subset of T : u in B1 } as Subset of T ;
set B2 = finsups B0;
defpred S1[ set , set ] means ex y being Subset of T st
( $1 = y & $2 = inf y );
A2: for x being set st x in B1 holds
ex y being set st
( y in B0 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in B1 implies ex y being set st
( y in B0 & S1[x,y] ) )
assume A3: x in B1 ; ::_thesis: ex y being set st
( y in B0 & S1[x,y] )
then reconsider z = x as Subset of T ;
take y = inf z; ::_thesis: ( y in B0 & S1[x,y] )
thus y in B0 by A3; ::_thesis: S1[x,y]
take z ; ::_thesis: ( x = z & y = inf z )
thus ( x = z & y = inf z ) ; ::_thesis: verum
end;
consider f being Function such that
A4: dom f = B1 and
rng f c= B0 and
A5: for x being set st x in B1 holds
S1[x,f . x] from FUNCT_1:sch_5(A2);
B0 c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in B0 or z in rng f )
assume z in B0 ; ::_thesis: z in rng f
then consider u being Subset of T such that
A6: z = inf u and
A7: u in B1 ;
ex y being Subset of T st
( u = y & f . u = inf y ) by A5, A7;
hence z in rng f by A4, A6, A7, FUNCT_1:def_3; ::_thesis: verum
end;
then A8: card B0 c= card B1 by A4, CARD_1:12;
A9: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
A10: now__::_thesis:_card_(finsups_B0)_=_card_B0
percases ( L1 is finite or L1 is infinite ) ;
supposeA11: L1 is finite ; ::_thesis: card (finsups B0) = card B0
the carrier of L1 c= B0
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the carrier of L1 or z in B0 )
assume z in the carrier of L1 ; ::_thesis: z in B0
then reconsider z1 = z as Element of T by A9;
z1 <= z1 ;
then A12: z1 in uparrow z1 by WAYBEL_0:18;
T is finite by A9, A11;
then uparrow z1 is open by WAYBEL11:def_5;
then consider A being Subset of T such that
A13: A in B1 and
A14: z1 in A and
A15: A c= uparrow z1 by A12, YELLOW_9:31;
( ex_inf_of uparrow z1,T & ex_inf_of A,T ) by YELLOW_0:17;
then inf (uparrow z1) <= inf A by A15, YELLOW_0:35;
then A16: z1 <= inf A by WAYBEL_0:39;
inf A <= z1 by A14, YELLOW_2:22;
then z = inf A by A16, YELLOW_0:def_3;
hence z in B0 by A13; ::_thesis: verum
end;
then ( B0 c= finsups B0 & finsups B0 c= B0 ) by A9, WAYBEL_0:50, XBOOLE_1:1;
hence card (finsups B0) = card B0 by XBOOLE_0:def_10; ::_thesis: verum
end;
suppose L1 is infinite ; ::_thesis: card (finsups B0) = card B0
then T is infinite by A9;
then B0 is infinite by Th23, YELLOW15:30;
hence card (finsups B0) = card B0 by YELLOW15:27; ::_thesis: verum
end;
end;
end;
( ex_sup_of {} ,T & {} is finite Subset of B0 ) by XBOOLE_1:2, YELLOW_0:42;
then "\/" ({},T) in { ("\/" (Y,T)) where Y is finite Subset of B0 : ex_sup_of Y,T } ;
then "\/" ({},T) in finsups B0 by WAYBEL_0:def_27;
then A17: Bottom L1 in finsups B0 by A9, YELLOW_0:26, YELLOW_0:42;
reconsider B2 = finsups B0 as Subset of L1 by A9;
now__::_thesis:_for_x,_y_being_Element_of_L1_st_x_in_B2_&_y_in_B2_holds_
sup_{x,y}_in_B2
let x, y be Element of L1; ::_thesis: ( x in B2 & y in B2 implies sup {x,y} in B2 )
assume that
A18: x in B2 and
A19: y in B2 ; ::_thesis: sup {x,y} in B2
y in { ("\/" (Y,T)) where Y is finite Subset of B0 : ex_sup_of Y,T } by A19, WAYBEL_0:def_27;
then consider Y2 being finite Subset of B0 such that
A20: y = "\/" (Y2,T) and
A21: ex_sup_of Y2,T ;
x in { ("\/" (Y,T)) where Y is finite Subset of B0 : ex_sup_of Y,T } by A18, WAYBEL_0:def_27;
then consider Y1 being finite Subset of B0 such that
A22: x = "\/" (Y1,T) and
A23: ex_sup_of Y1,T ;
A24: ex_sup_of Y1 \/ Y2,T by YELLOW_0:17;
sup {x,y} = x "\/" y by YELLOW_0:41
.= ("\/" (Y1,T)) "\/" ("\/" (Y2,T)) by A9, A22, A20, YELLOW12:10
.= "\/" ((Y1 \/ Y2),T) by A23, A21, YELLOW_2:3 ;
then sup {x,y} in { ("\/" (Y,T)) where Y is finite Subset of B0 : ex_sup_of Y,T } by A24;
hence sup {x,y} in B2 by WAYBEL_0:def_27; ::_thesis: verum
end;
then reconsider B2 = B2 as join-closed Subset of L1 by WAYBEL23:18;
for x, y being Element of L1 st x << y holds
ex b being Element of L1 st
( b in B2 & x <= b & b << y )
proof
let x, y be Element of L1; ::_thesis: ( x << y implies ex b being Element of L1 st
( b in B2 & x <= b & b << y ) )
reconsider x1 = x, y1 = y as Element of T by A9;
A25: B0 c= B2 by WAYBEL_0:50;
assume x << y ; ::_thesis: ex b being Element of L1 st
( b in B2 & x <= b & b << y )
then y in wayabove x by WAYBEL_3:8;
then A26: y1 in wayabove x1 by A9, YELLOW12:13;
wayabove x1 is open by WAYBEL11:36;
then consider u being Subset of T such that
A27: u in B1 and
A28: y1 in u and
A29: u c= wayabove x1 by A26, YELLOW_9:31;
reconsider b = inf u as Element of L1 by A9;
take b ; ::_thesis: ( b in B2 & x <= b & b << y )
b in B0 by A27;
hence b in B2 by A25; ::_thesis: ( x <= b & b << y )
A30: wayabove x1 c= uparrow x1 by WAYBEL_3:11;
( ex_inf_of uparrow x1,T & ex_inf_of u,T ) by YELLOW_0:17;
then inf (uparrow x1) <= inf u by A29, A30, XBOOLE_1:1, YELLOW_0:35;
then x1 <= inf u by WAYBEL_0:39;
hence x <= b by A9, YELLOW_0:1; ::_thesis: b << y
u is open by A27, YELLOW_8:10;
hence b << y by A9, A28, WAYBEL14:26, WAYBEL_8:8; ::_thesis: verum
end;
then A31: B2 is CLbasis of L1 by A17, WAYBEL23:47;
B2 is with_bottom by A17, WAYBEL23:def_8;
then CLweight L1 c= card B0 by A10, A31, Th1;
hence CLweight L1 c= weight T by A1, A8, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th24: :: WAYBEL31:24
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1 holds CLweight L1 = weight T
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being Scott TopAugmentation of L1 holds CLweight L1 = weight T
let T be Scott TopAugmentation of L1; ::_thesis: CLweight L1 = weight T
set T1 = the correct Lawson TopAugmentation of L1;
( weight T c= weight the correct Lawson TopAugmentation of L1 & weight the correct Lawson TopAugmentation of L1 c= CLweight L1 ) by Lm1, Lm2;
then A1: weight T c= CLweight L1 by XBOOLE_1:1;
CLweight L1 c= weight T by Lm3;
hence CLweight L1 = weight T by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: WAYBEL31:25
for L1 being lower-bounded continuous sup-Semilattice
for T being correct Lawson TopAugmentation of L1 holds CLweight L1 = weight T
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being correct Lawson TopAugmentation of L1 holds CLweight L1 = weight T
let T be correct Lawson TopAugmentation of L1; ::_thesis: CLweight L1 = weight T
set T1 = the Scott TopAugmentation of L1;
( CLweight L1 c= weight the Scott TopAugmentation of L1 & weight the Scott TopAugmentation of L1 c= weight T ) by Lm1, Lm3;
then A1: CLweight L1 c= weight T by XBOOLE_1:1;
weight T c= CLweight L1 by Lm2;
hence CLweight L1 = weight T by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th26: :: WAYBEL31:26
for L1, L2 being non empty RelStr st L1,L2 are_isomorphic holds
card the carrier of L1 = card the carrier of L2
proof
let L1, L2 be non empty RelStr ; ::_thesis: ( L1,L2 are_isomorphic implies card the carrier of L1 = card the carrier of L2 )
assume L1,L2 are_isomorphic ; ::_thesis: card the carrier of L1 = card the carrier of L2
then consider f being Function of L1,L2 such that
A1: f is isomorphic by WAYBEL_1:def_8;
A2: dom f = the carrier of L1 by FUNCT_2:def_1;
( f is V13() & rng f = the carrier of L2 ) by A1, WAYBEL_0:66;
then the carrier of L1, the carrier of L2 are_equipotent by A2, WELLORD2:def_4;
hence card the carrier of L1 = card the carrier of L2 by CARD_1:5; ::_thesis: verum
end;
theorem :: WAYBEL31:27
for L1 being lower-bounded continuous sup-Semilattice
for B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1 holds
CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1)))
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1 holds
CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1)))
let B1 be with_bottom CLbasis of L1; ::_thesis: ( card B1 = CLweight L1 implies CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1))) )
assume A1: card B1 = CLweight L1 ; ::_thesis: CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1)))
A2: card the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B1)))) = card the carrier of (subrelstr B1) by Th26, WAYBEL23:69;
thus CLweight (InclPoset (Ids (subrelstr B1))) = card the carrier of (CompactSublatt (InclPoset (Ids (subrelstr B1)))) by Th3
.= CLweight L1 by A1, A2, YELLOW_0:def_15 ; ::_thesis: verum
end;
registration
let L1 be lower-bounded continuous sup-Semilattice;
cluster InclPoset (sigma L1) -> with_suprema continuous ;
coherence
( InclPoset (sigma L1) is with_suprema & InclPoset (sigma L1) is continuous )
proof
set S = the Scott TopAugmentation of L1;
A1: RelStr(# the carrier of the Scott TopAugmentation of L1, the InternalRel of the Scott TopAugmentation of L1 #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def_4;
InclPoset (sigma the Scott TopAugmentation of L1) is complete ;
hence InclPoset (sigma L1) is with_suprema by A1, YELLOW_9:52; ::_thesis: InclPoset (sigma L1) is continuous
InclPoset (sigma the Scott TopAugmentation of L1) is continuous by WAYBEL14:36;
hence InclPoset (sigma L1) is continuous by A1, YELLOW_9:52; ::_thesis: verum
end;
end;
theorem :: WAYBEL31:28
for L1 being lower-bounded continuous sup-Semilattice holds CLweight L1 c= CLweight (InclPoset (sigma L1))
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: CLweight L1 c= CLweight (InclPoset (sigma L1))
set S = the Scott TopAugmentation of L1;
A1: RelStr(# the carrier of the Scott TopAugmentation of L1, the InternalRel of the Scott TopAugmentation of L1 #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def_4;
A2: InclPoset the topology of the Scott TopAugmentation of L1 = InclPoset (sigma L1) by YELLOW_9:51;
A3: CLweight L1 = weight the Scott TopAugmentation of L1 by Th24;
now__::_thesis:_CLweight_L1_c=_CLweight_(InclPoset_(sigma_L1))
percases ( L1 is infinite or L1 is finite ) ;
suppose L1 is infinite ; ::_thesis: CLweight L1 c= CLweight (InclPoset (sigma L1))
then the Scott TopAugmentation of L1 is infinite by A1;
hence CLweight L1 c= CLweight (InclPoset (sigma L1)) by A3, A2, Th6; ::_thesis: verum
end;
supposeA4: L1 is finite ; ::_thesis: CLweight L1 c= CLweight (InclPoset (sigma L1))
A5: card the carrier of the Scott TopAugmentation of L1 c= card the carrier of (InclPoset (sigma L1)) by A2, Th7;
A6: the Scott TopAugmentation of L1 is finite by A1, A4;
then weight the Scott TopAugmentation of L1 = card the carrier of the Scott TopAugmentation of L1 by Th8;
hence CLweight L1 c= CLweight (InclPoset (sigma L1)) by A3, A2, A6, A5, Th9; ::_thesis: verum
end;
end;
end;
hence CLweight L1 c= CLweight (InclPoset (sigma L1)) ; ::_thesis: verum
end;
theorem :: WAYBEL31:29
for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds
CLweight L1 = CLweight (InclPoset (sigma L1))
proof
let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: ( L1 is infinite implies CLweight L1 = CLweight (InclPoset (sigma L1)) )
set S = the Scott TopAugmentation of L1;
assume A1: L1 is infinite ; ::_thesis: CLweight L1 = CLweight (InclPoset (sigma L1))
A2: ( CLweight L1 = weight the Scott TopAugmentation of L1 & InclPoset the topology of the Scott TopAugmentation of L1 = InclPoset (sigma L1) ) by Th24, YELLOW_9:51;
RelStr(# the carrier of the Scott TopAugmentation of L1, the InternalRel of the Scott TopAugmentation of L1 #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def_4;
then the Scott TopAugmentation of L1 is infinite by A1;
hence CLweight L1 = CLweight (InclPoset (sigma L1)) by A2, Th6; ::_thesis: verum
end;