:: TOPGEN_1 semantic presentation

Lemma1: for b₁ being empty TopSpace
for b₂ being Subset of b₁ holds b₂ = {}
;

definition

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

proof end;

end;

theorem Th1: :: TOPGEN_1:1

for b₁ being 1-sorted
for b₂, b₃ being Subset of b₁ holds
( b₂ meets b₃ ` iff b₂ \ b₃ <> {} )

proof end;

theorem Th2: :: TOPGEN_1:2

for b₁ being 1-sorted holds
( b₁ is countable iff [#] b₁ is countable )

proof end;

theorem Th3: :: TOPGEN_1:3

for b₁ being 1-sorted holds
( b₁ is countable iff Card ([#] b₁) <=` alef 0 )

proof end;

registration

let c₁ be finite 1-sorted ;
cluster [#] a₁ -> finite ;
coherence by PRE_TOPC:def 3;

end;

registration

cluster finite -> countable 1-sorted ;
coherence

proof end;

end;

registration

cluster non empty countable 1-sorted ;
existence

proof end;

cluster non empty countable TopStruct ;
existence

proof end;

end;

registration

let c₁ be countable 1-sorted ;
cluster [#] a₁ -> countable ;
coherence

proof end;

end;

registration

cluster non empty being_T1 TopStruct ;
existence

proof end;

end;

theorem Th4: :: TOPGEN_1:4

for b₁ being TopStruct
for b₂ being Subset of b₁ holds b₂ \/ ([#] b₁) = [#] b₁

proof end;

theorem Th5: :: TOPGEN_1:5

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Int b₂ = (Cl (b₂ ` )) `

proof end;

definition

let c₁ be TopSpace;
let c₂ be Subset-Family of c₁;
func Fr c₂ -> Subset-Family of a₁ means :Def1: :: TOPGEN_1:def 1
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ex b₂ being Subset of a₁ st
( b₁ = Fr b₂ & b₂ in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Fr TOPGEN_1:def 1 :

theorem Th6: :: TOPGEN_1:6

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ st b₂ = {} holds
Fr b₂ = {}

proof end;

theorem Th7: :: TOPGEN_1:7

for b₁ being TopSpace
for b₂ being Subset-Family of b₁
for b₃ being Subset of b₁ st b₂ = {b₃} holds
Fr b₂ = {(Fr b₃)}

proof end;

theorem Th8: :: TOPGEN_1:8

for b₁ being TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ c= b₃ holds
Fr b₂ c= Fr b₃

proof end;

theorem Th9: :: TOPGEN_1:9

for b₁ being TopSpace
for b₂, b₃ being Subset-Family of b₁ holds Fr (b₂ \/ b₃) = (Fr b₂) \/ (Fr b₃)

proof end;

theorem Th10: :: TOPGEN_1:10

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Fr b₂ = (Cl b₂) \ (Int b₂)

proof end;

theorem Th11: :: TOPGEN_1:11

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Fr b₂ iff for b₄ being Subset of b₁ st b₄ is open & b₃ in b₄ holds
( b₂ meets b₄ & b₄ \ b₂ <> {} ) )

proof end;

theorem Th12: :: TOPGEN_1:12

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Fr b₂ iff for b₄ being Basis of b₃
for b₅ being Subset of b₁ st b₅ in b₄ holds
( b₂ meets b₅ & b₅ \ b₂ <> {} ) )

proof end;

theorem Th13: :: TOPGEN_1:13

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Fr b₂ iff ex b₄ being Basis of b₃ st
for b₅ being Subset of b₁ st b₅ in b₄ holds
( b₂ meets b₅ & b₅ \ b₂ <> {} ) )

proof end;

theorem Th14: :: TOPGEN_1:14

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds Fr (b₂ /\ b₃) c= ((Cl b₂) /\ (Fr b₃)) \/ ((Fr b₂) /\ (Cl b₃))

proof end;

theorem Th15: :: TOPGEN_1:15

for b₁ being TopSpace
for b₂ being Subset of b₁ holds the carrier of b₁ = ((Int b₂) \/ (Fr b₂)) \/ (Int (b₂ ` ))

proof end;

theorem Th16: :: TOPGEN_1:16

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( ( b₂ is open & b₂ is closed ) iff Fr b₂ = {} )

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
let c₃ be set ;
pred c₃ is_an_accumulation_point_of c₂ means :Def2: :: TOPGEN_1:def 2
a₃ in Cl (a₂ \ {a₃});

end;

:: deftheorem Def2 defines is_an_accumulation_point_of TOPGEN_1:def 2 :

theorem Th17: :: TOPGEN_1:17

for b₁ being TopSpace
for b₂ being Subset of b₁
for b₃ being set st b₃ is_an_accumulation_point_of b₂ holds
b₃ is Point of b₁

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
func Der c₂ -> Subset of a₁ means :Def3: :: TOPGEN_1:def 3
for b₁ being set st b₁ in the carrier of a₁ holds
( b₁ in a₃ iff b₁ is_an_accumulation_point_of a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Der TOPGEN_1:def 3 :

theorem Th18: :: TOPGEN_1:18

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being set holds
( b₃ in Der b₂ iff b₃ is_an_accumulation_point_of b₂ )

proof end;

theorem Th19: :: TOPGEN_1:19

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Der b₂ iff for b₄ being open Subset of b₁ st b₃ in b₄ holds
ex b₅ being Point of b₁ st
( b₅ in b₂ /\ b₄ & b₃ <> b₅ ) )

proof end;

theorem Th20: :: TOPGEN_1:20

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Der b₂ iff for b₄ being Basis of b₃
for b₅ being Subset of b₁ st b₅ in b₄ holds
ex b₆ being Point of b₁ st
( b₆ in b₂ /\ b₅ & b₃ <> b₆ ) )

proof end;

theorem Th21: :: TOPGEN_1:21

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Der b₂ iff ex b₄ being Basis of b₃ st
for b₅ being Subset of b₁ st b₅ in b₄ holds
ex b₆ being Point of b₁ st
( b₆ in b₂ /\ b₅ & b₃ <> b₆ ) )

proof end;

definition

let c₁ be TopSpace;
let c₂ be Subset of c₁;
let c₃ be set ;
pred c₃ is_isolated_in c₂ means :Def4: :: TOPGEN_1:def 4
( a₃ in a₂ & not a₃ is_an_accumulation_point_of a₂ );

end;

:: deftheorem Def4 defines is_isolated_in TOPGEN_1:def 4 :

theorem Th22: :: TOPGEN_1:22

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being set holds
( b₃ in b₂ \ (Der b₂) iff b₃ is_isolated_in b₂ )

proof end;

theorem Th23: :: TOPGEN_1:23

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ is_an_accumulation_point_of b₂ iff for b₄ being open Subset of b₁ st b₃ in b₄ holds
ex b₅ being Point of b₁ st
( b₅ <> b₃ & b₅ in b₂ & b₅ in b₄ ) )

proof end;

theorem Th24: :: TOPGEN_1:24

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ is_isolated_in b₂ iff ex b₄ being open Subset of b₁ st b₄ /\ b₂ = {b₃} )

proof end;

definition

let c₁ be TopSpace;
let c₂ be Point of c₁;
attr a₂ is isolated means :Def5: :: TOPGEN_1:def 5
a₂ is_isolated_in [#] a₁;

end;

:: deftheorem Def5 defines isolated TOPGEN_1:def 5 :

theorem Th25: :: TOPGEN_1:25

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds
( b₂ is isolated iff {b₂} is open )

proof end;

definition

let c₁ be TopSpace;
let c₂ be Subset-Family of c₁;
func Der c₂ -> Subset-Family of a₁ means :Def6: :: TOPGEN_1:def 6
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ex b₂ being Subset of a₁ st
( b₁ = Der b₂ & b₂ in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Der TOPGEN_1:def 6 :

theorem Th26: :: TOPGEN_1:26

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ = {} holds
Der b₂ = {}

proof end;

theorem Th27: :: TOPGEN_1:27

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

proof end;

theorem Th28: :: TOPGEN_1:28

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ c= b₃ holds
Der b₂ c= Der b₃

proof end;

theorem Th29: :: TOPGEN_1:29

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ holds Der (b₂ \/ b₃) = (Der b₂) \/ (Der b₃)

proof end;

theorem Th30: :: TOPGEN_1:30

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

proof end;

theorem Th31: :: TOPGEN_1:31

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Cl b₂ = b₂ \/ (Der b₂)

proof end;

theorem Th32: :: TOPGEN_1:32

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

proof end;

theorem Th33: :: TOPGEN_1:33

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

proof end;

theorem Th34: :: TOPGEN_1:34

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

proof end;

theorem Th35: :: TOPGEN_1:35

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₁ is being_T1 holds
Cl (Der b₂) = Der b₂

proof end;

registration

let c₁ be non empty being_T1 TopSpace;
let c₂ be Subset of c₁;
cluster Der a₂ -> closed ;
coherence

proof end;

end;

theorem Th36: :: TOPGEN_1:36

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ holds union (Der b₂) c= Der (union b₂)

proof end;

theorem Th37: :: TOPGEN_1:37

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

proof end;

definition

let c₁ be TopSpace;
let c₂ be Subset of c₁;
attr a₂ is dense-in-itself means :Def7: :: TOPGEN_1:def 7
a₂ c= Der a₂;

end;

:: deftheorem Def7 defines dense-in-itself TOPGEN_1:def 7 :

definition

let c₁ be non empty TopSpace;
attr a₁ is dense-in-itself means :: TOPGEN_1:def 8
[#] a₁ is dense-in-itself;

end;

:: deftheorem Def8 defines dense-in-itself TOPGEN_1:def 8 :

theorem Th38: :: TOPGEN_1:38

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₁ is being_T1 & b₂ is dense-in-itself holds
Cl b₂ is dense-in-itself

proof end;

definition

let c₁ be TopSpace;
let c₂ be Subset-Family of c₁;
attr a₂ is dense-in-itself means :Def9: :: TOPGEN_1:def 9
for b₁ being Subset of a₁ st b₁ in a₂ holds
b₁ is dense-in-itself;

end;

:: deftheorem Def9 defines dense-in-itself TOPGEN_1:def 9 :

theorem Th39: :: TOPGEN_1:39

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is dense-in-itself holds
union b₂ c= union (Der b₂)

proof end;

theorem Th40: :: TOPGEN_1:40

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is dense-in-itself holds
union b₂ is dense-in-itself

proof end;

theorem Th41: :: TOPGEN_1:41

for b₁ being non empty TopSpace holds Fr ({} b₁) = {}

proof end;

registration

let c₁ be TopSpace;
let c₂ be open closed Subset of c₁;
cluster Fr a₂ -> empty ;
coherence by Th16;

end;

registration

let c₁ be non empty non discrete TopSpace;
cluster non open Element of K10(the carrier of a₁);
existence by TDLAT_3:17;
cluster non closed Element of K10(the carrier of a₁);
existence by TDLAT_3:18;

end;

registration

let c₁ be non empty non discrete TopSpace;
let c₂ be non open Subset of c₁;
cluster Fr a₂ -> non empty ;
coherence by Th16;

end;

registration

let c₁ be non empty non discrete TopSpace;
let c₂ be non closed Subset of c₁;
cluster Fr a₂ -> non empty ;
coherence by Th16;

end;

definition

let c₁ be TopSpace;
let c₂ be Subset of c₁;
attr a₂ is perfect means :Def10: :: TOPGEN_1:def 10
( a₂ is closed & a₂ is dense-in-itself );

end;

:: deftheorem Def10 defines perfect TOPGEN_1:def 10 :

registration

let c₁ be TopSpace;
cluster perfect -> closed dense-in-itself Element of K10(the carrier of a₁);
coherence by Def10;
cluster closed dense-in-itself -> perfect Element of K10(the carrier of a₁);
coherence by Def10;

end;

theorem Th42: :: TOPGEN_1:42

for b₁ being TopSpace holds Der ({} b₁) = {} b₁

proof end;

Lemma36: for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is closed & b₂ is dense-in-itself holds
Der b₂ = b₂

proof end;

theorem Th43: :: TOPGEN_1:43

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is perfect iff Der b₂ = b₂ )

proof end;

theorem Th44: :: TOPGEN_1:44

for b₁ being TopSpace holds {} b₁ is perfect

proof end;

registration

let c₁ be TopSpace;
cluster empty -> closed dense-in-itself perfect Element of K10(the carrier of a₁);
coherence

proof end;

end;

registration

let c₁ be TopSpace;
cluster closed dense-in-itself perfect Element of K10(the carrier of a₁);
existence

proof end;

end;

definition

let c₁ be TopSpace;
let c₂ be Subset of c₁;
attr a₂ is scattered means :Def11: :: TOPGEN_1:def 11
for b₁ being Subset of a₁ holds
( b₁ is empty or not b₁ c= a₂ or not b₁ is dense-in-itself );

end;

:: deftheorem Def11 defines scattered TOPGEN_1:def 11 :

registration

let c₁ be non empty TopSpace;
cluster non empty scattered -> non dense-in-itself Element of K10(the carrier of a₁);
coherence by Def11;
cluster non empty dense-in-itself -> non scattered Element of K10(the carrier of a₁);
coherence by Def11;

end;

theorem Th45: :: TOPGEN_1:45

for b₁ being TopSpace holds {} b₁ is scattered

proof end;

registration

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

proof end;

end;

theorem Th46: :: TOPGEN_1:46

for b₁ being non empty TopSpace st b₁ is being_T1 holds
ex b₂, b₃ being Subset of b₁ st
( b₂ \/ b₃ = [#] b₁ & b₂ misses b₃ & b₂ is perfect & b₃ is scattered )

proof end;

registration

let c₁ be discrete TopSpace;
let c₂ be Subset of c₁;
cluster Fr a₂ -> empty closed dense-in-itself perfect scattered ;
coherence

proof end;

end;

registration

let c₁ be discrete TopSpace;
cluster -> open closed Element of K10(the carrier of a₁);
coherence by TDLAT_3:18, TDLAT_3:17;

end;

theorem Th47: :: TOPGEN_1:47

for b₁ being discrete TopSpace
for b₂ being Subset of b₁ holds Der b₂ = {}

proof end;

registration

let c₁ be non empty discrete TopSpace;
let c₂ be Subset of c₁;
cluster Der a₂ -> empty open closed dense-in-itself perfect scattered ;
coherence by Th47;

end;

theorem Th48: :: TOPGEN_1:48

for b₁ being non empty discrete TopSpace
for b₂ being Subset of b₁ st b₂ is dense holds
b₂ = [#] b₁

proof end;

definition

let c₁ be TopSpace;
func density c₁ -> cardinal number means :Def12: :: TOPGEN_1:def 12
( ex b₁ being Subset of a₁ st
( b₁ is dense & a₂ = Card b₁ ) & ( for b₁ being Subset of a₁ st b₁ is dense holds
a₂ <=` Card b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines density TOPGEN_1:def 12 :

definition

let c₁ be TopSpace;
attr a₁ is separable means :Def13: :: TOPGEN_1:def 13
density a₁ <=` alef 0;

end;

:: deftheorem Def13 defines separable TOPGEN_1:def 13 :

theorem Th49: :: TOPGEN_1:49

for b₁ being countable TopSpace holds b₁ is separable

proof end;

registration

cluster countable -> separable TopStruct ;
coherence by Th49;

end;

theorem Th50: :: TOPGEN_1:50

for b₁ being Subset of R^1 st b₁ = RAT holds
b₁ ` = IRRAT by BORSUK_5:def 3, BORSUK_5:13, PRE_TOPC:17;

Lemma45: RAT = REAL \ IRRAT

proof end;

theorem Th51: :: TOPGEN_1:51

for b₁ being Subset of R^1 st b₁ = IRRAT holds
b₁ ` = RAT by Lemma45, BORSUK_5:13, PRE_TOPC:17;

theorem Th52: :: TOPGEN_1:52

for b₁ being Subset of R^1 st b₁ = RAT holds
Int b₁ = {}

proof end;

theorem Th53: :: TOPGEN_1:53

for b₁ being Subset of R^1 st b₁ = IRRAT holds
Int b₁ = {}

proof end;

theorem Th54: :: TOPGEN_1:54

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

proof end;

theorem Th55: :: TOPGEN_1:55

for b₁ being Subset of R^1 st b₁ = IRRAT holds
b₁ is dense

proof end;

theorem Th56: :: TOPGEN_1:56

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

proof end;

theorem Th57: :: TOPGEN_1:57

for b₁ being Subset of R^1 st b₁ = IRRAT holds
b₁ is boundary

proof end;

theorem Th58: :: TOPGEN_1:58

for b₁ being Subset of R^1 st b₁ = REAL holds
not b₁ is boundary

proof end;

theorem Th59: :: TOPGEN_1:59

ex b₁, b₂ being Subset of R^1 st
( b₁ is boundary & b₂ is boundary & not b₁ \/ b₂ is boundary )

proof end;