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


begin

theorem Th1: :: TOPGEN_1:1
for T being 1-sorted
for A, B being Subset of T holds
( A meets B ` iff A \ B <> {} )
proofend;

theorem :: TOPGEN_1:2
for T being 1-sorted holds
( T is countable iff card ([#] T) c= omega )
proofend;

registration
let T be finite 1-sorted ;
cluster [#] T ->  finite ;
coherence
 [#] T is finite ;
end;

registration
cluster finite  ->  countable for 1-sorted ;
coherence
 for b1 being 1-sorted st b1 is finite holds
b1 is countable
proofend;
end;

registration
cluster non empty countable for 1-sorted ;
existence
 ex b1 being 1-sorted st
( b1 is countable &amp; not b1 is empty )
proofend;
cluster non empty TopSpace-like countable for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is countable &amp; not b1 is empty )
proofend;
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 b1 being TopSpace st
( b1 is T_1 &amp; not b1 is empty )
proofend;
end;

begin

theorem Th3: :: TOPGEN_1:3
for T being TopSpace
for A being Subset of T holds Int A = (Cl (A `)) `
proofend;

:: 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 &amp; B in F ) );
existence
 ex b1 being Subset-Family of T st
for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Fr B &amp; B in F ) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of T st ( for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Fr B &amp; B in F ) ) ) &amp; ( for A being Subset of T holds
( A in b2 iff ex B being Subset of T st
( A = Fr B &amp; B in F ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Fr TOPGEN_1:def_1_:_
 for T being TopSpace
for F, b3 being Subset-Family of T holds
( b3 = Fr F iff for A being Subset of T holds
( A in b3 iff ex B being Subset of T st
( A = Fr B &amp; B in F ) ) );

theorem :: TOPGEN_1:4
for T being TopSpace
for F being Subset-Family of T st F = {} holds
Fr F = {}
proofend;

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)}
proofend;

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

theorem :: TOPGEN_1:7
for T being TopSpace
for F, G being Subset-Family of T holds Fr (F \/ G) = (Fr F) \/ (Fr G)
proofend;

theorem Th8: :: TOPGEN_1:8
for T being TopStruct
for A being Subset of T holds Fr A = (Cl A) \ (Int A)
proofend;

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 &amp; p in U holds
( A meets U &amp; U \ A <> {} ) )
proofend;

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 &amp; U \ A <> {} ) )
proofend;

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 &amp; U \ A <> {} ) )
proofend;

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))
proofend;

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

theorem Th14: :: TOPGEN_1:14
for T being TopSpace
for A being Subset of T holds
( ( A is open &amp; A is closed ) iff Fr A = {} )
proofend;

begin

:: 1.3.2. Accumulation Points
definition
let T be TopStruct ;
let A be Subset of T;
let x be set ;
predx 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_:_
 for T being TopStruct
for A being Subset of T
for x being set holds
( x is_an_accumulation_point_of A iff x in Cl (A \ {x}) );

theorem Th15: :: TOPGEN_1:15
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
proofend;

:: 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 b1 being Subset of T st
for x being set st x in the carrier of T holds
( x in b1 iff x is_an_accumulation_point_of A )
proofend;
uniqueness
 for b1, b2 being Subset of T st ( for x being set st x in the carrier of T holds
( x in b1 iff x is_an_accumulation_point_of A ) ) &amp; ( for x being set st x in the carrier of T holds
( x in b2 iff x is_an_accumulation_point_of A ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Der TOPGEN_1:def_3_:_
 for T being TopStruct
for A, b3 being Subset of T holds
( b3 = Der A iff for x being set st x in the carrier of T holds
( x in b3 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 set holds
( x in Der A iff x is_an_accumulation_point_of A )
proofend;

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 &amp; x <> y ) )
proofend;

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 &amp; x <> y ) )
proofend;

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 &amp; x <> y ) )
proofend;

begin

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

:: deftheorem Def4 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 &amp; 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 )
proofend;

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 &amp; q in A &amp; q in U ) )
proofend;

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} )
proofend;

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

:: deftheorem Def5 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 )
proofend;

begin

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 &amp; B in F ) );
existence
 ex b1 being Subset-Family of T st
for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Der B &amp; B in F ) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of T st ( for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Der B &amp; B in F ) ) ) &amp; ( for A being Subset of T holds
( A in b2 iff ex B being Subset of T st
( A = Der B &amp; B in F ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines Der TOPGEN_1:def_6_:_
 for T being TopSpace
for F, b3 being Subset-Family of T holds
( b3 = Der F iff for A being Subset of T holds
( A in b3 iff ex B being Subset of T st
( A = Der B &amp; 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 = {}
proofend;

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)}
proofend;

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

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)
proofend;

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

theorem Th29: :: TOPGEN_1:29
for T being TopSpace
for A being Subset of T holds Cl A = A \/ (Der A)
proofend;

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

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)
proofend;

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

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

registration
let T be non empty T_1 TopSpace;
let A be Subset of T;
cluster Der A ->  closed ;
coherence
 Der A is closed
proofend;
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)
proofend;

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 &amp; x is_an_accumulation_point_of A holds
x is_an_accumulation_point_of B
proofend;

begin

definition
let T be TopSpace;
let A be Subset of T;
attrA 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_:_
 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;
attrT 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 &amp; A is dense-in-itself holds
Cl A is dense-in-itself
proofend;

definition
let T be TopSpace;
let F be Subset-Family of T;
attrF 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_:_
 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)
proofend;

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

theorem :: TOPGEN_1:39
for T being non empty TopSpace holds Fr ({} T) = {}
proofend;

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 b1 being Subset of T holds b1 is open by TDLAT_3:15;
cluster non closed for Element of K10( the carrier of T);
existence
 not for b1 being Subset of T holds b1 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;

begin

definition
let T be TopSpace;
let A be Subset of T;
attrA is perfect  means :Def10: :: TOPGEN_1:def 10
( A is closed &amp; A is dense-in-itself );
end;

:: deftheorem Def10 defines perfect TOPGEN_1:def_10_:_
 for T being TopSpace
for A being Subset of T holds
( A is perfect iff ( A is closed &amp; 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 b1 being Subset of T st b1 is perfect holds
( b1 is closed &amp; b1 is dense-in-itself ) by Def10;
cluster closed dense-in-itself  ->  perfect for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is closed &amp; b1 is dense-in-itself holds
b1 is perfect by Def10;
end;

theorem Th40: :: TOPGEN_1:40
for T being TopSpace holds Der ({} T) = {} T
proofend;

Lm1:  for T being TopSpace
for A being Subset of T st A is closed &amp; A is dense-in-itself holds
Der A = A
proofend;

theorem Th41: :: TOPGEN_1:41
for T being TopSpace
for A being Subset of T holds
( A is perfect iff Der A = A )
proofend;

theorem Th42: :: TOPGEN_1:42
for T being TopSpace holds {} T is perfect
proofend;

registration
let T be TopSpace;
cluster empty  ->  perfect for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is empty holds
b1 is perfect
proofend;
end;

registration
let T be TopSpace;
cluster perfect for Element of K10( the carrier of T);
existence
 ex b1 being Subset of T st b1 is perfect
proofend;
end;

begin

definition
let T be TopSpace;
let A be Subset of T;
attrA 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_:_
 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 b1 being Subset of T st not b1 is empty &amp; b1 is scattered holds
not b1 is dense-in-itself by Def11;
cluster non empty dense-in-itself  ->  non scattered for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is dense-in-itself &amp; not b1 is empty holds
not b1 is scattered ;
end;

theorem Th43: :: TOPGEN_1:43
for T being TopSpace holds {} T is scattered
proofend;

registration
let T be TopSpace;
cluster empty  ->  scattered for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is empty holds
b1 is scattered
proofend;
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 &amp; A misses B &amp; A is perfect &amp; B is scattered )
proofend;

registration
let T be discrete TopSpace;
let A be Subset of T;
cluster Fr A ->  empty ;
coherence
 Fr A is empty
proofend;
end;

registration
let T be discrete TopSpace;
cluster  ->  open closed for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T holds
( b1 is closed &amp; b1 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 = {}
proofend;

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;

begin

:: 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 &amp; it = card A ) &amp; ( for B being Subset of T st B is dense holds
it c= card B ) );
existence
 ex b1 being cardinal number st
( ex A being Subset of T st
( A is dense &amp; b1 = card A ) &amp; ( for B being Subset of T st B is dense holds
b1 c= card B ) )
proofend;
uniqueness
 for b1, b2 being cardinal number st ex A being Subset of T st
( A is dense &amp; b1 = card A ) &amp; ( for B being Subset of T st B is dense holds
b1 c= card B ) &amp; ex A being Subset of T st
( A is dense &amp; b2 = card A ) &amp; ( for B being Subset of T st B is dense holds
b2 c= card B ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines density TOPGEN_1:def_12_:_
 for T being TopSpace
for b2 being cardinal number holds
( b2 = density T iff ( ex A being Subset of T st
( A is dense &amp; b2 = card A ) &amp; ( for B being Subset of T st B is dense holds
b2 c= card B ) ) );

:: Separable Spaces
definition
let T be TopSpace;
attrT is separable  means :Def13: :: TOPGEN_1:def 13
 density T c= omega ;
end;

:: deftheorem Def13 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
proofend;

registration
cluster TopSpace-like countable  ->  separable for TopStruct ;
coherence
 for b1 being TopSpace st b1 is countable holds
b1 is separable by Th46;
end;

begin

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

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 = {}
proofend;

theorem :: TOPGEN_1:50
for A being Subset of R^1 st A = IRRAT holds
Int A = {}
proofend;

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

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

theorem Th52: :: TOPGEN_1:52
IRRAT is dense Subset of R^1
proofend;

theorem Th53: :: TOPGEN_1:53
RAT is boundary Subset of R^1
proofend;

theorem Th54: :: TOPGEN_1:54
IRRAT is boundary Subset of R^1
proofend;

theorem Th55: :: TOPGEN_1:55
REAL is non boundary Subset of R^1
proofend;

theorem :: TOPGEN_1:56
ex A, B being Subset of R^1 st
( A is boundary &amp; B is boundary &amp; not A \/ B is boundary )
proofend;