TOPGEN_4: On the {B}orel Families of Subsets of Topological Spaces

:: On the {B}orel Families of Subsets of Topological Spaces
:: by Adam Grabowski
::
:: Received August 30, 2005
:: Copyright (c) 2005-2011 Association of Mizar Users

begin

definition

let T be 1-sorted ;
func TotFam T -> Subset-Family of T equals :: TOPGEN_4:def 1
bool the carrier of T;
coherence ;

end;

:: deftheorem defines TotFam TOPGEN_4:def 1 :

theorem Th1: :: TOPGEN_4:1

for T being set
for F being Subset-Family of T holds
( F is countable iff COMPLEMENT F is countable )

proof end;

registration

cluster RAT -> countable ;
coherence by CARD_3:def 15, TOPGEN_3:17;

end;

Lm1: for X being set holds
( X is countable iff ex f being Function st
( dom f = RAT & X c= rng f ) )

proof end;

scheme :: TOPGEN_4:sch 1
FraenCoun11{ P₁[ set ] } :

{ {n} where n is Element of RAT : P₁[n] } is countable

proof end;

theorem :: TOPGEN_4:2

for T being non empty TopSpace
for A being Subset of T holds Der A = { x where x is Point of T : x in Cl (A \ {x}) }

proof end;

registration

cluster finite -> second-countable TopStruct ;
coherence

proof end;

end;

registration

cluster REAL -> non countable ;
coherence

proof end;

end;

registration

cluster non countable -> non finite set ;
coherence ;
cluster non finite -> non trivial set ;
coherence

proof end;

cluster non empty non countable set ;
existence

proof end;

end;

theorem :: TOPGEN_4:3

for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff Der A c= A )

proof end;

theorem Th4: :: TOPGEN_4:4

for T being non empty TopStruct
for B being Basis of T
for V being Subset of T st V is open & V <> {} holds
ex W being Subset of T st
( W in B & W c= V & W <> {} )

proof end;

begin

theorem Th5: :: TOPGEN_4:5

for T being non empty TopSpace holds density T c= weight T

proof end;

theorem :: TOPGEN_4:6

for T being non empty TopSpace holds
( T is separable iff ex A being Subset of T st
( A is dense & A is countable ) )

proof end;

theorem Th7: :: TOPGEN_4:7

for T being non empty TopSpace st T is second-countable holds
T is separable

proof end;

registration

cluster non empty TopSpace-like second-countable -> non empty separable TopStruct ;
coherence by Th7;

end;

theorem :: TOPGEN_4:8

for T being non empty TopSpace
for A, B being Subset of T st A,B are_separated holds
Fr (A \/ B) = (Fr A) \/ (Fr B)

proof end;

theorem :: TOPGEN_4:9

for T being non empty TopSpace
for F being Subset-Family of T st F is locally_finite holds
Fr (union F) c= union (Fr F)

proof end;

theorem Th10: :: TOPGEN_4:10

