begin
:: deftheorem defines TotFam TOPGEN_4:def 1 :
theorem Th1:
Lm1:
for X being set holds
( X is countable iff ex f being Function st
( dom f = RAT & X c= rng f ) )
theorem
theorem
theorem Th4:
begin
theorem Th5:
theorem
theorem Th7:
theorem
theorem
theorem Th10:
theorem
begin
:: deftheorem Def2 defines all-open-containing TOPGEN_4:def 2 :
:: deftheorem Def3 defines all-closed-containing TOPGEN_4:def 3 :
:: deftheorem Def4 defines closed_for_countable_unions TOPGEN_4:def 4 :
Lm2:
for T being set
for F being Subset-Family of T st F is SigmaField of T holds
F is closed_for_countable_unions
theorem Th12:
theorem Th13:
:: deftheorem Def5 defines closed_for_countable_meets TOPGEN_4:def 5 :
theorem Th14:
theorem
theorem Th16:
theorem Th17:
begin
theorem Th18:
begin
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem
theorem Th32:
theorem
theorem Th34:
begin
:: deftheorem Def6 defines F_sigma TOPGEN_4:def 6 :
:: deftheorem Def7 defines G_delta TOPGEN_4:def 7 :
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def8 defines T_1/2 TOPGEN_4:def 8 :
theorem Th48:
theorem Th49:
begin
:: deftheorem Def9 defines is_a_condensation_point_of TOPGEN_4:def 9 :
theorem
canceled;
theorem Th51:
:: deftheorem Def10 defines ^0 TOPGEN_4:def 10 :
theorem Th52:
theorem
theorem
theorem Th55:
theorem Th56:
theorem
theorem Th58:
theorem Th59:
theorem
begin
theorem
theorem
canceled;
theorem Th63:
theorem
theorem Th65:
theorem
theorem Th67:
:: deftheorem Def11 defines BorelSets TOPGEN_4:def 11 :
theorem Th68:
theorem Th69:
theorem
:: deftheorem Def12 defines Borel TOPGEN_4:def 12 :