:: TOPGEN_4 semantic presentation

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_4:def 1, 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 by CARD_4:43;
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;

theorem Th5: :: TOPGEN_4:5

for T being non empty TopSpace holds density T <=` 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 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) <=` alef 0 )

proof end;

theorem :: TOPGEN_4:11

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

proof end;

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 sigma_Field_Subset of T holds
F is closed_for_countable_unions

proof end;

registration

let T be set ;
cluster -> closed_for_countable_unions Element of K10(K10(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 K10(K10(T));
coherence by Th12;

end;

theorem Th13: :: TOPGEN_4:13

for T being set
for F being Subset-Family of T holds
( F is sigma_Field_Subset 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 K10(K10(the carrier of T));
coherence by Th17, Th14;
cluster compl-closed all-closed-containing closed_for_countable_meets -> non empty all-open-containing closed_for_countable_unions Element of K10(K10(the carrier of T));
coherence by Th17, Th14;

end;

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 non empty TopSpace;
cluster empty -> open closed Element of K10(K10(the carrier of T));
coherence

proof end;

end;

registration

let T be non empty TopSpace;
cluster open closed countable Element of K10(K10(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

proof end;

end;

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) <=` 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) <=` 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;

definition

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

end;

:: deftheorem Def6 defines F_sigma TOPGEN_4:def 6 :

definition

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

end;

:: deftheorem Def7 defines G_delta TOPGEN_4:def 7 :

theorem Th35: :: TOPGEN_4:35

for T being non empty TopSpace holds {} T is F_sigma

proof end;

theorem Th36: :: TOPGEN_4:36

for T being non empty TopSpace holds {} T is G_delta

proof end;

registration

let T be non empty TopSpace;
cluster {} T -> countable F_sigma G_delta ;
coherence by Th36, Th35;

end;

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;

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 being_T1 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;

theorem :: TOPGEN_4:50

for T being non empty TopSpace
for p being Point of T holds
( p is_isolated_in [#] T or p is_an_accumulation_point_of [#] T )

proof end;

registration

cluster T_1/2 -> T_0 TopStruct ;
coherence

proof end;

cluster being_T1 -> T_1/2 TopStruct ;
coherence by Th48;

end;

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 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 countable ;
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 second-countable separable TopStruct ;
existence

proof end;

end;

registration

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

proof end;

end;

theorem Th61: :: 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 Th62: :: TOPGEN_4:62

for T, F being set holds
( F is SigmaField of T iff F is sigma_Field_Subset of T )

proof end;

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;
mode sigma_Field_Subset of T is sigma_Field_Subset of the carrier of T;

end;

registration

let T be non empty TopSpace;
cluster non empty compl-closed all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets Element of K10(K10(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) -> compl-closed all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets ;
coherence by Th65;

end;

registration

let T be non empty 1-sorted ;
cluster non empty compl-closed sigma_Field_Subset-like closed_for_countable_unions Element of K10(K10(the carrier of T));
existence

proof end;

end;

registration

let T be non empty TopSpace;
cluster -> non empty closed_for_countable_unions SigmaField of the carrier of T;
coherence by Th62;

end;

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

proof end;

registration

let T be non empty TopSpace;
cluster all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets SigmaField of 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 K10(the carrier of T);
coherence

proof end;

end;

registration

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

proof end;

end;