:: TOPGEN_2 semantic presentation
begin
theorem Th1: :: TOPGEN_2:1
for T being non empty TopSpace
for B being Basis of T
for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x
proof
let T be non empty TopSpace; ::_thesis: for B being Basis of T
for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x
let B be Basis of T; ::_thesis: for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x
let x be Element of T; ::_thesis: { U where U is Subset of T : ( x in U & U in B ) } is Basis of x
set Bx = { U where U is Subset of T : ( x in U & U in B ) } ;
A1: { U where U is Subset of T : ( x in U & U in B ) } c= B
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { U where U is Subset of T : ( x in U & U in B ) } or a in B )
assume a in { U where U is Subset of T : ( x in U & U in B ) } ; ::_thesis: a in B
then ex U being Subset of T st
( a = U & x in U & U in B ) ;
hence a in B ; ::_thesis: verum
end;
then reconsider Bx = { U where U is Subset of T : ( x in U & U in B ) } as Subset-Family of T by XBOOLE_1:1;
Bx is Basis of x
proof
B c= the topology of T by TOPS_2:64;
then Bx c= the topology of T by A1, XBOOLE_1:1;
then A2: Bx is open by TOPS_2:64;
Bx is x -quasi_basis
proof
now__::_thesis:_for_a_being_set_st_a_in_Bx_holds_
x_in_a
let a be set ; ::_thesis: ( a in Bx implies x in a )
assume a in Bx ; ::_thesis: x in a
then ex U being Subset of T st
( a = U & x in U & U in B ) ;
hence x in a ; ::_thesis: verum
end;
hence x in Intersect Bx by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of K32( the carrier of T) holds
( not b1 is open or not x in b1 or ex b2 being Element of K32( the carrier of T) st
( b2 in Bx & b2 c= b1 ) )
let S be Subset of T; ::_thesis: ( not S is open or not x in S or ex b1 being Element of K32( the carrier of T) st
( b1 in Bx & b1 c= S ) )
assume that
A3: S is open and
A4: x in S ; ::_thesis: ex b1 being Element of K32( the carrier of T) st
( b1 in Bx & b1 c= S )
consider V being Subset of T such that
A5: V in B and
A6: x in V and
A7: V c= S by A3, A4, YELLOW_9:31;
V in Bx by A5, A6;
hence ex b1 being Element of K32( the carrier of T) st
( b1 in Bx & b1 c= S ) by A7; ::_thesis: verum
end;
hence Bx is Basis of x by A2; ::_thesis: verum
end;
hence { U where U is Subset of T : ( x in U & U in B ) } is Basis of x ; ::_thesis: verum
end;
theorem Th2: :: TOPGEN_2:2
for T being non empty TopSpace
for B being ManySortedSet of T st ( for x being Element of T holds B . x is Basis of x ) holds
Union B is Basis of T
proof
let T be non empty TopSpace; ::_thesis: for B being ManySortedSet of T st ( for x being Element of T holds B . x is Basis of x ) holds
Union B is Basis of T
let B be ManySortedSet of T; ::_thesis: ( ( for x being Element of T holds B . x is Basis of x ) implies Union B is Basis of T )
assume A1: for x being Element of T holds B . x is Basis of x ; ::_thesis: Union B is Basis of T
Union B c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Union B or a in bool the carrier of T )
assume a in Union B ; ::_thesis: a in bool the carrier of T
then consider b being set such that
A2: b in dom B and
A3: a in B . b by CARD_5:2;
reconsider b = b as Point of T by A2;
B . b is Basis of b by A1;
hence a in bool the carrier of T by A3; ::_thesis: verum
end;
then reconsider W = Union B as Subset-Family of T ;
A4: dom B = the carrier of T by PARTFUN1:def_2;
A5: now__::_thesis:_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_W_&_p_in_a_&_a_c=_A_)
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 W & p in a & a c= A ) )
assume A6: A is open ; ::_thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in W & p in a & a c= A )
let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st
( a in W & p in a & a c= A ) )
assume A7: p in A ; ::_thesis: ex a being Subset of T st
( a in W & p in a & a c= A )
A8: B . p is Basis of p by A1;
then consider a being Subset of T such that
A9: a in B . p and
A10: a c= A by A6, A7, YELLOW_8:def_1;
take a = a; ::_thesis: ( a in W & p in a & a c= A )
thus a in W by A4, A9, CARD_5:2; ::_thesis: ( p in a & a c= A )
thus p in a by A8, A9, YELLOW_8:12; ::_thesis: a c= A
thus a c= A by A10; ::_thesis: verum
end;
W c= the topology of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in W or a in the topology of T )
assume a in W ; ::_thesis: a in the topology of T
then consider b being set such that
A11: b in dom B and
A12: a in B . b by CARD_5:2;
reconsider b = b as Point of T by A11;
B . b is Basis of b by A1;
then B . b c= the topology of T by TOPS_2:64;
hence a in the topology of T by A12; ::_thesis: verum
end;
hence Union B is Basis of T by A5, YELLOW_9:32; ::_thesis: verum
end;
definition
let T be non empty TopStruct ;
let x be Element of T;
func Chi (x,T) -> cardinal number means :Def1: :: TOPGEN_2:def 1
( ex B being Basis of x st it = card B & ( for B being Basis of x holds it c= card B ) );
existence
ex b1 being cardinal number st
( ex B being Basis of x st b1 = card B & ( for B being Basis of x holds b1 c= card B ) )
proof
set B0 = the Basis of x;
defpred S1[ ordinal number ] means ex B being Basis of x st $1 = card B;
card the Basis of x is ordinal ;
then A1: ex A being ordinal number st S1[A] ;
consider A being ordinal number such that
A2: S1[A] and
A3: for B being ordinal number st S1[B] holds
A c= B from ORDINAL1:sch_1(A1);
consider B1 being Basis of x such that
A4: A = card B1 by A2;
take card B1 ; ::_thesis: ( ex B being Basis of x st card B1 = card B & ( for B being Basis of x holds card B1 c= card B ) )
thus ( ex B being Basis of x st card B1 = card B & ( for B being Basis of x holds card B1 c= card B ) ) by A3, A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being cardinal number st ex B being Basis of x st b1 = card B & ( for B being Basis of x holds b1 c= card B ) & ex B being Basis of x st b2 = card B & ( for B being Basis of x holds b2 c= card B ) holds
b1 = b2
proof
let M1, M2 be cardinal number ; ::_thesis: ( ex B being Basis of x st M1 = card B & ( for B being Basis of x holds M1 c= card B ) & ex B being Basis of x st M2 = card B & ( for B being Basis of x holds M2 c= card B ) implies M1 = M2 )
assume that
A5: ex B being Basis of x st M1 = card B and
A6: for B being Basis of x holds M1 c= card B and
A7: ex B being Basis of x st M2 = card B and
A8: for B being Basis of x holds M2 c= card B ; ::_thesis: M1 = M2
thus ( M1 c= M2 & M2 c= M1 ) by A5, A6, A7, A8; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Chi TOPGEN_2:def_1_:_
for T being non empty TopStruct
for x being Element of T
for b3 being cardinal number holds
( b3 = Chi (x,T) iff ( ex B being Basis of x st b3 = card B & ( for B being Basis of x holds b3 c= card B ) ) );
theorem Th3: :: TOPGEN_2:3
for X being set st ( for a being set st a in X holds
a is cardinal number ) holds
union X is cardinal number
proof
let X be set ; ::_thesis: ( ( for a being set st a in X holds
a is cardinal number ) implies union X is cardinal number )
assume A1: for a being set st a in X holds
a is cardinal number ; ::_thesis: union X is cardinal number
now__::_thesis:_for_a_being_set_st_a_in_X_holds_
ex_b_being_set_st_
(_b_in_X_&_a_c=_b_&_b_is_cardinal_set_)
let a be set ; ::_thesis: ( a in X implies ex b being set st
( b in X & a c= b & b is cardinal set ) )
assume A2: a in X ; ::_thesis: ex b being set st
( b in X & a c= b & b is cardinal set )
then a is cardinal number by A1;
hence ex b being set st
( b in X & a c= b & b is cardinal set ) by A2; ::_thesis: verum
end;
hence union X is cardinal number by CARD_LAR:32; ::_thesis: verum
end;
Lm1: now__::_thesis:_for_T_being_non_empty_TopStruct_holds_
(_union__{__(Chi_(x,T))_where_x_is_Point_of_T_:_verum__}__is_cardinal_number_&_(_for_m_being_cardinal_number_st_m_=_union__{__(Chi_(x,T))_where_x_is_Point_of_T_:_verum__}__holds_
(_(_for_x_being_Point_of_T_holds_Chi_(x,T)_c=_m_)_&_(_for_M_being_cardinal_number_st_(_for_x_being_Point_of_T_holds_Chi_(x,T)_c=_M_)_holds_
m_c=_M_)_)_)_)
let T be non empty TopStruct ; ::_thesis: ( union { (Chi (x,T)) where x is Point of T : verum } is cardinal number & ( for m being cardinal number st m = union { (Chi (x,T)) where x is Point of T : verum } holds
( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) ) ) )
set X = { (Chi (x,T)) where x is Point of T : verum } ;
now__::_thesis:_for_a_being_set_st_a_in__{__(Chi_(x,T))_where_x_is_Point_of_T_:_verum__}__holds_
a_is_cardinal_number
let a be set ; ::_thesis: ( a in { (Chi (x,T)) where x is Point of T : verum } implies a is cardinal number )
assume a in { (Chi (x,T)) where x is Point of T : verum } ; ::_thesis: a is cardinal number
then ex x being Point of T st a = Chi (x,T) ;
hence a is cardinal number ; ::_thesis: verum
end;
hence union { (Chi (x,T)) where x is Point of T : verum } is cardinal number by Th3; ::_thesis: for m being cardinal number st m = union { (Chi (x,T)) where x is Point of T : verum } holds
( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) )
let m be cardinal number ; ::_thesis: ( m = union { (Chi (x,T)) where x is Point of T : verum } implies ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) ) )
assume A1: m = union { (Chi (x,T)) where x is Point of T : verum } ; ::_thesis: ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) )
hereby ::_thesis: for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M
let x be Point of T; ::_thesis: Chi (x,T) c= m
Chi (x,T) in { (Chi (x,T)) where x is Point of T : verum } ;
hence Chi (x,T) c= m by A1, ZFMISC_1:74; ::_thesis: verum
end;
let M be cardinal number ; ::_thesis: ( ( for x being Point of T holds Chi (x,T) c= M ) implies m c= M )
assume A2: for x being Point of T holds Chi (x,T) c= M ; ::_thesis: m c= M
now__::_thesis:_for_a_being_set_st_a_in__{__(Chi_(x,T))_where_x_is_Point_of_T_:_verum__}__holds_
a_c=_M
let a be set ; ::_thesis: ( a in { (Chi (x,T)) where x is Point of T : verum } implies a c= M )
assume a in { (Chi (x,T)) where x is Point of T : verum } ; ::_thesis: a c= M
then ex x being Point of T st a = Chi (x,T) ;
hence a c= M by A2; ::_thesis: verum
end;
hence m c= M by A1, ZFMISC_1:76; ::_thesis: verum
end;
definition
let T be non empty TopStruct ;
func Chi T -> cardinal number means :Def2: :: TOPGEN_2:def 2
( ( for x being Point of T holds Chi (x,T) c= it ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
it c= M ) );
existence
ex b1 being cardinal number st
( ( for x being Point of T holds Chi (x,T) c= b1 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
b1 c= M ) )
proof
set X = { (Chi (x,T)) where x is Point of T : verum } ;
reconsider m = union { (Chi (x,T)) where x is Point of T : verum } as cardinal number by Lm1;
take m ; ::_thesis: ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) )
thus ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) ) by Lm1; ::_thesis: verum
end;
uniqueness
for b1, b2 being cardinal number st ( for x being Point of T holds Chi (x,T) c= b1 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
b1 c= M ) & ( for x being Point of T holds Chi (x,T) c= b2 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
b2 c= M ) holds
b1 = b2
proof
let M1, M2 be cardinal number ; ::_thesis: ( ( for x being Point of T holds Chi (x,T) c= M1 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
M1 c= M ) & ( for x being Point of T holds Chi (x,T) c= M2 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
M2 c= M ) implies M1 = M2 )
assume that
A1: for x being Point of T holds Chi (x,T) c= M1 and
A2: for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
M1 c= M and
A3: for x being Point of T holds Chi (x,T) c= M2 and
A4: for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
M2 c= M ; ::_thesis: M1 = M2
thus ( M1 c= M2 & M2 c= M1 ) by A1, A2, A3, A4; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Chi TOPGEN_2:def_2_:_
for T being non empty TopStruct
for b2 being cardinal number holds
( b2 = Chi T iff ( ( for x being Point of T holds Chi (x,T) c= b2 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
b2 c= M ) ) );
theorem Th4: :: TOPGEN_2:4
for T being non empty TopStruct holds Chi T = union { (Chi (x,T)) where x is Point of T : verum }
proof
let T be non empty TopStruct ; ::_thesis: Chi T = union { (Chi (x,T)) where x is Point of T : verum }
set X = { (Chi (x,T)) where x is Point of T : verum } ;
reconsider m = union { (Chi (x,T)) where x is Point of T : verum } as cardinal number by Lm1;
A1: for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M by Lm1;
for x being Point of T holds Chi (x,T) c= m by Lm1;
hence Chi T = union { (Chi (x,T)) where x is Point of T : verum } by A1, Def2; ::_thesis: verum
end;
theorem Th5: :: TOPGEN_2:5
for T being non empty TopStruct
for x being Point of T holds Chi (x,T) c= Chi T
proof
let T be non empty TopStruct ; ::_thesis: for x being Point of T holds Chi (x,T) c= Chi T
set X = { (Chi (x,T)) where x is Point of T : verum } ;
let x be Point of T; ::_thesis: Chi (x,T) c= Chi T
A1: Chi (x,T) in { (Chi (x,T)) where x is Point of T : verum } ;
Chi T = union { (Chi (x,T)) where x is Point of T : verum } by Th4;
hence Chi (x,T) c= Chi T by A1, ZFMISC_1:74; ::_thesis: verum
end;
theorem :: TOPGEN_2:6
for T being non empty TopSpace holds
( T is first-countable iff Chi T c= omega )
proof
let T be non empty TopSpace; ::_thesis: ( T is first-countable iff Chi T c= omega )
set X = { (Chi (x,T)) where x is Point of T : verum } ;
A1: Chi T = union { (Chi (x,T)) where x is Point of T : verum } by Th4;
thus ( T is first-countable implies Chi T c= omega ) ::_thesis: ( Chi T c= omega implies T is first-countable )
proof
assume A2: for x being Point of T ex B being Basis of x st B is countable ; :: according to FRECHET:def_2 ::_thesis: Chi T c= omega
now__::_thesis:_for_a_being_set_st_a_in__{__(Chi_(x,T))_where_x_is_Point_of_T_:_verum__}__holds_
a_c=_omega
let a be set ; ::_thesis: ( a in { (Chi (x,T)) where x is Point of T : verum } implies a c= omega )
assume a in { (Chi (x,T)) where x is Point of T : verum } ; ::_thesis: a c= omega
then consider x being Point of T such that
A3: a = Chi (x,T) ;
consider B being Basis of x such that
A4: B is countable by A2;
A5: card B c= omega by A4, CARD_3:def_14;
Chi (x,T) c= card B by Def1;
hence a c= omega by A3, A5, XBOOLE_1:1; ::_thesis: verum
end;
hence Chi T c= omega by A1, ZFMISC_1:76; ::_thesis: verum
end;
assume A6: Chi T c= omega ; ::_thesis: T is first-countable
let x be Point of T; :: according to FRECHET:def_2 ::_thesis: ex b1 being Element of K32(K32( the carrier of T)) st b1 is countable
consider B being Basis of x such that
A7: Chi (x,T) = card B by Def1;
take B ; ::_thesis: B is countable
Chi (x,T) c= Chi T by Th5;
hence card B c= omega by A6, A7, XBOOLE_1:1; :: according to CARD_3:def_14 ::_thesis: verum
end;
begin
definition
let T be non empty TopSpace;
mode Neighborhood_System of T -> ManySortedSet of T means :Def3: :: TOPGEN_2:def 3
for x being Element of T holds it . x is Basis of x;
existence
ex b1 being ManySortedSet of T st
for x being Element of T holds b1 . x is Basis of x
proof
set B = the Basis of T;
deffunc H1( Point of T) -> set = { U where U is Subset of T : ( $1 in U & U in the Basis of T ) } ;
consider F being ManySortedSet of T such that
A1: for x being Point of T holds F . x = H1(x) from PBOOLE:sch_5();
take F ; ::_thesis: for x being Element of T holds F . x is Basis of x
let x be Point of T; ::_thesis: F . x is Basis of x
F . x = H1(x) by A1;
hence F . x is Basis of x by Th1; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Neighborhood_System TOPGEN_2:def_3_:_
for T being non empty TopSpace
for b2 being ManySortedSet of T holds
( b2 is Neighborhood_System of T iff for x being Element of T holds b2 . x is Basis of x );
definition
let T be non empty TopSpace;
let N be Neighborhood_System of T;
:: original: Union
redefine func Union N -> Basis of T;
coherence
Union N is Basis of T
proof
for x being Point of T holds N . x is Basis of x by Def3;
hence Union N is Basis of T by Th2; ::_thesis: verum
end;
let x be Point of T;
:: original: .
redefine funcN . x -> Basis of x;
coherence
N . x is Basis of x by Def3;
end;
theorem :: TOPGEN_2:7
for T being non empty TopSpace
for x, y being Point of T
for B1 being Basis of x
for B2 being Basis of y
for U being set st x in U & U in B2 holds
ex V being open Subset of T st
( V in B1 & V c= U )
proof
let T be non empty TopSpace; ::_thesis: for x, y being Point of T
for B1 being Basis of x
for B2 being Basis of y
for U being set st x in U & U in B2 holds
ex V being open Subset of T st
( V in B1 & V c= U )
let x, y be Point of T; ::_thesis: for B1 being Basis of x
for B2 being Basis of y
for U being set st x in U & U in B2 holds
ex V being open Subset of T st
( V in B1 & V c= U )
let B1 be Basis of x; ::_thesis: for B2 being Basis of y
for U being set st x in U & U in B2 holds
ex V being open Subset of T st
( V in B1 & V c= U )
let B2 be Basis of y; ::_thesis: for U being set st x in U & U in B2 holds
ex V being open Subset of T st
( V in B1 & V c= U )
let U be set ; ::_thesis: ( x in U & U in B2 implies ex V being open Subset of T st
( V in B1 & V c= U ) )
assume that
A1: x in U and
A2: U in B2 ; ::_thesis: ex V being open Subset of T st
( V in B1 & V c= U )
U is open Subset of T by A2, YELLOW_8:12;
then consider V being Subset of T such that
A3: V in B1 and
A4: V c= U by A1, YELLOW_8:13;
V is open by A3, YELLOW_8:12;
hence ex V being open Subset of T st
( V in B1 & V c= U ) by A3, A4; ::_thesis: verum
end;
theorem :: TOPGEN_2:8
for T being non empty TopSpace
for x being Point of T
for B being Basis of x
for U1, U2 being set st U1 in B & U2 in B holds
ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
proof
let T be non empty TopSpace; ::_thesis: for x being Point of T
for B being Basis of x
for U1, U2 being set st U1 in B & U2 in B holds
ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
let x be Point of T; ::_thesis: for B being Basis of x
for U1, U2 being set st U1 in B & U2 in B holds
ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
let B be Basis of x; ::_thesis: for U1, U2 being set st U1 in B & U2 in B holds
ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
let U1, U2 be set ; ::_thesis: ( U1 in B & U2 in B implies ex V being open Subset of T st
( V in B & V c= U1 /\ U2 ) )
assume that
A1: U1 in B and
A2: U2 in B ; ::_thesis: ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
reconsider U1 = U1, U2 = U2 as open Subset of T by A1, A2, YELLOW_8:12;
A3: x in U2 by A2, YELLOW_8:12;
x in U1 by A1, YELLOW_8:12;
then x in U1 /\ U2 by A3, XBOOLE_0:def_4;
then consider V being Subset of T such that
A4: V in B and
A5: V c= U1 /\ U2 by YELLOW_8:13;
V is open by A4, YELLOW_8:12;
hence ex V being open Subset of T st
( V in B & V c= U1 /\ U2 ) by A4, A5; ::_thesis: verum
end;
Lm2: now__::_thesis:_for_T_being_non_empty_TopSpace
for_A_being_Subset_of_T
for_x_being_Element_of_T_st_x_in_Cl_A_holds_
for_B_being_Basis_of_x
for_U_being_set_st_U_in_B_holds_
U_meets_A
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for x being Element of T st x in Cl A holds
for B being Basis of x
for U being set st U in B holds
U meets A
let A be Subset of T; ::_thesis: for x being Element of T st x in Cl A holds
for B being Basis of x
for U being set st U in B holds
U meets A
let x be Element of T; ::_thesis: ( x in Cl A implies for B being Basis of x
for U being set st U in B holds
U meets A )
assume A1: x in Cl A ; ::_thesis: for B being Basis of x
for U being set st U in B holds
U meets A
let B be Basis of x; ::_thesis: for U being set st U in B holds
U meets A
let U be set ; ::_thesis: ( U in B implies U meets A )
assume A2: U in B ; ::_thesis: U meets A
then x in U by YELLOW_8:12;
then U meets Cl A by A1, XBOOLE_0:3;
hence U meets A by A2, TSEP_1:36, YELLOW_8:12; ::_thesis: verum
end;
Lm3: now__::_thesis:_for_T_being_non_empty_TopSpace
for_A_being_Subset_of_T
for_x_being_Element_of_T_st_ex_B_being_Basis_of_x_st_
for_U_being_set_st_U_in_B_holds_
U_meets_A_holds_
x_in_Cl_A
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for x being Element of T st ex B being Basis of x st
for U being set st U in B holds
U meets A holds
x in Cl A
let A be Subset of T; ::_thesis: for x being Element of T st ex B being Basis of x st
for U being set st U in B holds
U meets A holds
x in Cl A
let x be Element of T; ::_thesis: ( ex B being Basis of x st
for U being set st U in B holds
U meets A implies x in Cl A )
given B being Basis of x such that A1: for U being set st U in B holds
U meets A ; ::_thesis: x in Cl A
now__::_thesis:_for_U_being_Subset_of_T_st_U_is_open_&_x_in_U_holds_
A_meets_U
let U be Subset of T; ::_thesis: ( U is open & x in U implies A meets U )
assume that
A2: U is open and
A3: x in U ; ::_thesis: A meets U
ex V being Subset of T st
( V in B & V c= U ) by A2, A3, YELLOW_8:def_1;
hence A meets U by A1, XBOOLE_1:63; ::_thesis: verum
end;
hence x in Cl A by PRE_TOPC:def_7; ::_thesis: verum
end;
theorem :: TOPGEN_2:9
for T being non empty TopSpace
for A being Subset of T
for x being Element of T holds
( x in Cl A iff for B being Basis of x
for U being set st U in B holds
U meets A )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for x being Element of T holds
( x in Cl A iff for B being Basis of x
for U being set st U in B holds
U meets A )
let A be Subset of T; ::_thesis: for x being Element of T holds
( x in Cl A iff for B being Basis of x
for U being set st U in B holds
U meets A )
let x be Element of T; ::_thesis: ( x in Cl A iff for B being Basis of x
for U being set st U in B holds
U meets A )
set B = the Basis of x;
thus ( x in Cl A implies for B being Basis of x
for U being set st U in B holds
U meets A ) by Lm2; ::_thesis: ( ( for B being Basis of x
for U being set st U in B holds
U meets A ) implies x in Cl A )
assume for B being Basis of x
for U being set st U in B holds
U meets A ; ::_thesis: x in Cl A
then for U being set st U in the Basis of x holds
U meets A ;
hence x in Cl A by Lm3; ::_thesis: verum
end;
theorem :: TOPGEN_2:10
for T being non empty TopSpace
for A being Subset of T
for x being Element of T holds
( x in Cl A iff ex B being Basis of x st
for U being set st U in B holds
U meets A )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T
for x being Element of T holds
( x in Cl A iff ex B being Basis of x st
for U being set st U in B holds
U meets A )
let A be Subset of T; ::_thesis: for x being Element of T holds
( x in Cl A iff ex B being Basis of x st
for U being set st U in B holds
U meets A )
let x be Element of T; ::_thesis: ( x in Cl A iff ex B being Basis of x st
for U being set st U in B holds
U meets A )
set B = the Basis of x;
( x in Cl A implies for U being set st U in the Basis of x holds
U meets A ) by Lm2;
hence ( x in Cl A implies ex B being Basis of x st
for U being set st U in B holds
U meets A ) ; ::_thesis: ( ex B being Basis of x st
for U being set st U in B holds
U meets A implies x in Cl A )
thus ( ex B being Basis of x st
for U being set st U in B holds
U meets A implies x in Cl A ) by Lm3; ::_thesis: verum
end;
registration
let T be TopSpace;
cluster non empty open for Element of K32(K32( the carrier of T));
existence
ex b1 being Subset-Family of T st
( b1 is open & not b1 is empty )
proof
take the topology of T ; ::_thesis: ( the topology of T is open & not the topology of T is empty )
thus ( the topology of T is open & not the topology of T is empty ) ; ::_thesis: verum
end;
end;
begin
theorem Th11: :: TOPGEN_2:11
for T being non empty TopSpace
for S being open Subset-Family of T ex G being open Subset-Family of T st
( G c= S & union G = union S & card G c= weight T )
proof
defpred S1[ set , set ] means $1 c= $2;
let T be non empty TopSpace; ::_thesis: for S being open Subset-Family of T ex G being open Subset-Family of T st
( G c= S & union G = union S & card G c= weight T )
let S be open Subset-Family of T; ::_thesis: ex G being open Subset-Family of T st
( G c= S & union G = union S & card G c= weight T )
consider B being Basis of T such that
A1: card B = weight T by WAYBEL23:74;
set B1 = { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } ;
{ W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } c= B
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } or a in B )
assume a in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } ; ::_thesis: a in B
then ex W being Subset of T st
( a = W & W in B & ex U being set st
( U in S & W c= U ) ) ;
hence a in B ; ::_thesis: verum
end;
then A2: card { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } c= card B by CARD_1:11;
A3: now__::_thesis:_for_a_being_set_st_a_in__{__W_where_W_is_Subset_of_T_:_(_W_in_B_&_ex_U_being_set_st_
(_U_in_S_&_W_c=_U_)_)__}__holds_
ex_b_being_set_st_
(_b_in_S_&_S1[a,b]_)
let a be set ; ::_thesis: ( a in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } implies ex b being set st
( b in S & S1[a,b] ) )
assume a in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } ; ::_thesis: ex b being set st
( b in S & S1[a,b] )
then ex W being Subset of T st
( a = W & W in B & ex U being set st
( U in S & W c= U ) ) ;
hence ex b being set st
( b in S & S1[a,b] ) ; ::_thesis: verum
end;
consider f being Function such that
A4: ( dom f = { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } & rng f c= S ) and
A5: for a being set st a in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } holds
S1[a,f . a] from FUNCT_1:sch_5(A3);
set G = rng f;
reconsider G = rng f as open Subset-Family of T by A4, TOPS_2:11, XBOOLE_1:1;
take G ; ::_thesis: ( G c= S & union G = union S & card G c= weight T )
thus ( G c= S & union G c= union S ) by A4, ZFMISC_1:77; :: according to XBOOLE_0:def_10 ::_thesis: ( union S c= union G & card G c= weight T )
thus union S c= union G ::_thesis: card G c= weight T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union S or a in union G )
assume a in union S ; ::_thesis: a in union G
then consider b being set such that
A6: a in b and
A7: b in S by TARSKI:def_4;
reconsider b = b as open Subset of T by A7, TOPS_2:def_1;
reconsider a = a as Point of T by A6, A7;
consider W0 being Subset of T such that
A8: W0 in B and
A9: a in W0 and
A10: W0 c= b by A6, YELLOW_9:31;
A11: W0 in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } by A7, A8, A10;
then f . W0 in G by A4, FUNCT_1:def_3;
then A12: f . W0 c= union G by ZFMISC_1:74;
W0 c= f . W0 by A5, A11;
then a in f . W0 by A9;
hence a in union G by A12; ::_thesis: verum
end;
card G c= card { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } by A4, CARD_1:12;
hence card G c= weight T by A1, A2, XBOOLE_1:1; ::_thesis: verum
end;
definition
let T be TopStruct ;
attrT is finite-weight means :Def4: :: TOPGEN_2:def 4
weight T is finite ;
end;
:: deftheorem Def4 defines finite-weight TOPGEN_2:def_4_:_
for T being TopStruct holds
( T is finite-weight iff weight T is finite );
notation
let T be TopStruct ;
antonym infinite-weight T for finite-weight ;
end;
registration
cluster finite -> finite-weight for TopStruct ;
coherence
for b1 being TopStruct st b1 is finite holds
b1 is finite-weight
proof
let T be TopStruct ; ::_thesis: ( T is finite implies T is finite-weight )
assume A1: the carrier of T is finite ; :: according to STRUCT_0:def_11 ::_thesis: T is finite-weight
ex B being Basis of T st card B = weight T by WAYBEL23:74;
hence weight T is finite by A1; :: according to TOPGEN_2:def_4 ::_thesis: verum
end;
cluster infinite-weight -> infinite for TopStruct ;
coherence
for b1 being TopStruct st b1 is infinite-weight holds
b1 is infinite ;
end;
theorem Th12: :: TOPGEN_2:12
for X being set holds card (SmallestPartition X) = card X
proof
let X be set ; ::_thesis: card (SmallestPartition X) = card X
set A = SmallestPartition X;
percases ( X = {} or X <> {} ) ;
suppose X = {} ; ::_thesis: card (SmallestPartition X) = card X
hence card (SmallestPartition X) = card X by EQREL_1:32; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: card (SmallestPartition X) = card X
then reconsider X = X as non empty set ;
deffunc H1( set ) -> set = {$1};
A1: SmallestPartition X = { {x} where x is Element of X : verum } by EQREL_1:37;
then A2: for a being set st a in X holds
H1(a) in SmallestPartition X ;
consider f being Function of X,(SmallestPartition X) such that
A3: for a being set st a in X holds
f . a = H1(a) from FUNCT_2:sch_2(A2);
A4: rng f = SmallestPartition X
proof
thus rng f c= SmallestPartition X ; :: according to XBOOLE_0:def_10 ::_thesis: SmallestPartition X c= rng f
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SmallestPartition X or a in rng f )
assume a in SmallestPartition X ; ::_thesis: a in rng f
then consider b being Element of X such that
A5: a = {b} by A1;
f . b = a by A3, A5;
hence a in rng f by FUNCT_2:4; ::_thesis: verum
end;
A6: f is one-to-one
proof
let a be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not a in proj1 f or not b1 in proj1 f or not f . a = f . b1 or a = b1 )
let b be set ; ::_thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b )
assume that
A7: a in dom f and
A8: b in dom f ; ::_thesis: ( not f . a = f . b or a = b )
assume f . a = f . b ; ::_thesis: a = b
then {a} = f . b by A3, A7
.= {b} by A3, A8 ;
hence a = b by ZFMISC_1:3; ::_thesis: verum
end;
dom f = X by FUNCT_2:def_1;
then X, SmallestPartition X are_equipotent by A4, A6, WELLORD2:def_4;
hence card (SmallestPartition X) = card X by CARD_1:5; ::_thesis: verum
end;
end;
end;
theorem Th13: :: TOPGEN_2:13
for T being non empty discrete TopStruct holds
( SmallestPartition the carrier of T is Basis of T & ( for B being Basis of T holds SmallestPartition the carrier of T c= B ) )
proof
let T be non empty discrete TopStruct ; ::_thesis: ( SmallestPartition the carrier of T is Basis of T & ( for B being Basis of T holds SmallestPartition the carrier of T c= B ) )
set B0 = SmallestPartition the carrier of T;
A1: SmallestPartition the carrier of T c= the topology of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SmallestPartition the carrier of T or a in the topology of T )
assume a in SmallestPartition the carrier of T ; ::_thesis: a in the topology of T
then reconsider a = a as Subset of T ;
a is open by TDLAT_3:15;
hence a in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
A2: SmallestPartition the carrier of T = { {a} where a is Element of T : verum } by EQREL_1:37;
now__::_thesis:_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_SmallestPartition_the_carrier_of_T_&_p_in_a_&_a_c=_A_)
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 SmallestPartition the carrier of T & 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 SmallestPartition the carrier of T & p in a & a c= A )
let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st
( a in SmallestPartition the carrier of T & p in a & a c= A ) )
assume A3: p in A ; ::_thesis: ex a being Subset of T st
( a in SmallestPartition the carrier of T & p in a & a c= A )
reconsider a = {p} as Subset of T ;
take a = a; ::_thesis: ( a in SmallestPartition the carrier of T & p in a & a c= A )
thus a in SmallestPartition the carrier of T by A2; ::_thesis: ( p in a & a c= A )
thus p in a by TARSKI:def_1; ::_thesis: a c= A
thus a c= A by A3, ZFMISC_1:31; ::_thesis: verum
end;
hence A4: SmallestPartition the carrier of T is Basis of T by A1, YELLOW_9:32; ::_thesis: for B being Basis of T holds SmallestPartition the carrier of T c= B
let B be Basis of T; ::_thesis: SmallestPartition the carrier of T c= B
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SmallestPartition the carrier of T or a in B )
assume A5: a in SmallestPartition the carrier of T ; ::_thesis: a in B
then consider b being Element of T such that
A6: a = {b} by A2;
reconsider a = a as Subset of T by A5;
A7: b in a by A6, TARSKI:def_1;
a is open by A4, A5, YELLOW_8:10;
then consider U being Subset of T such that
A8: U in B and
A9: b in U and
A10: U c= a by A7, YELLOW_9:31;
a c= U by A6, A9, ZFMISC_1:31;
hence a in B by A8, A10, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th14: :: TOPGEN_2:14
for T being non empty discrete TopStruct holds weight T = card the carrier of T
proof
let T be non empty discrete TopStruct ; ::_thesis: weight T = card the carrier of T
set M = { (card C) where C is Basis of T : verum } ;
reconsider B0 = SmallestPartition the carrier of T as Basis of T by Th13;
A1: card B0 in { (card C) where C is Basis of T : verum } ;
A2: card B0 = card the carrier of T by Th12;
weight T = meet { (card C) where C is Basis of T : verum } by WAYBEL23:def_5;
hence weight T c= card the carrier of T by A2, A1, SETFAM_1:3; :: according to XBOOLE_0:def_10 ::_thesis: card the carrier of T c= weight T
ex B being Basis of T st card B = weight T by WAYBEL23:74;
hence card the carrier of T c= weight T by A2, Th13, CARD_1:11; ::_thesis: verum
end;
registration
cluster TopSpace-like infinite-weight for TopStruct ;
existence
ex b1 being TopSpace st b1 is infinite-weight
proof
set A = the infinite set ;
reconsider O = bool the infinite set as Subset-Family of the infinite set ;
reconsider T = TopStruct(# the infinite set ,O #) as non empty discrete TopStruct by TDLAT_3:def_1;
take T ; ::_thesis: T is infinite-weight
weight T = card the carrier of T by Th14;
hence weight T is infinite ; :: according to TOPGEN_2:def_4 ::_thesis: verum
end;
end;
Lm4: for T being infinite-weight TopSpace
for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
proof
let T be infinite-weight TopSpace; ::_thesis: for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
let B be Basis of T; ::_thesis: ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
consider B0 being Basis of T such that
A1: card B0 = weight T by WAYBEL23:74;
defpred S1[ set , set ] means ( union $2 = $1 & card $2 c= weight T );
A2: now__::_thesis:_for_a_being_set_st_a_in_B0_holds_
ex_b_being_set_st_
(_b_in_bool_B_&_S1[a,b]_)
let a be set ; ::_thesis: ( a in B0 implies ex b being set st
( b in bool B & S1[a,b] ) )
set Sa = { U where U is Subset of T : ( U in B & U c= a ) } ;
A3: { U where U is Subset of T : ( U in B & U c= a ) } c= B
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { U where U is Subset of T : ( U in B & U c= a ) } or b in B )
assume b in { U where U is Subset of T : ( U in B & U c= a ) } ; ::_thesis: b in B
then ex U being Subset of T st
( b = U & U in B & U c= a ) ;
hence b in B ; ::_thesis: verum
end;
assume a in B0 ; ::_thesis: ex b being set st
( b in bool B & S1[a,b] )
then reconsider W = a as open Subset of T by YELLOW_8:10;
A4: union { U where U is Subset of T : ( U in B & U c= a ) } = W by YELLOW_8:9;
reconsider Sa = { U where U is Subset of T : ( U in B & U c= a ) } as open Subset-Family of T by A3, TOPS_2:11, XBOOLE_1:1;
consider G being open Subset-Family of T such that
A5: G c= Sa and
A6: union G = union Sa and
A7: card G c= weight T by Th11;
reconsider b = G as set ;
take b = b; ::_thesis: ( b in bool B & S1[a,b] )
b c= B by A3, A5, XBOOLE_1:1;
hence b in bool B ; ::_thesis: S1[a,b]
thus S1[a,b] by A4, A6, A7; ::_thesis: verum
end;
consider f being Function such that
A8: ( dom f = B0 & rng f c= bool B ) and
A9: for a being set st a in B0 holds
S1[a,f . a] from FUNCT_1:sch_5(A2);
A10: Union f c= union (bool B) by A8, ZFMISC_1:77;
then A11: Union f c= B by ZFMISC_1:81;
then reconsider B1 = Union f as Subset-Family of T by XBOOLE_1:1;
now__::_thesis:_(_B1_c=_the_topology_of_T_&_(_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_B1_&_p_in_a_&_a_c=_A_)_)_)
B c= the topology of T by TOPS_2:64;
hence B1 c= the topology of T by A11, XBOOLE_1:1; ::_thesis: 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 B1 & p in a & a c= A )
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 B1 & p in a & a c= A ) )
assume A12: A is open ; ::_thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in B1 & p in a & a c= A )
let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st
( a in B1 & p in a & a c= A ) )
assume p in A ; ::_thesis: ex a being Subset of T st
( a in B1 & p in a & a c= A )
then consider U being Subset of T such that
A13: U in B0 and
A14: p in U and
A15: U c= A by A12, YELLOW_9:31;
A16: S1[U,f . U] by A9, A13;
then consider a being set such that
A17: p in a and
A18: a in f . U by A14, TARSKI:def_4;
A19: a c= U by A16, A18, ZFMISC_1:74;
a in B1 by A8, A13, A18, CARD_5:2;
hence ex a being Subset of T st
( a in B1 & p in a & a c= A ) by A15, A17, A19, XBOOLE_1:1; ::_thesis: verum
end;
then reconsider B1 = B1 as Basis of T by YELLOW_9:32;
now__::_thesis:_(_card_(rng_f)_c=_weight_T_&_(_for_a_being_set_st_a_in_rng_f_holds_
card_a_c=_weight_T_)_)
thus card (rng f) c= weight T by A1, A8, CARD_1:12; ::_thesis: for a being set st a in rng f holds
card a c= weight T
let a be set ; ::_thesis: ( a in rng f implies card a c= weight T )
assume a in rng f ; ::_thesis: card a c= weight T
then ex b being set st
( b in dom f & a = f . b ) by FUNCT_1:def_3;
hence card a c= weight T by A8, A9; ::_thesis: verum
end;
then A20: card B1 c= (weight T) *` (weight T) by CARD_2:87;
take B1 ; ::_thesis: ( B1 c= B & card B1 = weight T )
thus B1 c= B by A10, ZFMISC_1:81; ::_thesis: card B1 = weight T
weight T is infinite by Def4;
hence card B1 c= weight T by A20, CARD_4:15; :: according to XBOOLE_0:def_10 ::_thesis: weight T c= card B1
thus weight T c= card B1 by WAYBEL23:73; ::_thesis: verum
end;
theorem Th15: :: TOPGEN_2:15
for T being non empty finite-weight TopSpace ex B0 being Basis of T ex f being Function of the carrier of T, the topology of T st
( B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) )
proof
let T be non empty finite-weight TopSpace; ::_thesis: ex B0 being Basis of T ex f being Function of the carrier of T, the topology of T st
( B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) )
consider B being Basis of T such that
A1: card B = weight T by WAYBEL23:74;
deffunc H1( set ) -> set = meet { U where U is Subset of T : ( $1 in U & U in B ) } ;
A2: B is finite by A1, Def4;
A3: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_T_holds_
H1(a)_in_the_topology_of_T
B c= the topology of T by TOPS_2:64;
then FinMeetCl B c= FinMeetCl the topology of T by CANTOR_1:14;
then A4: FinMeetCl B c= the topology of T by CANTOR_1:5;
let a be set ; ::_thesis: ( a in the carrier of T implies H1(a) in the topology of T )
assume a in the carrier of T ; ::_thesis: H1(a) in the topology of T
then reconsider x = a as Point of T ;
set S = { U where U is Subset of T : ( x in U & U in B ) } ;
consider U being Subset of T such that
A5: U in B and
A6: x in U and
U c= [#] T by YELLOW_9:31;
A7: { U where U is Subset of T : ( x in U & U in B ) } c= B
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { U where U is Subset of T : ( x in U & U in B ) } or a in B )
assume a in { U where U is Subset of T : ( x in U & U in B ) } ; ::_thesis: a in B
then ex U being Subset of T st
( a = U & x in U & U in B ) ;
hence a in B ; ::_thesis: verum
end;
then reconsider S = { U where U is Subset of T : ( x in U & U in B ) } as Subset-Family of T by XBOOLE_1:1;
Intersect S in FinMeetCl B by A2, A7, CANTOR_1:def_3;
then A8: Intersect S in the topology of T by A4;
U in S by A5, A6;
hence H1(a) in the topology of T by A8, SETFAM_1:def_9; ::_thesis: verum
end;
consider f being Function of the carrier of T, the topology of T such that
A9: for a being set st a in the carrier of T holds
f . a = H1(a) from FUNCT_2:sch_2(A3);
set B0 = rng f;
reconsider B0 = rng f as Subset-Family of T by XBOOLE_1:1;
A10: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_T_holds_
a_in_f_._a
let a be set ; ::_thesis: ( a in the carrier of T implies a in f . a )
assume a in the carrier of T ; ::_thesis: a in f . a
then reconsider x = a as Point of T ;
set S = { U where U is Subset of T : ( x in U & U in B ) } ;
consider U being Subset of T such that
A11: U in B and
A12: x in U and
U c= [#] T by YELLOW_9:31;
A13: now__::_thesis:_for_b_being_set_st_b_in__{__U_where_U_is_Subset_of_T_:_(_x_in_U_&_U_in_B_)__}__holds_
a_in_b
let b be set ; ::_thesis: ( b in { U where U is Subset of T : ( x in U & U in B ) } implies a in b )
assume b in { U where U is Subset of T : ( x in U & U in B ) } ; ::_thesis: a in b
then ex U being Subset of T st
( b = U & a in U & U in B ) ;
hence a in b ; ::_thesis: verum
end;
A14: f . a = meet { U where U is Subset of T : ( x in U & U in B ) } by A9;
U in { U where U is Subset of T : ( x in U & U in B ) } by A11, A12;
hence a in f . a by A14, A13, SETFAM_1:def_1; ::_thesis: verum
end;
A15: now__::_thesis:_for_x_being_Point_of_T
for_V_being_Subset_of_T_st_x_in_V_&_V_is_open_holds_
f_._x_c=_V
let x be Point of T; ::_thesis: for V being Subset of T st x in V & V is open holds
f . x c= V
let V be Subset of T; ::_thesis: ( x in V & V is open implies f . x c= V )
set S = { U where U is Subset of T : ( x in U & U in B ) } ;
assume that
A16: x in V and
A17: V is open ; ::_thesis: f . x c= V
consider U being Subset of T such that
A18: U in B and
A19: x in U and
A20: U c= V by A16, A17, YELLOW_9:31;
A21: f . x = meet { U where U is Subset of T : ( x in U & U in B ) } by A9;
U in { U where U is Subset of T : ( x in U & U in B ) } by A18, A19;
then f . x c= U by A21, SETFAM_1:3;
hence f . x c= V by A20, XBOOLE_1:1; ::_thesis: verum
end;
now__::_thesis:_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_B0_&_p_in_a_&_a_c=_A_)
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 B0 & p in a & a c= A ) )
assume A22: A is open ; ::_thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in B0 & p in a & a c= A )
let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st
( a in B0 & p in a & a c= A ) )
assume A23: p in A ; ::_thesis: ex a being Subset of T st
( a in B0 & p in a & a c= A )
f . p in the topology of T ;
then reconsider a = f . p as Subset of T ;
take a = a; ::_thesis: ( a in B0 & p in a & a c= A )
thus a in B0 by FUNCT_2:4; ::_thesis: ( p in a & a c= A )
thus p in a by A10; ::_thesis: a c= A
thus a c= A by A15, A22, A23; ::_thesis: verum
end;
then reconsider B0 = B0 as Basis of T by YELLOW_9:32;
take B0 ; ::_thesis: ex f being Function of the carrier of T, the topology of T st
( B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) )
take f ; ::_thesis: ( B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) )
thus B0 = rng f ; ::_thesis: for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) )
let x be Point of T; ::_thesis: ( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) )
thus ( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) by A10, A15; ::_thesis: verum
end;
theorem Th16: :: TOPGEN_2:16
for T being TopSpace
for B0, B being Basis of T
for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
B0 c= B
proof
let T be TopSpace; ::_thesis: for B0, B being Basis of T
for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
B0 c= B
let B0, B be Basis of T; ::_thesis: for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
B0 c= B
let f be Function of the carrier of T, the topology of T; ::_thesis: ( B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) implies B0 c= B )
assume A1: B0 = rng f ; ::_thesis: ( ex x being Point of T st
( x in f . x implies ex U being open Subset of T st
( x in U & not f . x c= U ) ) or B0 c= B )
assume A2: for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ; ::_thesis: B0 c= B
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B0 or a in B )
assume A3: a in B0 ; ::_thesis: a in B
then reconsider V = a as Subset of T ;
consider b being set such that
A4: b in dom f and
A5: a = f . b by A1, A3, FUNCT_1:def_3;
A6: V is open by A3, YELLOW_8:10;
reconsider b = b as Element of T by A4;
b in V by A2, A5;
then consider U being Subset of T such that
A7: U in B and
A8: b in U and
A9: U c= V by A6, YELLOW_9:31;
U is open by A7, YELLOW_8:10;
then a c= U by A2, A5, A8;
hence a in B by A7, A9, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th17: :: TOPGEN_2:17
for T being TopSpace
for B0 being Basis of T
for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
weight T = card B0
proof
let T be TopSpace; ::_thesis: for B0 being Basis of T
for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
weight T = card B0
let B0 be Basis of T; ::_thesis: for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
weight T = card B0
let f be Function of the carrier of T, the topology of T; ::_thesis: ( B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) implies weight T = card B0 )
assume that
A1: B0 = rng f and
A2: for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ; ::_thesis: weight T = card B0
set M = { (card C) where C is Basis of T : verum } ;
A3: card B0 in { (card C) where C is Basis of T : verum } ;
weight T = meet { (card C) where C is Basis of T : verum } by WAYBEL23:def_5;
hence weight T c= card B0 by A3, SETFAM_1:3; :: according to XBOOLE_0:def_10 ::_thesis: card B0 c= weight T
ex B being Basis of T st card B = weight T by WAYBEL23:74;
hence card B0 c= weight T by A1, A2, Th16, CARD_1:11; ::_thesis: verum
end;
Lm5: for T being non empty finite-weight TopSpace
for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
proof
let T be non empty finite-weight TopSpace; ::_thesis: for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
let B be Basis of T; ::_thesis: ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
consider B0 being Basis of T, f being Function of the carrier of T, the topology of T such that
A1: B0 = rng f and
A2: for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) by Th15;
take B0 ; ::_thesis: ( B0 c= B & card B0 = weight T )
thus B0 c= B by A1, A2, Th16; ::_thesis: card B0 = weight T
thus card B0 c= weight T by A1, A2, Th17; :: according to XBOOLE_0:def_10 ::_thesis: weight T c= card B0
thus weight T c= card B0 by WAYBEL23:73; ::_thesis: verum
end;
theorem :: TOPGEN_2:18
for T being non empty TopSpace
for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
proof
let T be non empty TopSpace; ::_thesis: for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
let B be Basis of T; ::_thesis: ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
( T is finite-weight or T is infinite-weight ) ;
hence ex B1 being Basis of T st
( B1 c= B & card B1 = weight T ) by Lm4, Lm5; ::_thesis: verum
end;
begin
definition
let X, x0 be set ;
func DiscrWithInfin (X,x0) -> strict TopStruct means :Def5: :: TOPGEN_2:def 5
( the carrier of it = X & the topology of it = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } );
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = X & the topology of b1 = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } & the carrier of b2 = X & the topology of b2 = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } holds
b1 = b2 ;
existence
ex b1 being strict TopStruct st
( the carrier of b1 = X & the topology of b1 = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } )
proof
set O1 = { U where U is Subset of X : not x0 in U } ;
set O2 = { (F `) where F is Subset of X : F is finite } ;
set O = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ;
{ U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } c= bool X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } or a in bool X )
assume a in { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ; ::_thesis: a in bool X
then ( a in { U where U is Subset of X : not x0 in U } or a in { (F `) where F is Subset of X : F is finite } ) by XBOOLE_0:def_3;
then ( ex U being Subset of X st
( a = U & not x0 in U ) or ex F being Subset of X st
( a = F ` & F is finite ) ) ;
hence a in bool X ; ::_thesis: verum
end;
then reconsider O = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } as Subset-Family of X ;
take TopStruct(# X,O #) ; ::_thesis: ( the carrier of TopStruct(# X,O #) = X & the topology of TopStruct(# X,O #) = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } )
thus ( the carrier of TopStruct(# X,O #) = X & the topology of TopStruct(# X,O #) = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ) ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines DiscrWithInfin TOPGEN_2:def_5_:_
for X, x0 being set
for b3 being strict TopStruct holds
( b3 = DiscrWithInfin (X,x0) iff ( the carrier of b3 = X & the topology of b3 = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ) );
registration
let X, x0 be set ;
cluster DiscrWithInfin (X,x0) -> strict TopSpace-like ;
coherence
DiscrWithInfin (X,x0) is TopSpace-like
proof
set O1 = { U where U is Subset of X : not x0 in U } ;
set O2 = { (F `) where F is Subset of X : F is finite } ;
set O = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ;
set T = DiscrWithInfin (X,x0);
A1: the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
A2: the topology of (DiscrWithInfin (X,x0)) = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } by Def5;
({} X) ` = X ;
then X in { (F `) where F is Subset of X : F is finite } ;
hence the carrier of (DiscrWithInfin (X,x0)) in the topology of (DiscrWithInfin (X,x0)) by A1, A2, XBOOLE_0:def_3; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K32(K32( the carrier of (DiscrWithInfin (X,x0)))) holds
( not b1 c= the topology of (DiscrWithInfin (X,x0)) or union b1 in the topology of (DiscrWithInfin (X,x0)) ) ) & ( for b1, b2 being Element of K32( the carrier of (DiscrWithInfin (X,x0))) holds
( not b1 in the topology of (DiscrWithInfin (X,x0)) or not b2 in the topology of (DiscrWithInfin (X,x0)) or b1 /\ b2 in the topology of (DiscrWithInfin (X,x0)) ) ) )
hereby ::_thesis: for b1, b2 being Element of K32( the carrier of (DiscrWithInfin (X,x0))) holds
( not b1 in the topology of (DiscrWithInfin (X,x0)) or not b2 in the topology of (DiscrWithInfin (X,x0)) or b1 /\ b2 in the topology of (DiscrWithInfin (X,x0)) )
let a be Subset-Family of (DiscrWithInfin (X,x0)); ::_thesis: ( a c= the topology of (DiscrWithInfin (X,x0)) implies union b1 in the topology of (DiscrWithInfin (X,x0)) )
assume A3: a c= the topology of (DiscrWithInfin (X,x0)) ; ::_thesis: union b1 in the topology of (DiscrWithInfin (X,x0))
percases ( not a c= { U where U is Subset of X : not x0 in U } or a c= { U where U is Subset of X : not x0 in U } ) ;
suppose not a c= { U where U is Subset of X : not x0 in U } ; ::_thesis: union b1 in the topology of (DiscrWithInfin (X,x0))
then consider b being set such that
A4: b in a and
A5: not b in { U where U is Subset of X : not x0 in U } by TARSKI:def_3;
b in { (F `) where F is Subset of X : F is finite } by A2, A3, A4, A5, XBOOLE_0:def_3;
then A6: ex F being Subset of X st
( b = F ` & F is finite ) ;
A7: ((union a) `) ` = union a ;
b c= union a by A4, ZFMISC_1:74;
then (union a) ` is finite by A1, A6, FINSET_1:1, SUBSET_1:17;
then union a in { (F `) where F is Subset of X : F is finite } by A1, A7;
hence union a in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA8: a c= { U where U is Subset of X : not x0 in U } ; ::_thesis: union b1 in the topology of (DiscrWithInfin (X,x0))
now__::_thesis:_not_x0_in_union_a
assume x0 in union a ; ::_thesis: contradiction
then consider b being set such that
A9: x0 in b and
A10: b in a by TARSKI:def_4;
b in { U where U is Subset of X : not x0 in U } by A8, A10;
then ex U being Subset of X st
( b = U & not x0 in U ) ;
hence contradiction by A9; ::_thesis: verum
end;
then union a in { U where U is Subset of X : not x0 in U } by A1;
hence union a in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let a, b be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( not a in the topology of (DiscrWithInfin (X,x0)) or not b in the topology of (DiscrWithInfin (X,x0)) or a /\ b in the topology of (DiscrWithInfin (X,x0)) )
assume that
A11: a in the topology of (DiscrWithInfin (X,x0)) and
A12: b in the topology of (DiscrWithInfin (X,x0)) ; ::_thesis: a /\ b in the topology of (DiscrWithInfin (X,x0))
percases ( ( a in { (F `) where F is Subset of X : F is finite } & b in { (F `) where F is Subset of X : F is finite } ) or a in { U where U is Subset of X : not x0 in U } or b in { U where U is Subset of X : not x0 in U } ) by A2, A11, A12, XBOOLE_0:def_3;
supposeA13: ( a in { (F `) where F is Subset of X : F is finite } & b in { (F `) where F is Subset of X : F is finite } ) ; ::_thesis: a /\ b in the topology of (DiscrWithInfin (X,x0))
then consider F2 being Subset of X such that
A14: b = F2 ` and
A15: F2 is finite ;
consider F1 being Subset of X such that
A16: a = F1 ` and
A17: F1 is finite by A13;
a /\ b = (F1 \/ F2) ` by A16, A14, XBOOLE_1:53;
then a /\ b in { (F `) where F is Subset of X : F is finite } by A17, A15;
hence a /\ b in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( a in { U where U is Subset of X : not x0 in U } or b in { U where U is Subset of X : not x0 in U } ) ; ::_thesis: a /\ b in the topology of (DiscrWithInfin (X,x0))
then ( ex U being Subset of X st
( a = U & not x0 in U ) or ex U being Subset of X st
( b = U & not x0 in U ) ) ;
then not x0 in a /\ b by XBOOLE_0:def_4;
then a /\ b in { U where U is Subset of X : not x0 in U } by A1;
hence a /\ b in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
registration
let X be non empty set ;
let x0 be set ;
cluster DiscrWithInfin (X,x0) -> non empty strict ;
coherence
not DiscrWithInfin (X,x0) is empty by Def5;
end;
theorem Th19: :: TOPGEN_2:19
for X, x0 being set
for A being Subset of (DiscrWithInfin (X,x0)) holds
( A is open iff ( not x0 in A or A ` is finite ) )
proof
let X, x0 be set ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) holds
( A is open iff ( not x0 in A or A ` is finite ) )
set T = DiscrWithInfin (X,x0);
set O1 = { U where U is Subset of X : not x0 in U } ;
set O2 = { (F `) where F is Subset of X : F is finite } ;
let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A is open iff ( not x0 in A or A ` is finite ) )
A1: the topology of (DiscrWithInfin (X,x0)) = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } by Def5;
A2: the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
thus ( not A is open or not x0 in A or A ` is finite ) ::_thesis: ( ( not x0 in A or A ` is finite ) implies A is open )
proof
assume A in the topology of (DiscrWithInfin (X,x0)) ; :: according to PRE_TOPC:def_2 ::_thesis: ( not x0 in A or A ` is finite )
then ( A in { U where U is Subset of X : not x0 in U } or A in { (F `) where F is Subset of X : F is finite } ) by A1, XBOOLE_0:def_3;
then ( ex U being Subset of X st
( A = U & not x0 in U ) or ex F being Subset of X st
( A = F ` & F is finite ) ) ;
hence ( not x0 in A or A ` is finite ) by A2; ::_thesis: verum
end;
assume ( not x0 in A or A ` is finite ) ; ::_thesis: A is open
then ( A in { U where U is Subset of X : not x0 in U } or (A `) ` in { (F `) where F is Subset of X : F is finite } ) by A2;
hence A in the topology of (DiscrWithInfin (X,x0)) by A1, XBOOLE_0:def_3; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
theorem Th20: :: TOPGEN_2:20
for X, x0 being set
for A being Subset of (DiscrWithInfin (X,x0)) holds
( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) )
proof
let X, x0 be set ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) holds
( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) )
set T = DiscrWithInfin (X,x0);
let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) )
( A is closed iff A ` is open ) by TOPS_1:3;
then A1: ( A is closed iff ( not x0 in A ` or (A `) ` is finite ) ) by Th19;
the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
hence ( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) ) by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: TOPGEN_2:21
for X, x0, x being set st x in X holds
{x} is closed Subset of (DiscrWithInfin (X,x0))
proof
let X, x0, x be set ; ::_thesis: ( x in X implies {x} is closed Subset of (DiscrWithInfin (X,x0)) )
set T = DiscrWithInfin (X,x0);
the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
hence ( x in X implies {x} is closed Subset of (DiscrWithInfin (X,x0)) ) by Th20, ZFMISC_1:31; ::_thesis: verum
end;
theorem Th22: :: TOPGEN_2:22
for X, x0, x being set st x in X & x <> x0 holds
{x} is open Subset of (DiscrWithInfin (X,x0))
proof
let X, x0, x be set ; ::_thesis: ( x in X & x <> x0 implies {x} is open Subset of (DiscrWithInfin (X,x0)) )
set T = DiscrWithInfin (X,x0);
assume that
A1: x in X and
A2: x <> x0 ; ::_thesis: {x} is open Subset of (DiscrWithInfin (X,x0))
A3: the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
not x0 in {x} by A2, TARSKI:def_1;
hence {x} is open Subset of (DiscrWithInfin (X,x0)) by A3, A1, Th19, ZFMISC_1:31; ::_thesis: verum
end;
theorem :: TOPGEN_2:23
for X, x0 being set st X is infinite holds
for U being Subset of (DiscrWithInfin (X,x0)) st U = {x0} holds
not U is open
proof
let X, x0 be set ; ::_thesis: ( X is infinite implies for U being Subset of (DiscrWithInfin (X,x0)) st U = {x0} holds
not U is open )
set T = DiscrWithInfin (X,x0);
assume A1: X is infinite ; ::_thesis: for U being Subset of (DiscrWithInfin (X,x0)) st U = {x0} holds
not U is open
let U be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( U = {x0} implies not U is open )
assume A2: U = {x0} ; ::_thesis: not U is open
the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
then X = (U `) \/ {x0} by A2, XBOOLE_1:45;
then A3: U ` is infinite by A1;
x0 in U by A2, TARSKI:def_1;
hence not U is open by A3, Th19; ::_thesis: verum
end;
theorem Th24: :: TOPGEN_2:24
for X, x0 being set
for A being Subset of (DiscrWithInfin (X,x0)) st A is finite holds
Cl A = A
proof
let X, x0 be set ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) st A is finite holds
Cl A = A
let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A is finite implies Cl A = A )
assume A is finite ; ::_thesis: Cl A = A
then A is closed by Th20;
hence Cl A = A by PRE_TOPC:22; ::_thesis: verum
end;
theorem Th25: :: TOPGEN_2:25
for T being non empty TopSpace
for A being Subset of T st not A is closed holds
for a being Point of T st A \/ {a} is closed holds
Cl A = A \/ {a}
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T st not A is closed holds
for a being Point of T st A \/ {a} is closed holds
Cl A = A \/ {a}
let A be Subset of T; ::_thesis: ( not A is closed implies for a being Point of T st A \/ {a} is closed holds
Cl A = A \/ {a} )
assume A1: not A is closed ; ::_thesis: for a being Point of T st A \/ {a} is closed holds
Cl A = A \/ {a}
A2: A c= Cl A by PRE_TOPC:18;
let a be Point of T; ::_thesis: ( A \/ {a} is closed implies Cl A = A \/ {a} )
assume A \/ {a} is closed ; ::_thesis: Cl A = A \/ {a}
then A3: Cl (A \/ {a}) = A \/ {a} by PRE_TOPC:22;
Cl A c= Cl (A \/ {a}) by PRE_TOPC:19, XBOOLE_1:7;
hence Cl A = A \/ {a} by A1, A2, A3, ZFMISC_1:138; ::_thesis: verum
end;
theorem Th26: :: TOPGEN_2:26
for X, x0 being set st x0 in X holds
for A being Subset of (DiscrWithInfin (X,x0)) st A is infinite holds
Cl A = A \/ {x0}
proof
let X, x0 be set ; ::_thesis: ( x0 in X implies for A being Subset of (DiscrWithInfin (X,x0)) st A is infinite holds
Cl A = A \/ {x0} )
assume A1: x0 in X ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) st A is infinite holds
Cl A = A \/ {x0}
set T = DiscrWithInfin (X,x0);
reconsider T = DiscrWithInfin (X,x0) as non empty TopSpace by A1;
reconsider x = x0 as Point of T by A1, Def5;
let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A is infinite implies Cl A = A \/ {x0} )
reconsider B = {x} as Subset of T ;
reconsider A9 = A as Subset of T ;
x0 in {x0} by TARSKI:def_1;
then x0 in A9 \/ B by XBOOLE_0:def_3;
then A9 \/ B is closed by Th20;
then A2: Cl (A9 \/ B) = A9 \/ B by PRE_TOPC:22;
assume A is infinite ; ::_thesis: Cl A = A \/ {x0}
then ( not A9 is closed or x0 in A ) by A1, Th20;
hence Cl A = A \/ {x0} by A2, Th25, ZFMISC_1:40; ::_thesis: verum
end;
theorem :: TOPGEN_2:27
for X, x0 being set
for A being Subset of (DiscrWithInfin (X,x0)) st A ` is finite holds
Int A = A
proof
let X, x0 be set ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) st A ` is finite holds
Int A = A
let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A ` is finite implies Int A = A )
assume A ` is finite ; ::_thesis: Int A = A
then Cl (A `) = A ` by Th24;
hence Int A = (A `) ` by TOPS_1:def_1
.= A ;
::_thesis: verum
end;
theorem :: TOPGEN_2:28
for X, x0 being set st x0 in X holds
for A being Subset of (DiscrWithInfin (X,x0)) st A ` is infinite holds
Int A = A \ {x0}
proof
let X, x0 be set ; ::_thesis: ( x0 in X implies for A being Subset of (DiscrWithInfin (X,x0)) st A ` is infinite holds
Int A = A \ {x0} )
assume A1: x0 in X ; ::_thesis: for A being Subset of (DiscrWithInfin (X,x0)) st A ` is infinite holds
Int A = A \ {x0}
set T = DiscrWithInfin (X,x0);
reconsider T = DiscrWithInfin (X,x0) as non empty TopSpace by A1;
reconsider x = x0 as Point of T by A1, Def5;
let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A ` is infinite implies Int A = A \ {x0} )
reconsider A9 = A as Subset of T ;
assume A ` is infinite ; ::_thesis: Int A = A \ {x0}
then Cl (A `) = (A9 `) \/ {x} by A1, Th26;
hence Int A = ((A9 `) \/ {x}) ` by TOPS_1:def_1
.= ((A9 \ {x}) `) ` by SUBSET_1:14
.= A \ {x0} ;
::_thesis: verum
end;
theorem Th29: :: TOPGEN_2:29
for X, x0 being set ex B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite }
proof
let X, x0 be set ; ::_thesis: ex B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite }
set T = DiscrWithInfin (X,x0);
set B1 = (SmallestPartition X) \ {{x0}};
set B2 = { (F `) where F is Subset of X : F is finite } ;
A1: (SmallestPartition X) \ {{x0}} c= the topology of (DiscrWithInfin (X,x0))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (SmallestPartition X) \ {{x0}} or a in the topology of (DiscrWithInfin (X,x0)) )
assume A2: a in (SmallestPartition X) \ {{x0}} ; ::_thesis: a in the topology of (DiscrWithInfin (X,x0))
then A3: a in SmallestPartition X by ZFMISC_1:56;
then reconsider X = X as non empty set by EQREL_1:32;
SmallestPartition X = { {x} where x is Element of X : verum } by EQREL_1:37;
then A4: ex x being Element of X st a = {x} by A3;
a <> {x0} by A2, ZFMISC_1:56;
then not x0 in a by A4, TARSKI:def_1;
then a is open Subset of (DiscrWithInfin (X,x0)) by A2, Def5, Th19;
hence a in the topology of (DiscrWithInfin (X,x0)) by PRE_TOPC:def_2; ::_thesis: verum
end;
A5: the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
{ (F `) where F is Subset of X : F is finite } c= bool the carrier of (DiscrWithInfin (X,x0))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (F `) where F is Subset of X : F is finite } or a in bool the carrier of (DiscrWithInfin (X,x0)) )
assume a in { (F `) where F is Subset of X : F is finite } ; ::_thesis: a in bool the carrier of (DiscrWithInfin (X,x0))
then ex F being Subset of X st
( a = F ` & F is finite ) ;
hence a in bool the carrier of (DiscrWithInfin (X,x0)) by A5; ::_thesis: verum
end;
then reconsider B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } as Subset-Family of (DiscrWithInfin (X,x0)) by A5, XBOOLE_1:8;
A6: now__::_thesis:_for_A_being_Subset_of_(DiscrWithInfin_(X,x0))_st_A_is_open_holds_
for_p_being_Point_of_(DiscrWithInfin_(X,x0))_st_p_in_A_holds_
ex_a_being_Subset_of_(DiscrWithInfin_(X,x0))_st_
(_a_in_B0_&_p_in_a_&_a_c=_A_)
let A be Subset of (DiscrWithInfin (X,x0)); ::_thesis: ( A is open implies for p being Point of (DiscrWithInfin (X,x0)) st p in A holds
ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A ) )
assume A is open ; ::_thesis: for p being Point of (DiscrWithInfin (X,x0)) st p in A holds
ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A )
then A7: ( not x0 in A or A ` is finite ) by Th19;
let p be Point of (DiscrWithInfin (X,x0)); ::_thesis: ( p in A implies ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A ) )
assume A8: p in A ; ::_thesis: ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A )
reconsider X9 = X as non empty set by A8, Def5;
reconsider p9 = p as Element of X9 by Def5;
SmallestPartition X = { {x} where x is Element of X9 : verum } by EQREL_1:37;
then A9: {p9} in SmallestPartition X ;
( {p} <> {x0} or (A `) ` in { (F `) where F is Subset of X : F is finite } ) by A5, A8, A7, ZFMISC_1:3;
then ( not {p} in {{x0}} or A in { (F `) where F is Subset of X : F is finite } ) by TARSKI:def_1;
then ( {p} in (SmallestPartition X) \ {{x0}} or A in { (F `) where F is Subset of X : F is finite } ) by A9, XBOOLE_0:def_5;
then ( ( {p} in B0 & p in {p} & {p} c= A ) or ( A in B0 & A c= A ) ) by A8, XBOOLE_0:def_3, ZFMISC_1:31;
hence ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A ) by A8; ::_thesis: verum
end;
{ (F `) where F is Subset of X : F is finite } c= the topology of (DiscrWithInfin (X,x0))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (F `) where F is Subset of X : F is finite } or a in the topology of (DiscrWithInfin (X,x0)) )
assume a in { (F `) where F is Subset of X : F is finite } ; ::_thesis: a in the topology of (DiscrWithInfin (X,x0))
then consider F being Subset of X such that
A10: a = F ` and
A11: F is finite ;
(F `) ` is finite by A11;
then a is open Subset of (DiscrWithInfin (X,x0)) by A5, A10, Th19;
hence a in the topology of (DiscrWithInfin (X,x0)) by PRE_TOPC:def_2; ::_thesis: verum
end;
then reconsider B0 = B0 as Basis of (DiscrWithInfin (X,x0)) by A1, A6, XBOOLE_1:8, YELLOW_9:32;
take B0 ; ::_thesis: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite }
thus B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } ; ::_thesis: verum
end;
theorem :: TOPGEN_2:30
for X being infinite set holds card (Fin X) = card X
proof
deffunc H1( set ) -> set = proj2 $1;
let X be infinite set ; ::_thesis: card (Fin X) = card X
set FX = Fin X;
consider f being Function such that
A1: ( dom f = X * & ( for a being set st a in X * holds
f . a = H1(a) ) ) from FUNCT_1:sch_3();
Fin X c= rng f
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Fin X or a in rng f )
assume A2: a in Fin X ; ::_thesis: a in rng f
then a is finite by FINSUB_1:def_5;
then consider p being FinSequence such that
A3: a = rng p by FINSEQ_1:52;
a c= X by A2, FINSUB_1:def_5;
then p is FinSequence of X by A3, FINSEQ_1:def_4;
then A4: p in X * by FINSEQ_1:def_11;
then f . p in rng f by A1, FUNCT_1:def_3;
hence a in rng f by A1, A3, A4; ::_thesis: verum
end;
then card (Fin X) c= card (X *) by A1, CARD_1:12;
hence card (Fin X) c= card X by CARD_4:24; :: according to XBOOLE_0:def_10 ::_thesis: card X c= card (Fin X)
set SX = SmallestPartition X;
SmallestPartition X c= Fin X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SmallestPartition X or a in Fin X )
assume a in SmallestPartition X ; ::_thesis: a in Fin X
then a in { {x} where x is Element of X : verum } by EQREL_1:37;
then ex x being Element of X st a = {x} ;
hence a in Fin X by FINSUB_1:def_5; ::_thesis: verum
end;
then card (SmallestPartition X) c= card (Fin X) by CARD_1:11;
hence card X c= card (Fin X) by Th12; ::_thesis: verum
end;
theorem Th31: :: TOPGEN_2:31
for X being infinite set holds card { (F `) where F is Subset of X : F is finite } = card X
proof
let X be infinite set ; ::_thesis: card { (F `) where F is Subset of X : F is finite } = card X
set FX = { (F `) where F is Subset of X : F is finite } ;
deffunc H1( set ) -> Element of K32(X) = X \ (proj2 $1);
consider f being Function such that
A1: ( dom f = X * & ( for a being set st a in X * holds
f . a = H1(a) ) ) from FUNCT_1:sch_3();
{ (F `) where F is Subset of X : F is finite } c= rng f
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (F `) where F is Subset of X : F is finite } or a in rng f )
assume a in { (F `) where F is Subset of X : F is finite } ; ::_thesis: a in rng f
then consider F being Subset of X such that
A2: a = F ` and
A3: F is finite ;
consider p being FinSequence such that
A4: F = rng p by A3, FINSEQ_1:52;
p is FinSequence of X by A4, FINSEQ_1:def_4;
then A5: p in X * by FINSEQ_1:def_11;
then f . p in rng f by A1, FUNCT_1:def_3;
hence a in rng f by A1, A2, A4, A5; ::_thesis: verum
end;
then card { (F `) where F is Subset of X : F is finite } c= card (X *) by A1, CARD_1:12;
hence card { (F `) where F is Subset of X : F is finite } c= card X by CARD_4:24; :: according to XBOOLE_0:def_10 ::_thesis: card X c= card { (F `) where F is Subset of X : F is finite }
deffunc H2( set ) -> Element of K32(X) = X \ {$1};
consider f being Function such that
A6: ( dom f = X & ( for a being set st a in X holds
f . a = H2(a) ) ) from FUNCT_1:sch_3();
A7: rng f c= { (F `) where F is Subset of X : F is finite }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng f or a in { (F `) where F is Subset of X : F is finite } )
assume a in rng f ; ::_thesis: a in { (F `) where F is Subset of X : F is finite }
then consider b being set such that
A8: b in dom f and
A9: a = f . b by FUNCT_1:def_3;
reconsider b = b as Element of X by A6, A8;
{b} ` in { (F `) where F is Subset of X : F is finite } ;
hence a in { (F `) where F is Subset of X : F is finite } by A6, A9; ::_thesis: verum
end;
f is one-to-one
proof
let a be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not a in proj1 f or not b1 in proj1 f or not f . a = f . b1 or a = b1 )
let b be set ; ::_thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b )
assume that
A10: a in dom f and
A11: b in dom f and
A12: f . a = f . b ; ::_thesis: a = b
reconsider a = a, b = b as Element of X by A6, A10, A11;
{a} ` = f . b by A6, A12
.= {b} ` by A6 ;
then {a} = {b} by SUBSET_1:42;
hence a = b by ZFMISC_1:3; ::_thesis: verum
end;
hence card X c= card { (F `) where F is Subset of X : F is finite } by A6, A7, CARD_1:10; ::_thesis: verum
end;
theorem Th32: :: TOPGEN_2:32
for X being infinite set
for x0 being set
for B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } holds
card B0 = card X
proof
let X be infinite set ; ::_thesis: for x0 being set
for B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } holds
card B0 = card X
let x0 be set ; ::_thesis: for B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } holds
card B0 = card X
set T = DiscrWithInfin (X,x0);
let B0 be Basis of (DiscrWithInfin (X,x0)); ::_thesis: ( B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } implies card B0 = card X )
set SX = SmallestPartition X;
set FX = { (F `) where F is Subset of X : F is finite } ;
assume A1: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } ; ::_thesis: card B0 = card X
A2: card (SmallestPartition X) = card X by Th12;
A3: card {{x0}} = 1 by CARD_1:30;
A4: 1 in card X by CARD_3:86;
then (card X) +` 1 = card X by CARD_2:76;
then A5: card ((SmallestPartition X) \ {{x0}}) = card X by A3, A2, A4, CARD_2:98;
card { (F `) where F is Subset of X : F is finite } = card X by Th31;
then card B0 c= (card X) +` (card X) by A1, A5, CARD_2:34;
hence card B0 c= card X by CARD_2:75; :: according to XBOOLE_0:def_10 ::_thesis: card X c= card B0
thus card X c= card B0 by A1, A5, CARD_1:11, XBOOLE_1:7; ::_thesis: verum
end;
theorem Th33: :: TOPGEN_2:33
for X being infinite set
for x0 being set
for B being Basis of (DiscrWithInfin (X,x0)) holds card X c= card B
proof
let X be infinite set ; ::_thesis: for x0 being set
for B being Basis of (DiscrWithInfin (X,x0)) holds card X c= card B
let x0 be set ; ::_thesis: for B being Basis of (DiscrWithInfin (X,x0)) holds card X c= card B
set T = DiscrWithInfin (X,x0);
set SX = SmallestPartition X;
A1: card {{x0}} = 1 by CARD_1:30;
A2: card (SmallestPartition X) = card X by Th12;
let B be Basis of (DiscrWithInfin (X,x0)); ::_thesis: card X c= card B
A3: the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
A4: SmallestPartition X = { {x} where x is Element of X : verum } by EQREL_1:37;
A5: (SmallestPartition X) \ {{x0}} c= B
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (SmallestPartition X) \ {{x0}} or a in B )
assume A6: a in (SmallestPartition X) \ {{x0}} ; ::_thesis: a in B
then not a in {{x0}} by XBOOLE_0:def_5;
then A7: a <> {x0} by TARSKI:def_1;
a in SmallestPartition X by A6, XBOOLE_0:def_5;
then ex x being Element of X st a = {x} by A4;
then consider x being Element of (DiscrWithInfin (X,x0)) such that
A8: a = {x} and
A9: x <> x0 by A3, A7;
A10: x in a by A8, TARSKI:def_1;
a is open Subset of (DiscrWithInfin (X,x0)) by A3, A8, A9, Th22;
then consider U being Subset of (DiscrWithInfin (X,x0)) such that
A11: U in B and
A12: x in U and
A13: U c= a by A10, YELLOW_9:31;
a c= U by A8, A12, ZFMISC_1:31;
hence a in B by A11, A13, XBOOLE_0:def_10; ::_thesis: verum
end;
A14: 1 in card X by CARD_3:86;
then (card X) +` 1 = card X by CARD_2:76;
then card ((SmallestPartition X) \ {{x0}}) = card X by A1, A2, A14, CARD_2:98;
hence card X c= card B by A5, CARD_1:11; ::_thesis: verum
end;
theorem :: TOPGEN_2:34
for X being infinite set
for x0 being set holds weight (DiscrWithInfin (X,x0)) = card X
proof
let X be infinite set ; ::_thesis: for x0 being set holds weight (DiscrWithInfin (X,x0)) = card X
let x0 be set ; ::_thesis: weight (DiscrWithInfin (X,x0)) = card X
set T = DiscrWithInfin (X,x0);
consider B0 being Basis of (DiscrWithInfin (X,x0)) such that
A1: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } by Th29;
card B0 = card X by A1, Th32;
hence weight (DiscrWithInfin (X,x0)) c= card X by WAYBEL23:73; :: according to XBOOLE_0:def_10 ::_thesis: card X c= weight (DiscrWithInfin (X,x0))
ex B being Basis of (DiscrWithInfin (X,x0)) st card B = weight (DiscrWithInfin (X,x0)) by WAYBEL23:74;
hence card X c= weight (DiscrWithInfin (X,x0)) by Th33; ::_thesis: verum
end;
theorem :: TOPGEN_2:35
for X being non empty set
for x0 being set ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum }
proof
let X be non empty set ; ::_thesis: for x0 being set ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum }
let x0 be set ; ::_thesis: ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum }
set T = DiscrWithInfin (X,x0);
set SX = SmallestPartition X;
set FX = { (F `) where F is Subset of X : F is finite } ;
set AX = { ({x} `) where x is Element of X : verum } ;
reconsider SX = SmallestPartition X as Subset-Family of (DiscrWithInfin (X,x0)) by Def5;
{ ({x} `) where x is Element of X : verum } c= bool X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ({x} `) where x is Element of X : verum } or a in bool X )
assume a in { ({x} `) where x is Element of X : verum } ; ::_thesis: a in bool X
then ex x being Element of X st a = {x} ` ;
hence a in bool X ; ::_thesis: verum
end;
then reconsider AX = { ({x} `) where x is Element of X : verum } as Subset-Family of (DiscrWithInfin (X,x0)) by Def5;
reconsider pB = (SX \ {{x0}}) \/ AX as Subset-Family of (DiscrWithInfin (X,x0)) ;
consider B0 being Basis of (DiscrWithInfin (X,x0)) such that
A1: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } by Th29;
A2: the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
A3: { (F `) where F is Subset of X : F is finite } c= FinMeetCl pB
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (F `) where F is Subset of X : F is finite } or a in FinMeetCl pB )
assume a in { (F `) where F is Subset of X : F is finite } ; ::_thesis: a in FinMeetCl pB
then consider F being Subset of (DiscrWithInfin (X,x0)) such that
A4: a = F ` and
A5: F is finite by A2;
set SF = SmallestPartition F;
bool F c= bool X by A2, ZFMISC_1:67;
then reconsider SF = SmallestPartition F as Subset-Family of (DiscrWithInfin (X,x0)) by A2, XBOOLE_1:1;
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: a in FinMeetCl pB
hence a in FinMeetCl pB by A4, CANTOR_1:8; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: a in FinMeetCl pB
then reconsider F = F as non empty Subset of (DiscrWithInfin (X,x0)) ;
SF is a_partition of F ;
then reconsider SF = SF as non empty Subset-Family of (DiscrWithInfin (X,x0)) ;
A6: COMPLEMENT SF c= pB
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in COMPLEMENT SF or a in pB )
assume A7: a in COMPLEMENT SF ; ::_thesis: a in pB
then reconsider a = a as Subset of (DiscrWithInfin (X,x0)) ;
a ` in SF by A7, SETFAM_1:def_7;
then a ` in { {b} where b is Element of F : verum } by EQREL_1:37;
then consider b being Element of F such that
A8: a ` = {b} ;
reconsider b = b as Element of X by Def5;
{b} ` in AX ;
hence a in pB by A2, A8, XBOOLE_0:def_3; ::_thesis: verum
end;
F = union SF by EQREL_1:def_4;
then A9: a = meet (COMPLEMENT SF) by A4, TOPS_2:6;
COMPLEMENT SF is finite by A5, TOPS_2:8;
then Intersect (COMPLEMENT SF) in FinMeetCl pB by A6, CANTOR_1:def_3;
hence a in FinMeetCl pB by A9, SETFAM_1:def_9; ::_thesis: verum
end;
end;
end;
A10: pB c= FinMeetCl pB by CANTOR_1:4;
A11: B0 c= FinMeetCl pB
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B0 or a in FinMeetCl pB )
assume a in B0 ; ::_thesis: a in FinMeetCl pB
then ( a in SX \ {{x0}} or a in { (F `) where F is Subset of X : F is finite } ) by A1, XBOOLE_0:def_3;
then ( a in pB or a in { (F `) where F is Subset of X : F is finite } ) by XBOOLE_0:def_3;
hence a in FinMeetCl pB by A10, A3; ::_thesis: verum
end;
A12: B0 c= the topology of (DiscrWithInfin (X,x0)) by TOPS_2:64;
AX c= { (F `) where F is Subset of X : F is finite }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in AX or a in { (F `) where F is Subset of X : F is finite } )
assume a in AX ; ::_thesis: a in { (F `) where F is Subset of X : F is finite }
then ex x being Element of X st a = {x} ` ;
hence a in { (F `) where F is Subset of X : F is finite } ; ::_thesis: verum
end;
then pB c= B0 by A1, XBOOLE_1:9;
then pB c= the topology of (DiscrWithInfin (X,x0)) by A12, XBOOLE_1:1;
then FinMeetCl pB c= FinMeetCl the topology of (DiscrWithInfin (X,x0)) by CANTOR_1:14;
then FinMeetCl pB c= the topology of (DiscrWithInfin (X,x0)) by CANTOR_1:5;
then FinMeetCl pB is Basis of (DiscrWithInfin (X,x0)) by A11, WAYBEL19:22;
then pB is prebasis of (DiscrWithInfin (X,x0)) by YELLOW_9:23;
hence ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum } ; ::_thesis: verum
end;
begin
theorem :: TOPGEN_2:36
for T being TopSpace
for F being Subset-Family of T
for I being non empty Subset-Family of F st ( for G being set st G in I holds
F \ G is finite ) holds
Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } )
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T
for I being non empty Subset-Family of F st ( for G being set st G in I holds
F \ G is finite ) holds
Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } )
let F be Subset-Family of T; ::_thesis: for I being non empty Subset-Family of F st ( for G being set st G in I holds
F \ G is finite ) holds
Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } )
let I be non empty Subset-Family of F; ::_thesis: ( ( for G being set st G in I holds
F \ G is finite ) implies Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) )
set G0 = the Element of I;
reconsider G0 = the Element of I as Subset-Family of T by XBOOLE_1:1;
set Z = { (Cl (union G)) where G is Subset-Family of T : G in I } ;
A1: Cl (union G0) in { (Cl (union G)) where G is Subset-Family of T : G in I } ;
then reconsider Z9 = { (Cl (union G)) where G is Subset-Family of T : G in I } as non empty set ;
assume A2: for G being set st G in I holds
F \ G is finite ; ::_thesis: Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } )
thus Cl (union F) c= (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) :: according to XBOOLE_0:def_10 ::_thesis: (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) c= Cl (union F)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl (union F) or a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) )
assume that
A3: a in Cl (union F) and
A4: not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) ; ::_thesis: contradiction
reconsider a = a as Point of T by A3;
not a in meet Z9 by A4, XBOOLE_0:def_3;
then consider b being set such that
A5: b in { (Cl (union G)) where G is Subset-Family of T : G in I } and
A6: not a in b by SETFAM_1:def_1;
consider G being Subset-Family of T such that
A7: b = Cl (union G) and
A8: G in I by A5;
A9: not T is empty by A3;
then clf (F \ G) c= clf F by PCOMPS_1:14, XBOOLE_1:36;
then A10: union (clf (F \ G)) c= union (clf F) by ZFMISC_1:77;
F = G \/ (F \ G) by A8, XBOOLE_1:45;
then union F = (union G) \/ (union (F \ G)) by ZFMISC_1:78;
then Cl (union F) = (Cl (union G)) \/ (Cl (union (F \ G))) by PRE_TOPC:20;
then a in Cl (union (F \ G)) by A3, A6, A7, XBOOLE_0:def_3;
then a in union (clf (F \ G)) by A2, A8, A9, PCOMPS_1:16;
hence contradiction by A4, A10, XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) or a in Cl (union F) )
assume A11: a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) ; ::_thesis: a in Cl (union F)
percases ( a in union (clf F) or a in meet Z9 ) by A11, XBOOLE_0:def_3;
suppose a in union (clf F) ; ::_thesis: a in Cl (union F)
then consider b being set such that
A12: a in b and
A13: b in clf F by TARSKI:def_4;
ex W being Subset of T st
( b = Cl W & W in F ) by A13, PCOMPS_1:def_2;
then b c= Cl (union F) by PRE_TOPC:19, ZFMISC_1:74;
hence a in Cl (union F) by A12; ::_thesis: verum
end;
supposeA14: a in meet Z9 ; ::_thesis: a in Cl (union F)
union G0 c= union F by ZFMISC_1:77;
then A15: Cl (union G0) c= Cl (union F) by PRE_TOPC:19;
a in Cl (union G0) by A1, A14, SETFAM_1:def_1;
hence a in Cl (union F) by A15; ::_thesis: verum
end;
end;
end;
theorem :: TOPGEN_2:37
for T being TopSpace
for F being Subset-Family of T holds Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } )
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } )
let F be Subset-Family of T; ::_thesis: Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } )
set Z = { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ;
F \ F = {} by XBOOLE_1:37;
then A1: Cl (union F) in { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ;
then reconsider Z9 = { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } as non empty set ;
thus Cl (union F) c= (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) :: according to XBOOLE_0:def_10 ::_thesis: (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) c= Cl (union F)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl (union F) or a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) )
assume that
A2: a in Cl (union F) and
A3: not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) ; ::_thesis: contradiction
reconsider a = a as Point of T by A2;
not a in meet Z9 by A3, XBOOLE_0:def_3;
then consider b being set such that
A4: b in { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } and
A5: not a in b by SETFAM_1:def_1;
consider G being Subset-Family of T such that
A6: b = Cl (union G) and
A7: G c= F and
A8: F \ G is finite by A4;
A9: not T is empty by A2;
then clf (F \ G) c= clf F by PCOMPS_1:14, XBOOLE_1:36;
then A10: union (clf (F \ G)) c= union (clf F) by ZFMISC_1:77;
F = G \/ (F \ G) by A7, XBOOLE_1:45;
then union F = (union G) \/ (union (F \ G)) by ZFMISC_1:78;
then Cl (union F) = (Cl (union G)) \/ (Cl (union (F \ G))) by PRE_TOPC:20;
then a in Cl (union (F \ G)) by A2, A5, A6, XBOOLE_0:def_3;
then a in union (clf (F \ G)) by A8, A9, PCOMPS_1:16;
hence contradiction by A3, A10, XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) or a in Cl (union F) )
assume A11: a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) ; ::_thesis: a in Cl (union F)
percases ( a in union (clf F) or a in meet Z9 ) by A11, XBOOLE_0:def_3;
suppose a in union (clf F) ; ::_thesis: a in Cl (union F)
then consider b being set such that
A12: a in b and
A13: b in clf F by TARSKI:def_4;
ex W being Subset of T st
( b = Cl W & W in F ) by A13, PCOMPS_1:def_2;
then b c= Cl (union F) by PRE_TOPC:19, ZFMISC_1:74;
hence a in Cl (union F) by A12; ::_thesis: verum
end;
suppose a in meet Z9 ; ::_thesis: a in Cl (union F)
hence a in Cl (union F) by A1, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
theorem :: TOPGEN_2:38
for X being set
for O being Subset-Family of (bool X) st ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopSpace ) holds
ex B being Subset-Family of X st
( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
proof
let X be set ; ::_thesis: for O being Subset-Family of (bool X) st ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopSpace ) holds
ex B being Subset-Family of X st
( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
let O be Subset-Family of (bool X); ::_thesis: ( ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopSpace ) implies ex B being Subset-Family of X st
( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) ) )
assume A1: for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopSpace ; ::_thesis: ex B being Subset-Family of X st
( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
reconsider B = Intersect O as Subset-Family of X ;
set T = TopStruct(# X,B #);
take B ; ::_thesis: ( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
thus B = Intersect O ; ::_thesis: ( TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
A2: TopStruct(# X,B #) is TopSpace-like
proof
now__::_thesis:_(_the_carrier_of_TopStruct(#_X,B_#)_in_bool_the_carrier_of_TopStruct(#_X,B_#)_&_(_for_a_being_set_st_a_in_O_holds_
the_carrier_of_TopStruct(#_X,B_#)_in_a_)_)
thus the carrier of TopStruct(# X,B #) in bool the carrier of TopStruct(# X,B #) by ZFMISC_1:def_1; ::_thesis: for a being set st a in O holds
the carrier of TopStruct(# X,B #) in a
let a be set ; ::_thesis: ( a in O implies the carrier of TopStruct(# X,B #) in a )
assume A3: a in O ; ::_thesis: the carrier of TopStruct(# X,B #) in a
then reconsider o = a as Subset-Family of X ;
TopStruct(# X,o #) is TopSpace by A1, A3;
hence the carrier of TopStruct(# X,B #) in a by PRE_TOPC:def_1; ::_thesis: verum
end;
hence the carrier of TopStruct(# X,B #) in the topology of TopStruct(# X,B #) by SETFAM_1:43; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K32(K32( the carrier of TopStruct(# X,B #))) holds
( not b1 c= the topology of TopStruct(# X,B #) or union b1 in the topology of TopStruct(# X,B #) ) ) & ( for b1, b2 being Element of K32( the carrier of TopStruct(# X,B #)) holds
( not b1 in the topology of TopStruct(# X,B #) or not b2 in the topology of TopStruct(# X,B #) or b1 /\ b2 in the topology of TopStruct(# X,B #) ) ) )
hereby ::_thesis: for b1, b2 being Element of K32( the carrier of TopStruct(# X,B #)) holds
( not b1 in the topology of TopStruct(# X,B #) or not b2 in the topology of TopStruct(# X,B #) or b1 /\ b2 in the topology of TopStruct(# X,B #) )
let a be Subset-Family of TopStruct(# X,B #); ::_thesis: ( a c= the topology of TopStruct(# X,B #) implies union a in the topology of TopStruct(# X,B #) )
assume A4: a c= the topology of TopStruct(# X,B #) ; ::_thesis: union a in the topology of TopStruct(# X,B #)
now__::_thesis:_for_b_being_set_st_b_in_O_holds_
union_a_in_b
let b be set ; ::_thesis: ( b in O implies union a in b )
assume A5: b in O ; ::_thesis: union a in b
then reconsider o = b as Subset-Family of X ;
B c= b by A5, MSSUBFAM:2;
then A6: a c= o by A4, XBOOLE_1:1;
TopStruct(# X,o #) is TopSpace by A1, A5;
hence union a in b by A6, PRE_TOPC:def_1; ::_thesis: verum
end;
hence union a in the topology of TopStruct(# X,B #) by SETFAM_1:43; ::_thesis: verum
end;
let a, b be Subset of TopStruct(# X,B #); ::_thesis: ( not a in the topology of TopStruct(# X,B #) or not b in the topology of TopStruct(# X,B #) or a /\ b in the topology of TopStruct(# X,B #) )
assume that
A7: a in the topology of TopStruct(# X,B #) and
A8: b in the topology of TopStruct(# X,B #) ; ::_thesis: a /\ b in the topology of TopStruct(# X,B #)
now__::_thesis:_for_c_being_set_st_c_in_O_holds_
a_/\_b_in_c
let c be set ; ::_thesis: ( c in O implies a /\ b in c )
assume A9: c in O ; ::_thesis: a /\ b in c
then reconsider o = c as Subset-Family of X ;
A10: b in o by A8, A9, SETFAM_1:43;
A11: TopStruct(# X,o #) is TopSpace by A1, A9;
a in o by A7, A9, SETFAM_1:43;
hence a /\ b in c by A10, A11, PRE_TOPC:def_1; ::_thesis: verum
end;
hence a /\ b in the topology of TopStruct(# X,B #) by SETFAM_1:43; ::_thesis: verum
end;
hence TopStruct(# X,B #) is TopSpace ; ::_thesis: ( ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
thus for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ::_thesis: for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T
proof
let o be Subset-Family of X; ::_thesis: ( o in O implies TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) )
assume A12: o in O ; ::_thesis: TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #)
reconsider S = TopStruct(# X,o #) as TopSpace by A1, A12;
Intersect O c= o by A12, MSSUBFAM:2;
then S is TopExtension of TopStruct(# X,B #) by YELLOW_9:def_5;
hence TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ; ::_thesis: verum
end;
reconsider TT = TopStruct(# X,B #) as TopSpace by A2;
let T9 be TopSpace; ::_thesis: ( the carrier of T9 = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T9 ) implies TopStruct(# X,B #) is TopExtension of T9 )
assume that
A13: the carrier of T9 = X and
A14: for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T9 ; ::_thesis: TopStruct(# X,B #) is TopExtension of T9
now__::_thesis:_for_a_being_set_st_a_in_O_holds_
the_topology_of_T9_c=_a
let a be set ; ::_thesis: ( a in O implies the topology of T9 c= a )
assume A15: a in O ; ::_thesis: the topology of T9 c= a
then reconsider o = a as Subset-Family of X ;
TopStruct(# X,o #) is TopExtension of T9 by A14, A15;
hence the topology of T9 c= a by YELLOW_9:def_5; ::_thesis: verum
end;
then the topology of T9 c= Intersect O by A13, MSSUBFAM:4;
then TT is TopExtension of T9 by A13, YELLOW_9:def_5;
hence TopStruct(# X,B #) is TopExtension of T9 ; ::_thesis: verum
end;
theorem :: TOPGEN_2:39
for X being set
for O being Subset-Family of (bool X) ex B being Subset-Family of X st
( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
proof
reconsider e = {} (bool {}), tE = {({} {})} as Subset-Family of {} ;
reconsider E = {} (bool (bool {})) as empty Subset-Family of (bool {}) ;
let X be set ; ::_thesis: for O being Subset-Family of (bool X) ex B being Subset-Family of X st
( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
let O be Subset-Family of (bool X); ::_thesis: ex B being Subset-Family of X st
( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
reconsider B = UniCl (FinMeetCl (union O)) as Subset-Family of X ;
take B ; ::_thesis: ( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
thus B = UniCl (FinMeetCl (union O)) ; ::_thesis: ( TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
reconsider dT = TopStruct(# {},tE #) as discrete TopStruct by TDLAT_3:def_1, ZFMISC_1:1;
A1: UniCl tE = {{},{}} by YELLOW_9:11;
A2: {{},{}} = tE by ENUMSET1:29;
A3: FinMeetCl tE = {{},{}} by YELLOW_9:11;
A4: now__::_thesis:_(_X_is_empty_implies_(_(_union_O_=_e_or_union_O_=_tE_)_&_FinMeetCl_(union_E)_=_the_topology_of_dT_&_TopStruct(#_X,B_#)_is_TopSpace_)_)
assume A5: X is empty ; ::_thesis: ( ( union O = e or union O = tE ) & FinMeetCl (union E) = the topology of dT & TopStruct(# X,B #) is TopSpace )
hence A6: ( union O = e or union O = tE ) by ZFMISC_1:1, ZFMISC_1:33; ::_thesis: ( FinMeetCl (union E) = the topology of dT & TopStruct(# X,B #) is TopSpace )
thus FinMeetCl (union E) = the topology of dT by YELLOW_9:17; ::_thesis: TopStruct(# X,B #) is TopSpace
hence TopStruct(# X,B #) is TopSpace by A3, A2, A5, A6, YELLOW_9:11; ::_thesis: verum
end;
hence TopStruct(# X,B #) is TopSpace by CANTOR_1:15; ::_thesis: ( ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
reconsider TT = TopStruct(# X,B #) as TopSpace by A4, CANTOR_1:15;
hereby ::_thesis: for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #)
let o be Subset-Family of X; ::_thesis: ( o in O implies TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) )
set S = TopStruct(# X,o #);
A7: FinMeetCl (union O) c= B by CANTOR_1:1;
assume o in O ; ::_thesis: TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #)
then A8: o c= union O by ZFMISC_1:74;
union O c= FinMeetCl (union O) by CANTOR_1:4;
then o c= FinMeetCl (union O) by A8, XBOOLE_1:1;
then the topology of TopStruct(# X,o #) c= the topology of TT by A7, XBOOLE_1:1;
hence TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) by YELLOW_9:def_5; ::_thesis: verum
end;
let T be TopSpace; ::_thesis: ( the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) implies T is TopExtension of TopStruct(# X,B #) )
assume that
A9: the carrier of T = X and
A10: for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ; ::_thesis: T is TopExtension of TopStruct(# X,B #)
thus the carrier of T = the carrier of TopStruct(# X,B #) by A9; :: according to YELLOW_9:def_5 ::_thesis: the topology of TopStruct(# X,B #) c= the topology of T
A11: ( X <> {} implies not T is empty ) by A9;
now__::_thesis:_for_a_being_set_st_a_in_O_holds_
a_c=_the_topology_of_T
let a be set ; ::_thesis: ( a in O implies a c= the topology of T )
assume A12: a in O ; ::_thesis: a c= the topology of T
then reconsider o = a as Subset-Family of X ;
T is TopExtension of TopStruct(# X,o #) by A10, A12;
hence a c= the topology of T by YELLOW_9:def_5; ::_thesis: verum
end;
then union O c= the topology of T by ZFMISC_1:76;
then FinMeetCl (union O) c= FinMeetCl the topology of T by A9, CANTOR_1:14;
then A13: B c= UniCl (FinMeetCl the topology of T) by A9, CANTOR_1:9;
X in the topology of T by A9, PRE_TOPC:def_1;
hence the topology of TopStruct(# X,B #) c= the topology of T by A1, A3, A2, A4, A13, A11, CANTOR_1:7, ZFMISC_1:31; ::_thesis: verum
end;