:: On the Boundary and Derivative of a Set
::
:: Copyright (c) 2004-2018 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 ;

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

registration
coherence
for b1 being 1-sorted st b1 is finite holds
b1 is countable
proof end;
end;

registration
existence
ex b1 being 1-sorted st
( b1 is countable & not b1 is empty )
proof end;
existence
ex b1 being TopSpace st
( b1 is countable & not b1 is empty )
proof end;
end;

registration
let T be countable 1-sorted ;
coherence
[#] T is countable
by ORDERS_4:def 2;
end;

registration
existence
ex b1 being TopSpace st
( b1 is T_1 & not b1 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 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 & B in F ) )
proof end;
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 & B in F ) ) ) & ( for A being Subset of T holds
( A in b2 iff ex B being Subset of T st
( A = Fr B & B in F ) ) ) holds
b1 = b2
proof end;
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 & 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 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 )
proof end;
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 ) ) & ( 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
proof end;
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 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;
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 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 & B in F ) )
proof end;
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 & B in F ) ) ) & ( for A being Subset of T holds
( A in b2 iff ex B being Subset of T st
( A = Der B & B in F ) ) ) holds
b1 = b2
proof end;
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 & 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 ()
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;
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 Subset of T;
existence
not for b1 being Subset of T holds b1 is open
by TDLAT_3:15;
cluster non closed for Subset 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;

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;
coherence
for b1 being Subset of T st b1 is perfect holds
( b1 is closed & b1 is dense-in-itself )
;
coherence
for b1 being Subset of T st b1 is closed & b1 is dense-in-itself holds
b1 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 Subset of T;
coherence
for b1 being Subset of T st b1 is empty holds
b1 is perfect
proof end;
end;

registration
let T be TopSpace;
cluster perfect for Subset of T;
existence
ex b1 being Subset of T st b1 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 Subset of T;
coherence
for b1 being Subset of T st not b1 is empty & b1 is scattered holds
not b1 is dense-in-itself
;
cluster non empty dense-in-itself -> non scattered for Subset of T;
coherence
for b1 being Subset of T st b1 is dense-in-itself & not b1 is empty holds
not b1 is scattered
;
end;

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

registration
let T be TopSpace;
cluster empty -> scattered for Subset of T;
coherence
for b1 being Subset of T st b1 is empty holds
b1 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 Subset of T;
coherence
for b1 being Subset of T holds
( b1 is closed & b1 is open )
by ;
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 b1 being cardinal number st
( ex A being Subset of T st
( A is dense & b1 = card A ) & ( for B being Subset of T st B is dense holds
b1 c= card B ) )
proof end;
uniqueness
for b1, b2 being cardinal number st ex A being Subset of T st
( A is dense & b1 = card A ) & ( for B being Subset of T st B is dense holds
b1 c= card B ) & ex A being Subset of T st
( A is dense & b2 = card A ) & ( for B being Subset of T st B is dense holds
b2 c= card B ) holds
b1 = b2
;
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 & b2 = card A ) & ( for B being Subset of T st B is dense holds
b2 c= card B ) ) );

:: Separable Spaces
definition
let T be TopSpace;
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
coherence
for b1 being TopSpace st b1 is countable holds
b1 is separable
by Th46;
end;

theorem :: TOPGEN_1:47
for A being Subset of R^1 st A = RAT holds
A  = IRRAT by ;

Lm2:
proof end;

theorem :: TOPGEN_1:48
for A being Subset of R^1 st A = IRRAT holds
A  = RAT by ;

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 ;

theorem Th51: :: TOPGEN_1:51
proof end;

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

theorem Th52: :: TOPGEN_1:52
proof end;

theorem Th53: :: TOPGEN_1:53
proof end;

theorem Th54: :: TOPGEN_1:54
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;