:: On the Boundary and Derivative of a Set
:: by Adam Grabowski
::
:: Received November 8, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

theorem Th1: :: TOPGEN_1:1

for T being 1-sorted
for A, B being Subset of T holds
( A meets B ` iff A \ B <> {} ) by SUBSET_1:13;

theorem :: TOPGEN_1:2

for T being 1-sorted holds
( T is countable iff card ([#] T) c= omega ) by CARD_3:def 14, ORDERS_4:def 2;

registration

let T be finite 1-sorted ;

cluster [#] T -> finite ;

coherence
[#] T is finite ;

end;

registration

cluster finite -> countable for 1-sorted ;

coherence
for b₁ being 1-sorted st b₁ is finite holds
b₁ is countable

proof end;

end;

registration

cluster non empty countable for 1-sorted ;

existence
ex b₁ being 1-sorted st
( b₁ is countable & not b₁ is empty )

proof end;

cluster non empty TopSpace-like countable for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is countable & not b₁ is empty )

proof end;

end;

registration

let T be countable 1-sorted ;

cluster [#] T -> countable ;

coherence
[#] T is countable by ORDERS_4:def 2;

end;

registration

cluster non empty TopSpace-like T_1 for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is T_1 & not b₁ is empty )

proof end;

end;

theorem Th3: :: TOPGEN_1:3

for T being TopSpace
for A being Subset of T holds Int A = (Cl (A `)) `

proof end;

:: Collective Boundary

definition

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
ex b₁ being Subset-Family of T st
for A being Subset of T holds
( A in b₁ iff ex B being Subset of T st
( A = Fr B & B in F ) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of T st ( for A being Subset of T holds
( A in b₁ iff ex B being Subset of T st
( A = Fr B & B in F ) ) ) & ( for A being Subset of T holds
( A in b₂ iff ex B being Subset of T st
( A = Fr B & B in F ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Fr TOPGEN_1:def 1 :
for T being TopSpace
for F, b₃ being Subset-Family of T holds
( b₃ = Fr F iff for A being Subset of T holds
( A in b₃ iff ex B being Subset of T st
( A = Fr B & B in F ) ) );

theorem :: TOPGEN_1:4

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

proof end;

theorem :: TOPGEN_1:5

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 Th6: :: TOPGEN_1:6

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

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

proof end;

theorem Th8: :: TOPGEN_1:8

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

proof end;

theorem Th9: :: TOPGEN_1:9

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

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
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )

proof end;

theorem :: 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 ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )

proof end;

theorem :: TOPGEN_1:12

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

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

proof end;

theorem Th14: :: TOPGEN_1:14

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

proof end;

:: 1.3.2. Accumulation Points

definition

let T be TopStruct ;
let A be Subset of T;
let x be object ;

pred x is_an_accumulation_point_of A means :: TOPGEN_1:def 2
x in Cl (A \ {x});

end;

:: deftheorem defines is_an_accumulation_point_of TOPGEN_1:def 2 :
for T being TopStruct
for A being Subset of T
for x being object holds
( x is_an_accumulation_point_of A iff x in Cl (A \ {x}) );

theorem :: TOPGEN_1:15

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

:: Derivative of a Set

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
ex b₁ being Subset of T st
for x being set st x in the carrier of T holds
( x in b₁ iff x is_an_accumulation_point_of A )

proof end;

uniqueness
for b₁, b₂ being Subset of T st ( for x being set st x in the carrier of T holds
( x in b₁ iff x is_an_accumulation_point_of A ) ) & ( for x being set st x in the carrier of T holds
( x in b₂ iff x is_an_accumulation_point_of A ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Der TOPGEN_1:def 3 :
for T being TopStruct
for A, b₃ being Subset of T holds
( b₃ = Der A iff for x being set st x in the carrier of T holds
( x in b₃ iff x is_an_accumulation_point_of A ) );

:: 1.3.3. Characterizations of a Derivative

theorem Th16: :: TOPGEN_1:16

for T being non empty TopSpace
for A being Subset of T
for x being object holds
( x in Der A iff x is_an_accumulation_point_of A ) by Def3;

theorem Th17: :: TOPGEN_1:17

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

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
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: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 ex B being Basis of 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 :: TOPGEN_1:def 4
( x in A & not x is_an_accumulation_point_of A );

end;

:: deftheorem defines is_isolated_in TOPGEN_1:def 4 :
for T being TopSpace
for A being Subset of T
for x being set holds
( x is_isolated_in A iff ( x in A & not x is_an_accumulation_point_of A ) );

theorem :: TOPGEN_1:20

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 Th21: :: TOPGEN_1:21

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 Th22: :: TOPGEN_1:22

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 :: TOPGEN_1:def 5
p is_isolated_in [#] T;

end;

:: deftheorem defines isolated TOPGEN_1:def 5 :
for T being TopSpace
for p being Point of T holds
( p is isolated iff p is_isolated_in [#] T );

theorem :: TOPGEN_1:23

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
ex b₁ being Subset-Family of T st
for A being Subset of T holds
( A in b₁ iff ex B being Subset of T st
( A = Der B & B in F ) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of T st ( for A being Subset of T holds
( A in b₁ iff ex B being Subset of T st
( A = Der B & B in F ) ) ) & ( for A being Subset of T holds
( A in b₂ iff ex B being Subset of T st
( A = Der B & B in F ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Der TOPGEN_1:def 6 :
for T being TopSpace
for F, b₃ being Subset-Family of T holds
( b₃ = Der F iff for A being Subset of T holds
( A in b₃ iff ex B being Subset of T st
( A = Der B & B in F ) ) );

theorem :: TOPGEN_1:24

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

proof end;

theorem :: TOPGEN_1:25

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 Th26: :: TOPGEN_1:26

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

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

proof end;

:: 1.3.4. Properties of a Derivative of a Set

theorem Th28: :: TOPGEN_1:28

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

proof end;

theorem Th29: :: TOPGEN_1:29

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

proof end;

theorem Th30: :: TOPGEN_1:30

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 Th31: :: TOPGEN_1:31

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

proof end;

theorem Th32: :: TOPGEN_1:32

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

proof end;

theorem Th33: :: TOPGEN_1:33

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

proof end;

registration

let T be non empty T_1 TopSpace;
let A be Subset of T;

cluster Der A -> closed ;

coherence
Der A is closed

proof end;

end;

theorem Th34: :: TOPGEN_1:34

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

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 :: TOPGEN_1:def 7
A c= Der A;

end;

:: deftheorem defines dense-in-itself TOPGEN_1:def 7 :
for T being TopSpace
for A being Subset of T holds
( A is dense-in-itself iff A c= Der A );

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 :
for T being non empty TopSpace holds
( T is dense-in-itself iff [#] T is dense-in-itself );

theorem Th36: :: TOPGEN_1:36

for T being non empty TopSpace
for A being Subset of T st T is T_1 & 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 :: TOPGEN_1:def 9
for A being Subset of T st A in F holds
A is dense-in-itself ;

end;

:: deftheorem defines dense-in-itself TOPGEN_1:def 9 :
for T being TopSpace
for F being Subset-Family of T holds
( F is dense-in-itself iff for A being Subset of T st A in F holds
A is dense-in-itself );

theorem Th37: :: TOPGEN_1:37

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 Th38: :: TOPGEN_1:38

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

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
Fr A is empty by Th14;

end;

registration

let T be non empty non discrete TopSpace;

cluster non open for Element of K10( the carrier of T);

existence
not for b₁ being Subset of T holds b₁ is open by TDLAT_3:15;

cluster non closed for Element of K10( the carrier of T);

existence
not for b₁ being Subset of T holds b₁ is closed by TDLAT_3:16;

end;

registration

let T be non empty non discrete TopSpace;
let A be non open Subset of T;

cluster Fr A -> non empty ;

coherence
not Fr A is empty by Th14;

end;

registration

let T be non empty non discrete TopSpace;
let A be non closed Subset of T;

cluster Fr A -> non empty ;

coherence
not Fr A is empty by Th14;

end;

definition

let T be TopSpace;
let A be Subset of T;

attr A is perfect means :: TOPGEN_1:def 10
( A is closed & A is dense-in-itself );

end;

:: deftheorem defines perfect TOPGEN_1:def 10 :
for T being TopSpace
for A being Subset of T holds
( A is perfect iff ( A is closed & A is dense-in-itself ) );

registration

let T be TopSpace;

cluster perfect -> closed dense-in-itself for Element of K10( the carrier of T);

coherence
for b₁ being Subset of T st b₁ is perfect holds
( b₁ is closed & b₁ is dense-in-itself ) ;

cluster closed dense-in-itself -> perfect for Element of K10( the carrier of T);

coherence
for b₁ being Subset of T st b₁ is closed & b₁ is dense-in-itself holds
b₁ is perfect ;

end;

theorem Th40: :: TOPGEN_1:40

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

proof end;

Lm1: 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 Th41: :: TOPGEN_1:41

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

proof end;

theorem Th42: :: TOPGEN_1:42

for T being TopSpace holds {} T is perfect

proof end;

registration

let T be TopSpace;

cluster empty -> perfect for Element of K10( the carrier of T);

coherence
for b₁ being Subset of T st b₁ is empty holds
b₁ is perfect

proof end;

end;

registration

let T be TopSpace;

cluster perfect for Element of K10( the carrier of T);

existence
ex b₁ being Subset of T st b₁ is perfect

proof end;

end;

definition

let T be TopSpace;
let A be Subset of T;

attr A is scattered means :: 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 defines scattered TOPGEN_1:def 11 :
for T being TopSpace
for A being Subset of T holds
( A is scattered iff for B being Subset of T holds
( B is empty or not B c= A or not B is dense-in-itself ) );

registration

let T be non empty TopSpace;

cluster non empty scattered -> non dense-in-itself for Element of K10( the carrier of T);

coherence
for b₁ being Subset of T st not b₁ is empty & b₁ is scattered holds
not b₁ is dense-in-itself ;

cluster non empty dense-in-itself -> non scattered for Element of K10( the carrier of T);

coherence
for b₁ being Subset of T st b₁ is dense-in-itself & not b₁ is empty holds
not b₁ is scattered ;

end;

theorem :: TOPGEN_1:43

for T being TopSpace holds {} T is scattered ;

registration

let T be TopSpace;

cluster empty -> scattered for Element of K10( the carrier of T);

coherence
for b₁ being Subset of T st b₁ is empty holds
b₁ is scattered ;

end;

theorem :: TOPGEN_1:44

for T being non empty TopSpace st T is T_1 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 ;

coherence
Fr A is empty

proof end;

end;

registration

let T be discrete TopSpace;

cluster -> open closed for Element of K10( the carrier of T);

coherence
for b₁ being Subset of T holds
( b₁ is closed & b₁ is open ) by TDLAT_3:15, TDLAT_3:16;

end;

theorem Th45: :: TOPGEN_1:45

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 ;

coherence
Der A is empty by Th45;

end;

:: 1.3.6. Density of a Topological Space

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 c= card B ) );

existence
ex b₁ being cardinal number st
( ex A being Subset of T st
( A is dense & b₁ = card A ) & ( for B being Subset of T st B is dense holds
b₁ c= card B ) )

proof end;

uniqueness
for b₁, b₂ being cardinal number st ex A being Subset of T st
( A is dense & b₁ = card A ) & ( for B being Subset of T st B is dense holds
b₁ c= card B ) & ex A being Subset of T st
( A is dense & b₂ = card A ) & ( for B being Subset of T st B is dense holds
b₂ c= card B ) holds
b₁ = b₂ ;

end;

:: deftheorem Def12 defines density TOPGEN_1:def 12 :
for T being TopSpace
for b₂ being cardinal number holds
( b₂ = density T iff ( ex A being Subset of T st
( A is dense & b₂ = card A ) & ( for B being Subset of T st B is dense holds
b₂ c= card B ) ) );

:: Separable Spaces

definition

let T be TopSpace;

attr T is separable means :: TOPGEN_1:def 13
density T c= omega ;

end;

:: deftheorem defines separable TOPGEN_1:def 13 :
for T being TopSpace holds
( T is separable iff density T c= omega );

theorem Th46: :: TOPGEN_1:46

for T being countable TopSpace holds T is separable

proof end;

registration

cluster TopSpace-like countable -> separable for TopStruct ;

coherence
for b₁ being TopSpace st b₁ is countable holds
b₁ is separable by Th46;

end;

theorem :: TOPGEN_1:47

for A being Subset of R^1 st A = RAT holds
A ` = IRRAT by BORSUK_5:def 1, TOPMETR:17;

Lm2: RAT = REAL \ IRRAT

proof end;

theorem :: TOPGEN_1:48

for A being Subset of R^1 st A = IRRAT holds
A ` = RAT by Lm2, TOPMETR:17;

theorem :: TOPGEN_1:49

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

proof end;

theorem :: TOPGEN_1:50

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

proof end;

reconsider B = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17;

theorem Th51: :: TOPGEN_1:51

RAT is dense Subset of R^1

proof end;

reconsider A = IRRAT as Subset of R^1 by TOPMETR:17;

theorem Th52: :: TOPGEN_1:52

IRRAT is dense Subset of R^1

proof end;

theorem Th53: :: TOPGEN_1:53

RAT is boundary Subset of R^1

proof end;

theorem Th54: :: TOPGEN_1:54

IRRAT is boundary Subset of R^1

proof end;

theorem Th55: :: TOPGEN_1:55

REAL is non boundary Subset of R^1

proof end;

theorem :: TOPGEN_1:56

ex A, B being Subset of R^1 st
( A is boundary & B is boundary & not A \/ B is boundary )

proof end;