:: TOPGEN_4 semantic presentation

definition

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

end;

:: deftheorem Def1 defines TotFam TOPGEN_4:def 1 :

theorem Th1: :: TOPGEN_4:1

for b₁ being set
for b₂ being Subset-Family of b₁ holds
( b₂ is countable iff COMPLEMENT b₂ is countable )

proof end;

registration

cluster RAT -> countable ;
coherence by CARD_4:def 1, TOPGEN_3:17;

end;

Lemma2: for b₁ being set holds
( b₁ is countable iff ex b₂ being Function st
( dom b₂ = RAT & b₁ c= rng b₂ ) )

proof end;

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

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

proof end;

theorem Th2: :: TOPGEN_4:2

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds Der b₂ = { b₃ where B is Point of b₁ : b₃ in Cl (b₂ \ {b₃}) }

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 Th3: :: TOPGEN_4:3

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( b₂ is closed iff Der b₂ c= b₂ )

proof end;

theorem Th4: :: TOPGEN_4:4

for b₁ being non empty TopStruct
for b₂ being Basis of b₁
for b₃ being Subset of b₁ st b₃ is open & b₃ <> {} holds
ex b₄ being Subset of b₁ st
( b₄ in b₂ & b₄ c= b₃ & b₄ <> {} )

proof end;

theorem Th5: :: TOPGEN_4:5

for b₁ being non empty TopSpace holds density b₁ <=` weight b₁

proof end;

theorem Th6: :: TOPGEN_4:6

for b₁ being non empty TopSpace holds
( b₁ is separable iff ex b₂ being Subset of b₁ st
( b₂ is dense & b₂ is countable ) )

proof end;

theorem Th7: :: TOPGEN_4:7

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

proof end;

registration

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

end;

theorem Th8: :: TOPGEN_4:8

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ are_separated holds
Fr (b₂ \/ b₃) = (Fr b₂) \/ (Fr b₃)

proof end;

theorem Th9: :: TOPGEN_4:9

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is locally_finite holds
Fr (union b₂) c= union (Fr b₂)

proof end;

theorem Th10: :: TOPGEN_4:10

for b₁ being non empty discrete TopSpace holds
( b₁ is separable iff Card ([#] b₁) <=` alef 0 )

proof end;

theorem Th11: :: TOPGEN_4:11

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

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Subset-Family of c₁;
attr a₂ is all-open-containing means :Def2: :: TOPGEN_4:def 2
for b₁ being Subset of a₁ st b₁ is open holds
b₁ in a₂;

end;

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

definition

let c₁ be non empty TopSpace;
let c₂ be Subset-Family of c₁;
attr a₂ is all-closed-containing means :Def3: :: TOPGEN_4:def 3
for b₁ being Subset of a₁ st b₁ is closed holds
b₁ in a₂;

end;

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

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
attr a₂ is closed_for_countable_unions means :Def4: :: TOPGEN_4:def 4
for b₁ being countable Subset-Family of a₁ st b₁ c= a₂ holds
union b₁ in a₂;

end;

:: deftheorem Def4 defines closed_for_countable_unions TOPGEN_4:def 4 :

Lemma10: for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ is sigma_Field_Subset of b₁ holds
b₂ is closed_for_countable_unions

proof end;

registration

let c₁ be set ;
cluster -> closed_for_countable_unions Element of K10(K10(a₁));
coherence by Lemma10;

end;

theorem Th12: :: TOPGEN_4:12

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ is closed_for_countable_unions holds
{} in b₂

proof end;

registration

let c₁ be set ;
cluster closed_for_countable_unions -> non empty Element of K10(K10(a₁));
coherence by Th12;

end;

theorem Th13: :: TOPGEN_4:13

for b₁ being set
for b₂ being Subset-Family of b₁ holds
( b₂ is sigma_Field_Subset of b₁ iff ( b₂ is compl-closed & b₂ is closed_for_countable_unions ) )

proof end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
attr a₂ is closed_for_countable_meets means :Def5: :: TOPGEN_4:def 5
for b₁ being countable Subset-Family of a₁ st b₁ c= a₂ holds
meet b₁ in a₂;

end;

