let T be TopSpace;
let F be Subset-Family of T;
func Fr F -> Subset-Family of T means :Def1: :: TOPGEN_1:def 1
for A being Subset of T holds
( A in it iff ex B being Subset of T st
( A = Fr B & B in F ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Fr TOPGEN_1:def 1 :

theorem :: TOPGEN_1:6

for T being TopSpace
for F being Subset-Family of T st F = {} holds
Fr F = {}

proof end;

theorem :: TOPGEN_1:7

for T being TopSpace
for F being Subset-Family of T
for A being Subset of T st F = {A} holds
Fr F = {(Fr A)}

proof end;

theorem Th8: :: TOPGEN_1:8

for T being TopSpace
for F, G being Subset-Family of T st F c= G holds
Fr F c= Fr G

proof end;

theorem :: TOPGEN_1:9

for T being TopSpace
for F, G being Subset-Family of T holds Fr (F \/ G) = (Fr F) \/ (Fr G)

proof end;

theorem Th10: :: TOPGEN_1:10

for T being TopStruct
for A being Subset of T holds Fr A = (Cl A) \ (Int A)

proof end;

theorem Th11: :: TOPGEN_1:11

for T being non empty TopSpace
for A being Subset of T
for p being Point of T holds
( p in Fr A iff for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} ) )

proof end;

theorem :: TOPGEN_1:12

for T being non empty TopSpace
for A being Subset of T
for p being Point of T holds
( p in Fr A iff for B being Basis of p
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )

proof end;

theorem :: TOPGEN_1:13

for T being non empty TopSpace
for A being Subset of T
for p being Point of T holds
( p in Fr A iff ex B being Basis of p st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )

proof end;

theorem :: TOPGEN_1:14

for T being TopSpace
for A, B being Subset of T holds Fr (A /\ B) c= ((Cl A) /\ (Fr B)) \/ ((Fr A) /\ (Cl B))

proof end;

theorem :: TOPGEN_1:15

