:: On the {B}orel Families of Subsets of Topological Spaces
:: by Adam Grabowski
::
:: Received August 30, 2005
:: Copyright (c) 2005 Association of Mizar Users
:: deftheorem defines TotFam TOPGEN_4:def 1 :
theorem Th1: :: TOPGEN_4:1
Lm1:
for X being set holds
( X is countable iff ex f being Function st
( dom f = RAT & X c= rng f ) )
theorem :: TOPGEN_4:2
theorem :: TOPGEN_4:3
theorem Th4: :: TOPGEN_4:4
theorem Th5: :: TOPGEN_4:5
theorem :: TOPGEN_4:6
theorem Th7: :: TOPGEN_4:7
theorem :: TOPGEN_4:8
theorem :: TOPGEN_4:9
theorem Th10: :: TOPGEN_4:10
theorem :: TOPGEN_4:11
:: 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: :: TOPGEN_4:12
theorem Th13: :: TOPGEN_4:13
:: deftheorem Def5 defines closed_for_countable_meets TOPGEN_4:def 5 :
theorem Th14: :: TOPGEN_4:14
theorem :: TOPGEN_4:15
theorem Th16: :: TOPGEN_4:16
theorem Th17: :: TOPGEN_4:17
theorem Th18: :: TOPGEN_4:18
theorem Th19: :: TOPGEN_4:19
theorem Th20: :: TOPGEN_4:20
theorem Th21: :: TOPGEN_4:21
theorem Th22: :: TOPGEN_4:22
theorem Th23: :: TOPGEN_4:23
theorem Th24: :: TOPGEN_4:24
theorem Th25: :: TOPGEN_4:25
theorem Th26: :: TOPGEN_4:26
theorem Th27: :: TOPGEN_4:27
theorem Th28: :: TOPGEN_4:28
theorem Th29: :: TOPGEN_4:29
theorem :: TOPGEN_4:30
theorem :: TOPGEN_4:31
theorem Th32: :: TOPGEN_4:32
theorem :: TOPGEN_4:33
theorem Th34: :: TOPGEN_4:34
:: deftheorem Def6 defines F_sigma TOPGEN_4:def 6 :
:: deftheorem Def7 defines G_delta TOPGEN_4:def 7 :
theorem Th35: :: TOPGEN_4:35
theorem Th36: :: TOPGEN_4:36
theorem Th37: :: TOPGEN_4:37
theorem Th38: :: TOPGEN_4:38
theorem :: TOPGEN_4:39
theorem :: TOPGEN_4:40
theorem :: TOPGEN_4:41
theorem :: TOPGEN_4:42
theorem :: TOPGEN_4:43
theorem :: TOPGEN_4:44
theorem :: TOPGEN_4:45
theorem :: TOPGEN_4:46
theorem :: TOPGEN_4:47
:: deftheorem Def8 defines T_1/2 TOPGEN_4:def 8 :
theorem Th48: :: TOPGEN_4:48
theorem Th49: :: TOPGEN_4:49
:: deftheorem Def9 defines is_a_condensation_point_of TOPGEN_4:def 9 :
theorem :: TOPGEN_4:50
canceled;
theorem Th51: :: TOPGEN_4:51
:: deftheorem Def10 defines ^0 TOPGEN_4:def 10 :
theorem Th52: :: TOPGEN_4:52
theorem :: TOPGEN_4:53
theorem :: TOPGEN_4:54
theorem Th55: :: TOPGEN_4:55
theorem Th56: :: TOPGEN_4:56
theorem :: TOPGEN_4:57
theorem Th58: :: TOPGEN_4:58
theorem Th59: :: TOPGEN_4:59
theorem :: TOPGEN_4:60
theorem :: TOPGEN_4:61
theorem :: TOPGEN_4:62
canceled;
theorem Th63: :: TOPGEN_4:63
theorem :: TOPGEN_4:64
theorem Th65: :: TOPGEN_4:65
theorem :: TOPGEN_4:66
theorem Th67: :: TOPGEN_4:67
:: deftheorem Def11 defines BorelSets TOPGEN_4:def 11 :
theorem Th68: :: TOPGEN_4:68
theorem Th69: :: TOPGEN_4:69
theorem :: TOPGEN_4:70
:: deftheorem Def12 defines Borel TOPGEN_4:def 12 :