:: by Adam Grabowski

::

:: Received November 8, 2004

:: Copyright (c) 2004-2018 Association of Mizar Users

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;

( T is countable iff card ([#] T) c= omega ) by CARD_3:def 14, ORDERS_4:def 2;

registration
end;

registration

existence

ex b_{1} being 1-sorted st

( b_{1} is countable & not b_{1} is empty )

ex b_{1} being TopSpace st

( b_{1} is countable & not b_{1} is empty )

end;
ex b

( b

proof end;

existence ex b

( b

proof end;

registration
end;

:: Collective Boundary

definition

let T be TopSpace;

let F be Subset-Family of T;

ex b_{1} being Subset-Family of T st

for A being Subset of T holds

( A in b_{1} iff ex B being Subset of T st

( A = Fr B & B in F ) )

for b_{1}, b_{2} being Subset-Family of T st ( for A being Subset of T holds

( A in b_{1} iff ex B being Subset of T st

( A = Fr B & B in F ) ) ) & ( for A being Subset of T holds

( A in b_{2} iff ex B being Subset of T st

( A = Fr B & B in F ) ) ) holds

b_{1} = b_{2}

end;
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 for A being Subset of T holds

( A in it iff ex B being Subset of T st

( A = Fr B & B in F ) );

ex b

for A being Subset of T holds

( A in b

( A = Fr B & B in F ) )

proof end;

uniqueness for b

( A in b

( A = Fr B & B in F ) ) ) & ( for A being Subset of T holds

( A in b

( A = Fr B & B in F ) ) ) holds

b

proof end;

:: deftheorem Def1 defines Fr TOPGEN_1:def 1 :

for T being TopSpace

for F, b_{3} being Subset-Family of T holds

( b_{3} = Fr F iff for A being Subset of T holds

( A in b_{3} iff ex B being Subset of T st

( A = Fr B & B in F ) ) );

for T being TopSpace

for F, b

( b

( A in b

( A = Fr B & B in F ) ) );

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

for F being Subset-Family of T

for A being Subset of T st F = {A} holds

Fr F = {(Fr 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 <> {} ) )

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 <> {} ) )

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 <> {} ) )

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

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

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

proof end;

:: 1.3.2. Accumulation Points

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

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 ;

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;

ex b_{1} being Subset of T st

for x being set st x in the carrier of T holds

( x in b_{1} iff x is_an_accumulation_point_of A )

for b_{1}, b_{2} being Subset of T st ( for x being set st x in the carrier of T holds

( x in b_{1} iff x is_an_accumulation_point_of A ) ) & ( for x being set st x in the carrier of T holds

( x in b_{2} iff x is_an_accumulation_point_of A ) ) holds

b_{1} = b_{2}

end;
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 for x being set st x in the carrier of T holds

( x in it iff x is_an_accumulation_point_of A );

ex b

for x being set st x in the carrier of T holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def3 defines Der TOPGEN_1:def 3 :

for T being TopStruct

for A, b_{3} being Subset of T holds

( b_{3} = Der A iff for x being set st x in the carrier of T holds

( x in b_{3} iff x is_an_accumulation_point_of A ) );

for T being TopStruct

for A, b

( b

( x in b

:: 1.3.3. Characterizations of a Derivative

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

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

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

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;

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

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 )

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

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

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;

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

for T being TopSpace

for p being Point of T holds

( p is isolated iff p is_isolated_in [#] T );

definition

let T be TopSpace;

let F be Subset-Family of T;

ex b_{1} being Subset-Family of T st

for A being Subset of T holds

( A in b_{1} iff ex B being Subset of T st

( A = Der B & B in F ) )

for b_{1}, b_{2} being Subset-Family of T st ( for A being Subset of T holds

( A in b_{1} iff ex B being Subset of T st

( A = Der B & B in F ) ) ) & ( for A being Subset of T holds

( A in b_{2} iff ex B being Subset of T st

( A = Der B & B in F ) ) ) holds

b_{1} = b_{2}

end;
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 for A being Subset of T holds

( A in it iff ex B being Subset of T st

( A = Der B & B in F ) );

ex b

for A being Subset of T holds

( A in b

( A = Der B & B in F ) )

proof end;

uniqueness for b

( A in b

( A = Der B & B in F ) ) ) & ( for A being Subset of T holds

( A in b

( A = Der B & B in F ) ) ) holds

b

proof end;

:: deftheorem Def6 defines Der TOPGEN_1:def 6 :

for T being TopSpace

for F, b_{3} being Subset-Family of T holds

( b_{3} = Der F iff for A being Subset of T holds

( A in b_{3} iff ex B being Subset of T st

( A = Der B & B in F ) ) );

for T being TopSpace

for F, b

( b

( A in b

( A = Der B & B in F ) ) );

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

for A being Subset of T

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

Der F = {(Der A)}

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)

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

registration
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

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;

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

for T being TopSpace

for A being Subset of T holds

( A is dense-in-itself iff A c= Der A );

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

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

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;

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

for A being Subset of T st A in F holds

A is dense-in-itself ;

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

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)

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

