begin
theorem Th1:
theorem Th2:
:: deftheorem Def1 defines Chi TOPGEN_2:def 1 :
theorem Th3:
Lm1:
now
let T be non
empty TopStruct ;
( 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;
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 ;
( 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 }
;
( ( 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 ;
( ( 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
;
m c= M
now
let a be
set ;
( 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 }
;
a c= Mthen
ex
x being
Point of
T st
a = Chi x,
T
;
hence
a c= M
by A2;
verum
end;
hence
m c= M
by A1, ZFMISC_1:94;
verum
end;
:: deftheorem Def2 defines Chi TOPGEN_2:def 2 :
theorem Th4:
theorem Th5:
theorem
begin
:: deftheorem Def3 defines Neighborhood_System TOPGEN_2:def 3 :
theorem
canceled;
theorem
theorem
theorem
theorem
begin
theorem Th12:
:: deftheorem Def4 defines finite-weight TOPGEN_2:def 4 :
theorem Th13:
theorem Th14:
theorem Th15:
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
canceled;
theorem Th17:
theorem Th18:
theorem Th19:
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
begin
:: deftheorem Def5 defines DiscrWithInfin TOPGEN_2:def 5 :
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem
theorem Th31:
theorem
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem
begin
theorem
theorem
theorem
theorem