:: deftheorem Def5 defines closed_for_countable_meets TOPGEN_4:def 5 :

theorem Th14: :: TOPGEN_4:14

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

proof end;

theorem Th15: :: TOPGEN_4:15

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ is compl-closed holds
b₂ = COMPLEMENT b₂

proof end;

theorem Th16: :: TOPGEN_4:16

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ st b₂ c= b₃ & b₃ is compl-closed holds
COMPLEMENT b₂ c= b₃

proof end;

theorem Th17: :: TOPGEN_4:17

for b₁ being set
for b₂ being Subset-Family of b₁ holds
( b₂ is closed_for_countable_meets & b₂ is compl-closed iff ( b₂ is closed_for_countable_unions & b₂ is compl-closed ) )

proof end;

registration

let c₁ 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 a₁));
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 a₁));
coherence by Th17, Th14;

end;

registration

let c₁ be set ;
let c₂ be countable Subset-Family of c₁;
cluster COMPLEMENT a₂ -> countable ;
coherence by Th1;

end;

registration

let c₁ be non empty TopSpace;
cluster empty -> open closed Element of K10(K10(the carrier of a₁));
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster open closed countable Element of K10(K10(the carrier of a₁));
existence

proof end;

end;

theorem Th18: :: TOPGEN_4:18

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

proof end;

registration

cluster empty -> countable set ;
coherence

proof end;

end;

theorem Th19: :: TOPGEN_4:19

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Subset-Family of b₁ st b₃ = {b₂} holds
( b₂ is open iff b₃ is open )

proof end;

theorem Th20: :: TOPGEN_4:20

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Subset-Family of b₁ st b₃ = {b₂} holds
( b₂ is closed iff b₃ is closed )

proof end;

definition

let c₁ be set ;
let c₂, c₃ be Subset-Family of c₁;
redefine func INTERSECTION as INTERSECTION c₂,c₃ -> Subset-Family of a₁;
coherence

proof end;

redefine func UNION as UNION c₂,c₃ -> Subset-Family of a₁;
coherence

proof end;

end;

theorem Th21: :: TOPGEN_4:21

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ is closed & b₃ is closed holds
INTERSECTION b₂,b₃ is closed

proof end;

theorem Th22: :: TOPGEN_4:22

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ is closed & b₃ is closed holds
UNION b₂,b₃ is closed

proof end;

theorem Th23: :: TOPGEN_4:23

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ is open & b₃ is open holds
INTERSECTION b₂,b₃ is open

proof end;

theorem Th24: :: TOPGEN_4:24

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ is open & b₃ is open holds
UNION b₂,b₃ is open

proof end;

theorem Th25: :: TOPGEN_4:25

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ holds Card (INTERSECTION b₂,b₃) <=` Card [:b₂,b₃:]

proof end;

theorem Th26: :: TOPGEN_4:26

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ holds Card (UNION b₂,b₃) <=` Card [:b₂,b₃:]

proof end;

theorem Th27: :: TOPGEN_4:27

for b₁, b₂ being set holds union (UNION b₁,b₂) c= (union b₁) \/ (union b₂)

proof end;

theorem Th28: :: TOPGEN_4:28

for b₁, b₂ being set st b₁ <> {} & b₂ <> {} holds
(union b₁) \/ (union b₂) = union (UNION b₁,b₂)

proof end;

theorem Th29: :: TOPGEN_4:29

for b₁ being set holds UNION {} ,b₁ = {}

proof end;

theorem Th30: :: TOPGEN_4:30

for b₁, b₂ being set holds
( not UNION b₁,b₂ = {} or b₁ = {} or b₂ = {} )

proof end;

theorem Th31: :: TOPGEN_4:31

for b₁, b₂ being set holds
( not INTERSECTION b₁,b₂ = {} or b₁ = {} or b₂ = {} )

proof end;

theorem Th32: :: TOPGEN_4:32

for b₁, b₂ being set holds meet (UNION b₁,b₂) c= (meet b₁) \/ (meet b₂)

proof end;

theorem Th33: :: TOPGEN_4:33

for b₁, b₂ being set st b₁ <> {} & b₂ <> {} holds
meet (UNION b₁,b₂) = (meet b₁) \/ (meet b₂)