for T being TopSpace
for A being Subset of T holds the carrier of T = ((Int A) \/ (Fr A)) \/ (Int (A ` ))

proof end;

theorem Th16: :: TOPGEN_1:16

for T being TopSpace
for A being Subset of T holds
( ( A is open & A is closed ) iff Fr A = {} )

proof end;

definition

let T be TopStruct ;
let A be Subset of T;
let x be set ;
pred x is_an_accumulation_point_of A means :Def2: :: TOPGEN_1:def 2
x in Cl (A \ {x});

end;

:: deftheorem Def2 defines is_an_accumulation_point_of TOPGEN_1:def 2 :

theorem Th17: :: TOPGEN_1:17

for T being TopSpace
for A being Subset of T
for x being set st x is_an_accumulation_point_of A holds
x is Point of T

proof end;

definition

let T be TopStruct ;
let A be Subset of T;
func Der A -> Subset of T means :Def3: :: TOPGEN_1:def 3
for x being set st x in the carrier of T holds
( x in it iff x 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 T being non empty TopSpace
for A being Subset of T
for x being set holds
( x in Der A iff x is_an_accumulation_point_of A )

proof end;

theorem Th19: :: TOPGEN_1:19

for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x in Der A iff for U being open Subset of T st x in U holds
ex y being Point of T st
( y in A /\ U & x <> y ) )

proof end;

theorem :: TOPGEN_1:20

for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x in Der A iff for B being Basis of x
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )

proof end;

theorem :: TOPGEN_1:21

for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x in Der A iff ex B being Basis of x st
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )

proof end;

definition

let T be TopSpace;
let A be Subset of T;
let x be set ;
pred x is_isolated_in A means :Def4: :: TOPGEN_1:def 4
( x in A & not x is_an_accumulation_point_of A );

end;

:: deftheorem Def4 defines is_isolated_in TOPGEN_1:def 4 :

theorem :: TOPGEN_1:22

for T being non empty TopSpace
for A being Subset of T
for p being set holds
( p in A \ (Der A) iff p is_isolated_in A )

proof end;

theorem Th23: :: TOPGEN_1:23

for T being non empty TopSpace
for A being Subset of T
for p being Point of T holds
( p is_an_accumulation_point_of A iff for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U ) )

proof end;

theorem Th24: :: TOPGEN_1:24

for T being non empty TopSpace
for A being Subset of T
for p being Point of T holds
( p is_isolated_in A iff ex G being open Subset of T st G /\ A = {p} )

proof end;

definition

let T be TopSpace;
let p be Point of T;
attr p is isolated means :Def5: :: TOPGEN_1:def 5
p is_isolated_in [#] T;

end;

:: deftheorem Def5 defines isolated TOPGEN_1:def 5 :

theorem :: TOPGEN_1:25

for T being non empty TopSpace
for p being Point of T holds
( p is isolated iff {p} is open )

proof end;

definition

let T be TopSpace;
let F be Subset-Family of T;
func Der F -> Subset-Family of T means :Def6: :: TOPGEN_1:def 6
for A being Subset of T holds
( A in it iff ex B being Subset of T st
( A = Der B & B in F ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Der TOPGEN_1:def 6 :

theorem :: TOPGEN_1:26

for T being non empty TopSpace
for F being Subset-Family of T st F = {} holds
Der F = {}

proof end;

theorem :: TOPGEN_1:27

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

proof end;

theorem Th28: :: TOPGEN_1:28

for T being non empty TopSpace
for F, G being Subset-Family of T st F c= G holds
Der F c= Der G

proof end;

theorem :: TOPGEN_1:29

for T being non empty TopSpace
for F, G being Subset-Family of T holds Der (F \/ G) = (Der F) \/ (Der G)

proof end;

theorem Th30: :: TOPGEN_1:30

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

proof end;

theorem Th31: :: TOPGEN_1:31

for T being TopSpace
for A being Subset of T holds Cl A = A \/ (Der A)

proof end;

theorem Th32: :: TOPGEN_1:32

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

proof end;

theorem Th33: :: TOPGEN_1:33

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

proof end;

theorem Th34: :: TOPGEN_1:34

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

proof end;

theorem Th35: :: TOPGEN_1:35

for T being TopSpace
for A being Subset of T st T is being_T1 holds
Cl (Der A) = Der A

proof end;

registration

let T be non empty being_T1 TopSpace;
let A be Subset of T;
cluster Der A -> closed ;
coherence

proof end;

end;

theorem Th36: :: TOPGEN_1:36

for T being non empty TopSpace
for F being Subset-Family of T holds union (Der F) c= Der (union F)

proof end;

theorem :: TOPGEN_1:37

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

proof end;

definition

let T be TopSpace;
let A be Subset of T;
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 T be non empty TopSpace;
attr T is dense-in-itself means :: TOPGEN_1:def 8
[#] T is dense-in-itself;

end;

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

theorem Th38: :: TOPGEN_1:38

for T being non empty TopSpace
for A being Subset of T st T is being_T1 & A is dense-in-itself holds
Cl A is dense-in-itself

proof end;

definition

let T be TopSpace;
let F be Subset-Family of T;
attr F is dense-in-itself means :Def9: :: TOPGEN_1:def 9
for A being Subset of T st A in F holds
A is dense-in-itself;

end;

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

theorem Th39: :: TOPGEN_1:39

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

proof end;

theorem Th40: :: TOPGEN_1:40

for T being non empty TopSpace
for F being Subset-Family of T st F is dense-in-itself holds
union F is dense-in-itself

proof end;

theorem :: TOPGEN_1:41

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

proof end;

registration

let T be TopSpace;
let A be open closed Subset of T;
cluster Fr A -> empty ;
coherence by Th16;

end;

registration

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

end;

registration

let T be non empty non discrete TopSpace;
let A be non open Subset of T;
cluster Fr A -> non empty ;
coherence by Th16;

end;

registration

let T be non empty non discrete TopSpace;
let A be non closed Subset of T;
cluster Fr A -> non empty ;
coherence by Th16;

end;

definition

let T be TopSpace;
let A be Subset of T;
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 T be TopSpace;
cluster perfect -> closed dense-in-itself Element of K10(the carrier of T);
coherence by Def10;
cluster closed dense-in-itself -> perfect Element of K10(the carrier of T);
coherence by Def10;

end;

theorem Th42: :: TOPGEN_1:42

for T being TopSpace holds Der ({} T) = {} T

proof end;

Lm2: for T being TopSpace
for A being Subset of T st A is closed & A is dense-in-itself holds
Der A = A

proof end;

theorem Th43: :: TOPGEN_1:43

for T being TopSpace
for A being Subset of T holds
( A is perfect iff Der A = A )

proof end;

theorem Th44: :: TOPGEN_1:44

for T being TopSpace holds {} T is perfect

proof end;

registration

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

proof end;

end;

registration

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

proof end;

end;

definition

let T be TopSpace;
let A be Subset of T;
attr A is scattered means :Def11: :: TOPGEN_1:def 11
for B being Subset of T 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 T be non empty TopSpace;
cluster non empty scattered -> non dense-in-itself Element of K10(the carrier of T);
coherence by Def11;
cluster non empty dense-in-itself -> non scattered Element of K10(the carrier of T);
coherence by Def11;

end;

theorem Th45: :: TOPGEN_1:45

for T being TopSpace holds {} T is scattered

proof end;

registration

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

proof end;

end;

theorem :: TOPGEN_1:46

for T being non empty TopSpace st T is being_T1 holds
ex A, B being Subset of T st
( A \/ B = [#] T & A misses B & A is perfect & B is scattered )

proof end;

registration

let T be discrete TopSpace;
let A be Subset of T;
cluster Fr A -> empty closed dense-in-itself perfect scattered ;
coherence

proof end;

end;

registration

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

end;

theorem Th47: :: TOPGEN_1:47

for T being discrete TopSpace
for A being Subset of T holds Der A = {}

proof end;

registration

let T be non empty discrete TopSpace;
let A be Subset of T;
cluster Der A -> empty open closed dense-in-itself perfect scattered ;
coherence by Th47;

end;

theorem :: TOPGEN_1:48

for T being non empty discrete TopSpace
for A being Subset of T st A is dense holds
A = [#] T

proof end;

definition

let T be TopSpace;
func density T -> cardinal number means :Def12: :: TOPGEN_1:def 12
( ex A being Subset of T st
( A is dense & it = Card A ) & ( for B being Subset of T st B is dense holds
it <=` Card B ) );
existence

proof end;