:: On the characteristic and weight of a topological space
:: by Grzegorz Bancerek
::
:: Received December 10, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

::<DESC name="baza w punkcie a baza" monograph="topology"/>
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 &amp; U in B )  }  is Basis of x
proofend;

::<DESC name="baza w punkcie a baza" monograph="topology"/>
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
proofend;

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 &amp; ( 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 &amp; ( for B being Basis of x holds b1 c= card B ) )
proofend;
uniqueness
 for b1, b2 being cardinal number st ex B being Basis of x st b1 = card B &amp; ( for B being Basis of x holds b1 c= card B ) &amp; ex B being Basis of x st b2 = card B &amp; ( for B being Basis of x holds b2 c= card B ) holds
b1 = b2
proofend;
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 &amp; ( for B being Basis of x holds b3 c= card B ) ) );

::<DESC name="charakter punktu" monograph="topology"/>
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
proofend;

Lm1: now__::_thesis:_for_T_being_non_empty_TopStruct_holds_
(_union__{__(Chi_(x,T))_where_x_is_Point_of_T_:_verum__}__is_cardinal_number_&amp;_(_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_)_&amp;_(_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 &amp; ( 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 ) &amp; ( 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 ) &amp; ( 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 ) &amp; ( 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 ) &amp; ( 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 ) &amp; ( 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 ) &amp; ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
b1 c= M ) )
proofend;
uniqueness
 for b1, b2 being cardinal number st ( for x being Point of T holds Chi (x,T) c= b1 ) &amp; ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
b1 c= M ) &amp; ( for x being Point of T holds Chi (x,T) c= b2 ) &amp; ( 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
proofend;
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 ) &amp; ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
b2 c= M ) ) );

::<DESC name="charakter przestrzeni" monograph="topology"/>
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  }
proofend;

theorem Th5: :: TOPGEN_2:5
for T being non empty TopStruct
for x being Point of T holds Chi (x,T) c= Chi T
proofend;

::<DESC name="pierwszy aksjomat przeliczalno/sci" monograph="topology"/>
theorem :: TOPGEN_2:6
for T being non empty TopSpace holds
( T is first-countable iff Chi T c= omega )
proofend;

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
proofend;
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 );

::<DESC name="uk/lad otocze/n" monograph="topology"/>
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
proofend;
let x be Point of T;
:: original:.
redefine funcN . x ->  Basis of x;
coherence
 N . x is Basis of x by Def3;
end;

::<DESC name="uk/lad otocze/n: (BP1)" monograph="topology"/>
:: for T being non empty TopSpace
:: for N being Neighborhood_System of T
:: for x being Element of T holds N.x is non empty &amp;
:: for U being set st U in N.x holds x in U
:: by YELLOW_8:21; :: and clusters YELLOW12
::<DESC name="uk/lad otocze/n: (BP2)" monograph="topology"/>
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 &amp; U in B2 holds
ex V being open Subset of T st
( V in B1 &amp; V c= U )
proofend;

::<DESC name="uk/lad otocze/n: (BP3)" monograph="topology"/>
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 &amp; U2 in B holds
ex V being open Subset of T st
( V in B &amp; V c= U1 /\ U2 )
proofend;

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_&amp;_x_in_U_holds_
A_meets_U
let U be Subset of T; ::_thesis: ( U is open &amp; 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 &amp; 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;

::<DESC name="1.1.1. Twierdzenie: Cl a baza w punkcie" monograph="topology"/>
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 )
proofend;

::<DESC name="1.1.1. Twierdzenie: Cl a baza w punkcie" monograph="topology"/>
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 )
proofend;

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 &amp; not b1 is empty )
proofend;
end;

begin

::<DESC name="1.1.14. Twierdzenie: istnienie podrodziny mocy niewi/ekszej od wagi przestrzeni i o unii r/ownej" monograph="topology"/>
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 &amp; union G = union S &amp; card G c= weight T )
proofend;

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
proofend;
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
proofend;

theorem Th13: :: TOPGEN_2:13
for T being non empty discrete TopStruct holds
( SmallestPartition the carrier of T is Basis of T &amp; ( for B being Basis of T holds SmallestPartition the carrier of T c= B ) )
proofend;

theorem Th14: :: TOPGEN_2:14
for T being non empty discrete TopStruct holds weight T = card the carrier of T
proofend;

registration
cluster TopSpace-like infinite-weight for TopStruct ;
existence
 ex b1 being TopSpace st b1 is infinite-weight
proofend;
end;

Lm4:  for T being infinite-weight TopSpace
for B being Basis of T ex B1 being Basis of T st
( B1 c= B &amp; card B1 = weight T )
proofend;

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 &amp; ( for x being Point of T holds
( x in f . x &amp; ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) )
proofend;

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 &amp; ( for x being Point of T holds
( x in f . x &amp; ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
B0 c= B
proofend;

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 &amp; ( for x being Point of T holds
( x in f . x &amp; ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
weight T = card B0
proofend;

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 &amp; card B1 = weight T )
proofend;

::<DESC name="1.1.15. Twierdzenie: o istnieniu bazy bed/acej podrodzin/a bazy i maj/acej moc r/own/a wadze przestrzeni" monograph="topology"/>
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 &amp; card B1 = weight T )
proofend;

begin

definition
let X, x0 be set ;
func DiscrWithInfin (X,x0) ->  strict TopStruct  means :Def5: :: TOPGEN_2:def 5
( the carrier of it = X &amp; 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 &amp; 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  }  &amp; the carrier of b2 = X &amp; 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 &amp; 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  }  )
proofend;
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 &amp; 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
proofend;
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 ) )
proofend;

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 &amp; not x0 in A &amp; not A is finite ) )
proofend;

theorem :: TOPGEN_2:21
for X, x0, x being set st x in X holds
{x} is closed Subset of (DiscrWithInfin (X,x0))
proofend;

theorem Th22: :: TOPGEN_2:22
for X, x0, x being set st x in X &amp; x <> x0 holds
{x} is open Subset of (DiscrWithInfin (X,x0))
proofend;

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
proofend;

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
proofend;

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}
proofend;

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}
proofend;

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
proofend;

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}
proofend;

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  }
proofend;

theorem :: TOPGEN_2:30
for X being infinite set holds card (Fin X) = card X
proofend;

theorem Th31: :: TOPGEN_2:31
for X being infinite set holds card  {  (F `) where F is Subset of X : F is finite  }  = card X
proofend;

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
proofend;

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
proofend;

theorem :: TOPGEN_2:34
for X being infinite set
for x0 being set holds weight (DiscrWithInfin (X,x0)) = card X
proofend;

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  }
proofend;

begin

::<DSCR name="Exercise 1.1.B" monograph="topology"/>
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  }  )
proofend;

::<DSCR name="Exercise 1.1.B" monograph="topology"/>
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 &amp; F \ G is finite )  }  )
proofend;

::<DSCR name="Exercise 1.1.D" monograph="topology"/>
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 &amp; TopStruct(# X,B #) is TopSpace &amp; ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) &amp; ( for T being TopSpace st the carrier of T = X &amp; ( 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 ) )
proofend;

::<DSCR name="Exercise 1.1.D" monograph="topology"/>
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)) &amp; TopStruct(# X,B #) is TopSpace &amp; ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) &amp; ( for T being TopSpace st the carrier of T = X &amp; ( 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 #) ) )
proofend;