:: On the characteristic and weight of a topological space
:: by Grzegorz Bancerek
::
:: Received December 10, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: TOPGEN_2:1
theorem Th2: :: TOPGEN_2:2
:: deftheorem Def1 defines Chi TOPGEN_2:def 1 :
theorem Th3: :: TOPGEN_2:3
Lm1:
now
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 } ;
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 ) )
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
hence
m c= M
by A1, ZFMISC_1:94;
:: thesis: verum
end;
:: deftheorem Def2 defines Chi TOPGEN_2:def 2 :
theorem Th4: :: TOPGEN_2:4
theorem Th5: :: TOPGEN_2:5
theorem :: TOPGEN_2:6
:: deftheorem Def3 defines Neighborhood_System TOPGEN_2:def 3 :
theorem :: TOPGEN_2:7
canceled;
theorem :: TOPGEN_2:8
theorem :: TOPGEN_2:9
theorem :: TOPGEN_2:10
theorem :: TOPGEN_2:11
theorem Th12: :: TOPGEN_2:12
:: deftheorem Def4 defines finite-weight TOPGEN_2:def 4 :
theorem Th13: :: TOPGEN_2:13
theorem Th14: :: TOPGEN_2:14
theorem Th15: :: TOPGEN_2:15
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 )
theorem :: TOPGEN_2:16
canceled;
theorem Th17: :: TOPGEN_2:17
theorem Th18: :: TOPGEN_2:18
theorem Th19: :: TOPGEN_2:19
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 )
theorem :: TOPGEN_2:20
:: deftheorem Def5 defines DiscrWithInfin TOPGEN_2:def 5 :
theorem Th21: :: TOPGEN_2:21
theorem Th22: :: TOPGEN_2:22
theorem :: TOPGEN_2:23
theorem Th24: :: TOPGEN_2:24
theorem :: TOPGEN_2:25
theorem Th26: :: TOPGEN_2:26
theorem Th27: :: TOPGEN_2:27
theorem Th28: :: TOPGEN_2:28
theorem :: TOPGEN_2:29
theorem :: TOPGEN_2:30
theorem Th31: :: TOPGEN_2:31
theorem :: TOPGEN_2:32
theorem Th33: :: TOPGEN_2:33
theorem Th34: :: TOPGEN_2:34
theorem Th35: :: TOPGEN_2:35
theorem :: TOPGEN_2:36
theorem :: TOPGEN_2:37
theorem :: TOPGEN_2:38
theorem :: TOPGEN_2:39
theorem :: TOPGEN_2:40
theorem :: TOPGEN_2:41