proof end;

theorem Th34: :: TOPGEN_4:34

for b₁, b₂ being set st b₁ <> {} & b₂ <> {} holds
(meet b₁) /\ (meet b₂) = meet (INTERSECTION b₁,b₂)

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
attr a₂ is F_sigma means :Def6: :: TOPGEN_4:def 6
ex b₁ being closed countable Subset-Family of a₁ st a₂ = union b₁;

end;

:: deftheorem Def6 defines F_sigma TOPGEN_4:def 6 :

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
attr a₂ is G_delta means :Def7: :: TOPGEN_4:def 7
ex b₁ being open countable Subset-Family of a₁ st a₂ = meet b₁;

end;

:: deftheorem Def7 defines G_delta TOPGEN_4:def 7 :

theorem Th35: :: TOPGEN_4:35

for b₁ being non empty TopSpace holds {} b₁ is F_sigma

proof end;

theorem Th36: :: TOPGEN_4:36

for b₁ being non empty TopSpace holds {} b₁ is G_delta

proof end;

registration

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

end;

theorem Th37: :: TOPGEN_4:37

for b₁ being non empty TopSpace holds [#] b₁ is F_sigma

proof end;

theorem Th38: :: TOPGEN_4:38

for b₁ being non empty TopSpace holds [#] b₁ is G_delta

proof end;

registration

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

end;

theorem Th39: :: TOPGEN_4:39

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is F_sigma holds
b₂ ` is G_delta

proof end;

theorem Th40: :: TOPGEN_4:40

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is G_delta holds
b₂ ` is F_sigma

proof end;

theorem Th41: :: TOPGEN_4:41

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is F_sigma & b₃ is F_sigma holds
b₂ /\ b₃ is F_sigma

proof end;

theorem Th42: :: TOPGEN_4:42

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is F_sigma & b₃ is F_sigma holds
b₂ \/ b₃ is F_sigma

proof end;

theorem Th43: :: TOPGEN_4:43

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is G_delta & b₃ is G_delta holds
b₂ \/ b₃ is G_delta

proof end;

theorem Th44: :: TOPGEN_4:44

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is G_delta & b₃ is G_delta holds
b₂ /\ b₃ is G_delta

proof end;

theorem Th45: :: TOPGEN_4:45

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is closed holds
b₂ is F_sigma

proof end;

theorem Th46: :: TOPGEN_4:46

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is open holds
b₂ is G_delta

proof end;

theorem Th47: :: TOPGEN_4:47

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

proof end;

definition

let c₁ be TopSpace;
attr a₁ is T_1/2 means :Def8: :: TOPGEN_4:def 8
for b₁ being Subset of a₁ holds Der b₁ is closed;

end;

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

theorem Th48: :: TOPGEN_4:48

for b₁ being TopSpace st b₁ is being_T1 holds
b₁ is T_1/2

proof end;

theorem Th49: :: TOPGEN_4:49

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

proof end;

theorem Th50: :: TOPGEN_4:50

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds
( b₂ is_isolated_in [#] b₁ or b₂ is_an_accumulation_point_of [#] b₁ )

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 c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
let c₃ be Point of c₁;
pred c₃ is_a_condensation_point_of c₂ means :Def9: :: TOPGEN_4:def 9
for b₁ being a_neighborhood of a₃ holds not b₁ /\ a₂ is countable;

end;

:: deftheorem Def9 defines is_a_condensation_point_of TOPGEN_4:def 9 :

theorem Th51: :: TOPGEN_4:51

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Point of b₁ st b₄ is_a_condensation_point_of b₂ & b₂ c= b₃ holds
b₄ is_a_condensation_point_of b₃

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
func c₂ ^0 -> Subset of a₁ means :Def10: :: TOPGEN_4:def 10
for b₁ being Point of a₁ holds
( b₁ in a₃ iff b₁ 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 b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₃ is_a_condensation_point_of b₂ holds
b₃ is_an_accumulation_point_of b₂

proof end;

theorem Th53: :: TOPGEN_4:53

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds b₂ ^0 c= Der b₂

proof end;

theorem Th54: :: TOPGEN_4:54

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds b₂ ^0 = Cl (b₂ ^0 )

proof end;

theorem Th55: :: TOPGEN_4:55

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
b₂ ^0 c= b₃ ^0

proof end;

theorem Th56: :: TOPGEN_4:56

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Point of b₁ holds
( not b₄ is_a_condensation_point_of b₂ \/ b₃ or b₄ is_a_condensation_point_of b₂ or b₄ is_a_condensation_point_of b₃ )

proof end;

theorem Th57: :: TOPGEN_4:57

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ holds (b₂ \/ b₃) ^0 = (b₂ ^0 ) \/ (b₃ ^0 )

proof end;

theorem Th58: :: TOPGEN_4:58

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is countable holds
for b₃ being Point of b₁ holds not b₃ is_a_condensation_point_of b₂

proof end;

theorem Th59: :: TOPGEN_4:59

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is countable holds
b₂ ^0 = {}

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be countable Subset of c₁;
cluster a₂ ^0 -> empty countable ;
coherence by Th59;

end;

theorem Th60: :: TOPGEN_4:60

for b₁ being non empty TopSpace st b₁ is second-countable holds
ex b₂ being Basis of b₁ st b₂ is countable

proof end;

registration

cluster non empty second-countable separable TopStruct ;
existence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster TotFam a₁ -> 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 b₁ being set
for b₂ being SetSequence of b₁ holds rng b₂ is non empty countable Subset-Family of b₁

proof end;

theorem Th62: :: TOPGEN_4:62

for b₁, b₂ being set holds
( b₂ is SigmaField of b₁ iff b₂ is sigma_Field_Subset of b₁ )

proof end;

theorem Th63: :: TOPGEN_4:63

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ is all-open-containing & b₂ c= b₃ holds
b₃ is all-open-containing

proof end;

theorem Th64: :: TOPGEN_4:64

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ is all-closed-containing & b₂ c= b₃ holds
b₃ is all-closed-containing

proof end;

definition

let c₁ be 1-sorted ;
mode SigmaField of a₁ is SigmaField of the carrier of a₁;
mode sigma_Field_Subset of a₁ is sigma_Field_Subset of the carrier of a₁;

end;

registration

let c₁ 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 a₁));
existence

proof end;

end;

theorem Th65: :: TOPGEN_4:65

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

proof end;

registration

let c₁ be non empty TopSpace;
cluster sigma (TotFam a₁) -> compl-closed all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets ;
coherence by Th65;

end;

registration

let c₁ 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 a₁));
existence

proof end;

end;

registration

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

end;

theorem Th66: :: TOPGEN_4:66

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is compl-closed & b₂ is closed_for_countable_unions holds
b₂ is SigmaField of b₁

proof end;

registration

let c₁ be non empty TopSpace;
cluster all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets SigmaField of the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster Topology_of a₁ -> open all-open-containing ;
coherence

proof end;

end;

theorem Th67: :: TOPGEN_4:67

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ ex b₃ being compl-closed all-open-containing closed_for_countable_unions Subset-Family of b₁ st
( b₂ c= b₃ & ( for b₄ being compl-closed all-open-containing closed_for_countable_unions Subset-Family of b₁ st b₂ c= b₄ holds
b₃ c= b₄ ) )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines BorelSets TOPGEN_4:def 11 :

theorem Th68: :: TOPGEN_4:68

for b₁ being non empty TopSpace
for b₂ being closed Subset-Family of b₁ holds b₂ c= BorelSets b₁

proof end;

theorem Th69: :: TOPGEN_4:69

for b₁ being non empty TopSpace
for b₂ being open Subset-Family of b₁ holds b₂ c= BorelSets b₁

proof end;

theorem Th70: :: TOPGEN_4:70

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

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
attr a₂ is Borel means :Def12: :: TOPGEN_4:def 12
a₂ in BorelSets a₁;

end;

:: deftheorem Def12 defines Borel TOPGEN_4:def 12 :

registration

let c₁ be non empty TopSpace;
cluster F_sigma -> Borel Element of K10(the carrier of a₁);
coherence

proof end;

end;

registration

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

proof end;

end;