for F being Subset-Family of T st F is dense-in-itself holds

union F is dense-in-itself

proof end;

registration
end;

registration

let T be non empty non discrete TopSpace;

existence

not for b_{1} being Subset of T holds b_{1} is open
by TDLAT_3:15;

existence

not for b_{1} being Subset of T holds b_{1} is closed
by TDLAT_3:16;

end;
existence

not for b

existence

not for b

registration

let T be non empty non discrete TopSpace;

let A be non open Subset of T;

coherence

not Fr A is empty by Th14;

end;
let A be non open Subset of T;

coherence

not Fr A is empty by Th14;

registration

let T be non empty non discrete TopSpace;

let A be non closed Subset of T;

coherence

not Fr A is empty by Th14;

end;
let A be non closed Subset of T;

coherence

not Fr A is empty by Th14;

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

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 b_{1} being Subset of T st b_{1} is perfect holds

( b_{1} is closed & b_{1} is dense-in-itself )
;

coherence

for b_{1} being Subset of T st b_{1} is closed & b_{1} is dense-in-itself holds

b_{1} is perfect
;

end;
coherence

for b

( b

coherence

for b

b

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;

registration

let T be TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is empty holds

b_{1} is perfect

end;
coherence

for b

b

proof end;

registration
end;

definition

let T be TopSpace;

let A be Subset of T;

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

for B being Subset of T holds

( B is empty or not B c= A or not B is dense-in-itself );

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

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;

coherence

for b_{1} being Subset of T st not b_{1} is empty & b_{1} is scattered holds

not b_{1} is dense-in-itself
;

coherence

for b_{1} being Subset of T st b_{1} is dense-in-itself & not b_{1} is empty holds

not b_{1} is scattered
;

end;
coherence

for b

not b

coherence

for b

not b

registration

let T be TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is empty holds

b_{1} is scattered
;

end;
coherence

for b

b

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 )

ex A, B being Subset of T st

( A \/ B = [#] T & A misses B & A is perfect & B is scattered )

proof end;

registration
end;

registration

let T be discrete TopSpace;

coherence

for b_{1} being Subset of T holds

( b_{1} is closed & b_{1} is open )
by TDLAT_3:15, TDLAT_3:16;

end;
coherence

for b

( b

registration
end;

:: 1.3.6. Density of a Topological Space

definition

let T be TopSpace;

ex b_{1} being cardinal number st

( ex A being Subset of T st

( A is dense & b_{1} = card A ) & ( for B being Subset of T st B is dense holds

b_{1} c= card B ) )

for b_{1}, b_{2} being cardinal number st ex A being Subset of T st

( A is dense & b_{1} = card A ) & ( for B being Subset of T st B is dense holds

b_{1} c= card B ) & ex A being Subset of T st

( A is dense & b_{2} = card A ) & ( for B being Subset of T st B is dense holds

b_{2} c= card B ) holds

b_{1} = b_{2}
;

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

ex b

( ex A being Subset of T st

( A is dense & b

b

proof end;

uniqueness for b

( A is dense & b

b

( A is dense & b

b

b

:: deftheorem Def12 defines density TOPGEN_1:def 12 :

for T being TopSpace

for b_{2} being cardinal number holds

( b_{2} = density T iff ( ex A being Subset of T st

( A is dense & b_{2} = card A ) & ( for B being Subset of T st B is dense holds

b_{2} c= card B ) ) );

for T being TopSpace

for b

( b

( A is dense & b

b

:: Separable Spaces

definition
end;

:: deftheorem defines separable TOPGEN_1:def 13 :

for T being TopSpace holds

( T is separable iff density T c= omega );

for T being TopSpace holds

( T is separable iff density T c= omega );

registration
end;

theorem :: TOPGEN_1:47

Lm2: RAT = REAL \ IRRAT

proof end;

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

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