for T being non empty discrete TopSpace holds
( T is separable iff card ([#] T) c= omega )

proof end;

theorem :: TOPGEN_4:11

for T being non empty discrete TopSpace holds
( T is separable iff T is countable )

proof end;

begin

definition

let T be non empty TopSpace;
let F be Subset-Family of T;
attr F is all-open-containing means :Def2: :: TOPGEN_4:def 2
for A being Subset of T st A is open holds
A in F;

end;

:: deftheorem Def2 defines all-open-containing TOPGEN_4:def 2 :

definition

let T be non empty TopSpace;
let F be Subset-Family of T;
attr F is all-closed-containing means :Def3: :: TOPGEN_4:def 3
for A being Subset of T st A is closed holds
A in F;

end;

:: deftheorem Def3 defines all-closed-containing TOPGEN_4:def 3 :

definition

let T be set ;
let F be Subset-Family of T;
attr F is closed_for_countable_unions means :Def4: :: TOPGEN_4:def 4
for G being countable Subset-Family of T st G c= F holds
union G in F;

end;

:: 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

proof end;

registration

let T be set ;
cluster non empty compl-closed sigma-multiplicative -> closed_for_countable_unions Element of K21(K21(T));
coherence by Lm2;

end;

theorem Th12: :: TOPGEN_4:12

for T being set
for F being Subset-Family of T st F is closed_for_countable_unions holds
{} in F

proof end;

registration

let T be set ;
cluster closed_for_countable_unions -> non empty Element of K21(K21(T));
coherence by Th12;

end;

theorem Th13: :: TOPGEN_4:13

for T being set
for F being Subset-Family of T holds
( F is SigmaField of T iff ( F is compl-closed & F is closed_for_countable_unions ) )

proof end;

definition

let T be set ;
let F be Subset-Family of T;
attr F is closed_for_countable_meets means :Def5: :: TOPGEN_4:def 5
for G being countable Subset-Family of T st G c= F holds
meet G in F;

end;

:: deftheorem Def5 defines closed_for_countable_meets TOPGEN_4:def 5 :

theorem Th14: :: TOPGEN_4:14

for T being non empty TopSpace
for F being Subset-Family of T holds
( F is all-closed-containing & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )

proof end;

theorem :: TOPGEN_4:15

for T being set
for F being Subset-Family of T st F is compl-closed holds
F = COMPLEMENT F

proof end;

theorem Th16: :: TOPGEN_4:16

for T being set
for F, G being Subset-Family of T st F c= G & G is compl-closed holds
COMPLEMENT F c= G

proof end;

theorem Th17: :: TOPGEN_4:17

for T being set
for F being Subset-Family of T holds
( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )

proof end;

registration

let T be non empty TopSpace;
cluster compl-closed all-open-containing closed_for_countable_unions -> all-closed-containing closed_for_countable_meets Element of K21(K21( the carrier of T));
coherence by Th14, Th17;
cluster compl-closed all-closed-containing closed_for_countable_meets -> all-open-containing closed_for_countable_unions Element of K21(K21( the carrier of T));
coherence by Th14, Th17;

end;

begin

registration

let T be set ;
let F be countable Subset-Family of T;
cluster COMPLEMENT F -> countable ;
coherence by Th1;

end;

registration

let T be TopSpace;
cluster empty -> open closed Element of K21(K21( the carrier of T));
coherence

proof end;

end;

registration

let T be TopSpace;
cluster countable open closed Element of K21(K21( the carrier of T));
existence

proof end;

end;

theorem Th18: :: TOPGEN_4:18

for T being set holds {} is empty Subset-Family of T

proof end;

registration

cluster empty -> countable set ;
coherence ;

end;

begin

theorem Th19: :: TOPGEN_4:19

for T being non empty TopSpace
for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is open iff F is open )

proof end;

theorem Th20: :: TOPGEN_4:20

for T being non empty TopSpace
for A being Subset of T
for F being Subset-Family of T st F = {A} holds
( A is closed iff F is closed )

proof end;

definition

let T be set ;
let F, G be Subset-Family of T;
:: original: INTERSECTION
redefine func INTERSECTION (F,G) -> Subset-Family of T;
coherence

proof end;

:: original: UNION
redefine func UNION (F,G) -> Subset-Family of T;
coherence

proof end;

end;

theorem Th21: :: TOPGEN_4:21

for T being non empty TopSpace
for F, G being Subset-Family of T st F is closed & G is closed holds
INTERSECTION (F,G) is closed

proof end;

theorem Th22: :: TOPGEN_4:22

for T being non empty TopSpace
for F, G being Subset-Family of T st F is closed & G is closed holds
UNION (F,G) is closed

proof end;

theorem Th23: :: TOPGEN_4:23

for T being non empty TopSpace
for F, G being Subset-Family of T st F is open & G is open holds
INTERSECTION (F,G) is open

proof end;

theorem Th24: :: TOPGEN_4:24

for T being non empty TopSpace
for F, G being Subset-Family of T st F is open & G is open holds
UNION (F,G) is open

proof end;

theorem Th25: :: TOPGEN_4:25

for T being set
for F, G being Subset-Family of T holds card (INTERSECTION (F,G)) c= card [:F,G:]

proof end;

theorem Th26: :: TOPGEN_4:26

for T being set
for F, G being Subset-Family of T holds card (UNION (F,G)) c= card [:F,G:]

proof end;

theorem Th27: :: TOPGEN_4:27

for F, G being set holds union (UNION (F,G)) c= (union F) \/ (union G)

proof end;

theorem Th28: :: TOPGEN_4:28

for F, G being set st F <> {} & G <> {} holds
(union F) \/ (union G) = union (UNION (F,G))

proof end;

theorem Th29: :: TOPGEN_4:29

for F being set holds UNION ({},F) = {}

proof end;

theorem :: TOPGEN_4:30

for F, G being set holds
( not UNION (F,G) = {} or F = {} or G = {} )

proof end;

theorem :: TOPGEN_4:31

for F, G being set holds
( not INTERSECTION (F,G) = {} or F = {} or G = {} )

proof end;

theorem Th32: :: TOPGEN_4:32

for F, G being set holds meet (UNION (F,G)) c= (meet F) \/ (meet G)

proof end;

theorem :: TOPGEN_4:33

for F, G being set st F <> {} & G <> {} holds
meet (UNION (F,G)) = (meet F) \/ (meet G)

proof end;

theorem Th34: :: TOPGEN_4:34

for F, G being set st F <> {} & G <> {} holds
(meet F) /\ (meet G) = meet (INTERSECTION (F,G))

proof end;

begin

definition

let T be TopSpace;
let A be Subset of T;
attr A is F_sigma means :Def6: :: TOPGEN_4:def 6
ex F being countable closed Subset-Family of T st A = union F;

end;

:: deftheorem Def6 defines F_sigma TOPGEN_4:def 6 :

definition

let T be TopSpace;
let A be Subset of T;
attr A is G_delta means :Def7: :: TOPGEN_4:def 7
ex F being countable open Subset-Family of T st A = meet F;

end;

:: deftheorem Def7 defines G_delta TOPGEN_4:def 7 :

registration

let T be non empty TopSpace;
cluster empty -> F_sigma G_delta Element of K21( the carrier of T);
coherence

proof end;

end;

theorem :: TOPGEN_4:35

canceled;

theorem :: TOPGEN_4:36

canceled;

theorem Th37: :: TOPGEN_4:37

for T being non empty TopSpace holds [#] T is F_sigma

proof end;

theorem Th38: :: TOPGEN_4:38

for T being non empty TopSpace holds [#] T is G_delta

proof end;

registration

let T be non empty TopSpace;
cluster [#] T -> F_sigma G_delta ;
coherence by Th37, Th38;

end;

theorem :: TOPGEN_4:39

for T being non empty TopSpace
for A being Subset of T st A is F_sigma holds
A ` is G_delta

proof end;

theorem :: TOPGEN_4:40

for T being non empty TopSpace
for A being Subset of T st A is G_delta holds
A ` is F_sigma

proof end;

theorem :: TOPGEN_4:41

for T being non empty TopSpace
for A, B being Subset of T st A is F_sigma & B is F_sigma holds
A /\ B is F_sigma

proof end;

theorem :: TOPGEN_4:42

for T being non empty TopSpace
for A, B being Subset of T st A is F_sigma & B is F_sigma holds
A \/ B is F_sigma

proof end;

theorem :: TOPGEN_4:43

for T being non empty TopSpace
for A, B being Subset of T st A is G_delta & B is G_delta holds
A \/ B is G_delta

proof end;

theorem :: TOPGEN_4:44

for T being non empty TopSpace
for A, B being Subset of T st A is G_delta & B is G_delta holds
A /\ B is G_delta

proof end;

theorem :: TOPGEN_4:45

for T being non empty TopSpace
for A being Subset of T st A is closed holds
A is F_sigma

proof end;

theorem :: TOPGEN_4:46

for T being non empty TopSpace
for A being Subset of T st A is open holds
A is G_delta

proof end;

theorem :: TOPGEN_4:47

for A being Subset of R^1 st A = RAT holds
A is F_sigma

proof end;

begin

definition

let T be TopSpace;
attr T is T_1/2 means :Def8: :: TOPGEN_4:def 8
for A being Subset of T holds Der A is closed ;

end;

:: deftheorem Def8 defines T_1/2 TOPGEN_4:def 8 :

theorem Th48: :: TOPGEN_4:48

for T being TopSpace st T is T_1 holds
T is T_1/2

proof end;

theorem Th49: :: TOPGEN_4:49

for T being non empty TopSpace st T is T_1/2 holds
T is T_0

proof end;

registration

cluster TopSpace-like T_1/2 -> T_0 TopStruct ;
coherence

proof end;

cluster TopSpace-like T_1 -> T_1/2 TopStruct ;
coherence by Th48;

end;

begin

definition

let T be non empty TopSpace;
let A be Subset of T;
let x be Point of T;
pred x is_a_condensation_point_of A means :Def9: :: TOPGEN_4:def 9
for N being a_neighborhood of x holds not N /\ A is countable ;

end;

:: deftheorem Def9 defines is_a_condensation_point_of TOPGEN_4:def 9 :

theorem :: TOPGEN_4:50

canceled;

theorem Th51: :: TOPGEN_4:51

for T being non empty TopSpace
for A, B being Subset of T
for x being Point of T st x is_a_condensation_point_of A & A c= B holds
x is_a_condensation_point_of B

proof end;

definition

let T be non empty TopSpace;
let A be Subset of T;
func A ^0 -> Subset of T means :Def10: :: TOPGEN_4:def 10
for x being Point of T holds
( x in it iff x is_a_condensation_point_of A );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines ^0 TOPGEN_4:def 10 :

theorem Th52: :: TOPGEN_4:52

for T being non empty TopSpace
for A being Subset of T
for p being Point of T st p is_a_condensation_point_of A holds
p is_an_accumulation_point_of A

proof end;

theorem :: TOPGEN_4:53

for T being non empty TopSpace
for A being Subset of T holds A ^0 c= Der A

proof end;

theorem :: TOPGEN_4:54

for T being non empty TopSpace
for A being Subset of T holds A ^0 = Cl (A ^0)

proof end;

theorem Th55: :: TOPGEN_4:55

for T being non empty TopSpace
for A, B being Subset of T st A c= B holds
A ^0 c= B ^0

proof end;

theorem Th56: :: TOPGEN_4:56

for T being non empty TopSpace
for A, B being Subset of T
for x being Point of T holds
( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )

proof end;

theorem :: TOPGEN_4:57

for T being non empty TopSpace
for A, B being Subset of T holds (A \/ B) ^0 = (A ^0) \/ (B ^0)

proof end;

theorem Th58: :: TOPGEN_4:58

for T being non empty TopSpace
for A being Subset of T st A is countable holds
for x being Point of T holds not x is_a_condensation_point_of A

proof end;

theorem Th59: :: TOPGEN_4:59

for T being non empty TopSpace
for A being Subset of T st A is countable holds
A ^0 = {}

proof end;

registration

let T be non empty TopSpace;
let A be countable Subset of T;
cluster A ^0 -> empty ;
coherence by Th59;

end;

theorem :: TOPGEN_4:60

for T being non empty TopSpace st T is second-countable holds
ex B being Basis of T st B is countable

proof end;

registration

cluster non empty TopSpace-like second-countable TopStruct ;
existence

proof end;

end;

begin

registration

let T be non empty TopSpace;
cluster TotFam T -> non empty compl-closed all-open-containing closed_for_countable_unions ;
coherence

proof end;

end;

theorem :: TOPGEN_4:61

for T being set
for A being SetSequence of T holds rng A is non empty countable Subset-Family of T

proof end;

theorem :: TOPGEN_4:62

canceled;

theorem Th63: :: TOPGEN_4:63

for T being non empty TopSpace
for F, G being Subset-Family of T st F is all-open-containing & F c= G holds
G is all-open-containing

proof end;

theorem :: TOPGEN_4:64

for T being non empty TopSpace
for F, G being Subset-Family of T st F is all-closed-containing & F c= G holds
G is all-closed-containing

proof end;

definition

let T be 1-sorted ;
mode SigmaField of T is SigmaField of the carrier of T;

end;

registration

let T be non empty TopSpace;
cluster compl-closed all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets Element of K21(K21( the carrier of T));
existence

proof end;

end;

theorem Th65: :: TOPGEN_4:65

for T being non empty TopSpace holds
( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )

proof end;

registration

let T be non empty TopSpace;
cluster sigma (TotFam T) -> all-open-containing closed_for_countable_unions ;
coherence by Th65;

end;

registration

let T be non empty 1-sorted ;
cluster non empty compl-closed sigma-additive closed_for_countable_unions Element of K21(K21( the carrier of T));
existence

proof end;

end;

registration

let T be non empty TopSpace;
cluster non empty compl-closed sigma-multiplicative -> closed_for_countable_unions Element of K21(K21( the carrier of T));
coherence ;

end;

theorem :: TOPGEN_4:66

for T being non empty TopSpace
for F being Subset-Family of T st F is compl-closed & F is closed_for_countable_unions holds
F is SigmaField of T by Th13;

registration

let T be non empty TopSpace;
cluster non empty V18() V19() V20() compl-closed sigma-multiplicative sigma-additive all-open-containing closed_for_countable_unions Element of K21(K21( the carrier of T));
existence

proof end;

end;

registration

let T be non empty TopSpace;
cluster Topology_of T -> open all-open-containing ;
coherence

proof end;

end;

theorem Th67: :: TOPGEN_4:67

for T being non empty TopSpace
for X being Subset-Family of T ex Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st
( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds
Y c= Z ) )

proof end;

definition

let T be non empty TopSpace;
func BorelSets T -> compl-closed all-open-containing closed_for_countable_unions Subset-Family of T means :Def11: :: TOPGEN_4:def 11
for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds it c= G;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines BorelSets TOPGEN_4:def 11 :

theorem Th68: :: TOPGEN_4:68

for T being non empty TopSpace
for F being closed Subset-Family of T holds F c= BorelSets T

proof end;

theorem Th69: :: TOPGEN_4:69

for T being non empty TopSpace
for F being open Subset-Family of T holds F c= BorelSets T

proof end;

theorem :: TOPGEN_4:70

for T being non empty TopSpace holds BorelSets T = sigma (Topology_of T)

proof end;

definition

let T be non empty TopSpace;
let A be Subset of T;
attr A is Borel means :Def12: :: TOPGEN_4:def 12
A in BorelSets T;

end;

:: deftheorem Def12 defines Borel TOPGEN_4:def 12 :

registration

let T be non empty TopSpace;
cluster F_sigma -> Borel Element of K21( the carrier of T);
coherence

proof end;

end;

registration

let T be non empty TopSpace;
cluster G_delta -> Borel Element of K21( the carrier of T);
coherence

proof end;

end;