:: by Adam Grabowski

::

:: Received August 30, 2005

:: Copyright (c) 2005-2012 Association of Mizar Users

begin

definition
end;

:: deftheorem defines TotFam TOPGEN_4:def 1 :

for T being 1-sorted holds TotFam T = bool the carrier of T;

for T being 1-sorted holds TotFam T = bool the carrier of T;

theorem Th1: :: TOPGEN_4:1

for T being set

for F being Subset-Family of T holds

( F is countable iff COMPLEMENT F is countable )

for F being Subset-Family of T holds

( F is countable iff COMPLEMENT F is countable )

proof end;

registration
end;

Lm1: for X being set holds

( X is countable iff ex f being Function st

( dom f = RAT & X c= rng f ) )

proof end;

theorem :: TOPGEN_4:2

for T being non empty TopSpace

for A being Subset of T holds Der A = { x where x is Point of T : x in Cl (A \ {x}) }

for A being Subset of T holds Der A = { x where x is Point of T : x in Cl (A \ {x}) }

proof end;

registration
end;

registration

coherence

for b_{1} being set st not b_{1} is countable holds

not b_{1} is finite
;

coherence

for b_{1} being set st not b_{1} is finite holds

not b_{1} is trivial
;

existence

ex b_{1} being set st

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

end;
for b

not b

coherence

for b

not b

existence

ex b

( not b

proof end;

theorem Th4: :: TOPGEN_4:4

for T being non empty TopStruct

for B being Basis of T

for V being Subset of T st V is open & V <> {} holds

ex W being Subset of T st

( W in B & W c= V & W <> {} )

for B being Basis of T

for V being Subset of T st V is open & V <> {} holds

ex W being Subset of T st

( W in B & W c= V & W <> {} )

proof end;

begin

:: 1.3.7. Theorem

theorem :: TOPGEN_4:6

for T being non empty TopSpace holds

( T is separable iff ex A being Subset of T st

( A is dense & A is countable ) )

( T is separable iff ex A being Subset of T st

( A is dense & A is countable ) )

proof end;

:: 1.3.8. Corollary

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is second-countable holds

b_{1} is separable
by Th7;

end;
for b

b

:: Exercises

theorem :: TOPGEN_4:8

for T being non empty TopSpace

for A, B being Subset of T st A,B are_separated holds

Fr (A \/ B) = (Fr A) \/ (Fr B)

for A, B being Subset of T st A,B are_separated holds

Fr (A \/ B) = (Fr A) \/ (Fr B)

proof end;

:: Exercise 1.3.B.

theorem :: TOPGEN_4:9

for T being non empty TopSpace

for F being Subset-Family of T st F is locally_finite holds

Fr (union F) c= union (Fr F)

for F being Subset-Family of T st F is locally_finite holds

Fr (union F) c= union (Fr F)

proof end;

begin

definition

let T be non empty TopSpace;

let F be Subset-Family of T;

end;
let F be Subset-Family of T;

attr F is all-open-containing means :Def2: :: TOPGEN_4:def 2

for A being Subset of T st A is open holds

A in F;

for A being Subset of T st A is open holds

A in F;

:: deftheorem Def2 defines all-open-containing TOPGEN_4:def 2 :

for T being non empty TopSpace

for F being Subset-Family of T holds

( F is all-open-containing iff for A being Subset of T st A is open holds

A in F );

for T being non empty TopSpace

for F being Subset-Family of T holds

( F is all-open-containing iff for A being Subset of T st A is open holds

A in F );

definition

let T be non empty TopSpace;

let F be Subset-Family of T;

end;
let F be Subset-Family of T;

attr F is all-closed-containing means :Def3: :: TOPGEN_4:def 3

for A being Subset of T st A is closed holds

A in F;

for A being Subset of T st A is closed holds

A in F;

:: deftheorem Def3 defines all-closed-containing TOPGEN_4:def 3 :

for T being non empty TopSpace

for F being Subset-Family of T holds

( F is all-closed-containing iff for A being Subset of T st A is closed holds

A in F );

for T being non empty TopSpace

for F being Subset-Family of T holds

( F is all-closed-containing iff for A being Subset of T st A is closed holds

A in F );

definition

let T be set ;

let F be Subset-Family of T;

end;
let F be Subset-Family of T;

attr F is closed_for_countable_unions means :Def4: :: TOPGEN_4:def 4

for G being countable Subset-Family of T st G c= F holds

union G in F;

for G being countable Subset-Family of T st G c= F holds

union G in F;

:: deftheorem Def4 defines closed_for_countable_unions TOPGEN_4:def 4 :

for T being set

for F being Subset-Family of T holds

( F is closed_for_countable_unions iff for G being countable Subset-Family of T st G c= F holds

union G in F );

for T being set

for F being Subset-Family of T holds

( F is closed_for_countable_unions iff for G being countable Subset-Family of T st G c= F holds

union G in F );

Lm2: for T being set

for F being Subset-Family of T st F is SigmaField of T holds

F is closed_for_countable_unions

proof end;

registration

let T be set ;

for b_{1} being SigmaField of T holds b_{1} is closed_for_countable_unions
by Lm2;

end;
cluster non empty compl-closed sigma-multiplicative -> closed_for_countable_unions for Element of bool (bool T);

coherence for b

registration

let T be set ;

coherence

for b_{1} being Subset-Family of T st b_{1} is closed_for_countable_unions holds

not b_{1} is empty
by Th12;

end;
coherence

for b

not b

theorem Th13: :: TOPGEN_4:13

for T being set

for F being Subset-Family of T holds

( F is SigmaField of T iff ( F is compl-closed & F is closed_for_countable_unions ) )

for F being Subset-Family of T holds

( F is SigmaField of T iff ( F is compl-closed & F is closed_for_countable_unions ) )

proof end;

definition

let T be set ;

let F be Subset-Family of T;

end;
let F be Subset-Family of T;

attr F is closed_for_countable_meets means :Def5: :: TOPGEN_4:def 5

for G being countable Subset-Family of T st G c= F holds

meet G in F;

for G being countable Subset-Family of T st G c= F holds

meet G in F;

:: deftheorem Def5 defines closed_for_countable_meets TOPGEN_4:def 5 :

for T being set

for F being Subset-Family of T holds

( F is closed_for_countable_meets iff for G being countable Subset-Family of T st G c= F holds

meet G in F );

for T being set

for F being Subset-Family of T holds

( F is closed_for_countable_meets iff for G being countable Subset-Family of T st G c= F holds

meet G in F );

theorem Th14: :: TOPGEN_4:14

for T being non empty TopSpace

for F being Subset-Family of T holds

( F is all-closed-containing & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )

for F being Subset-Family of T holds

( F is all-closed-containing & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )

proof end;

theorem Th16: :: TOPGEN_4:16

for T being set

for F, G being Subset-Family of T st F c= G & G is compl-closed holds

COMPLEMENT F c= G

for F, G being Subset-Family of T st F c= G & G is compl-closed holds

COMPLEMENT F c= G

proof end;

theorem Th17: :: TOPGEN_4:17

for T being set

for F being Subset-Family of T holds

( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )

for F being Subset-Family of T holds

( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )

proof end;

registration

let T be non empty TopSpace;

for b_{1} being Subset-Family of T st b_{1} is all-open-containing & b_{1} is compl-closed & b_{1} is closed_for_countable_unions holds

( b_{1} is all-closed-containing & b_{1} is closed_for_countable_meets )
by Th14, Th17;

for b_{1} being Subset-Family of T st b_{1} is all-closed-containing & b_{1} is compl-closed & b_{1} is closed_for_countable_meets holds

( b_{1} is all-open-containing & b_{1} is closed_for_countable_unions )
by Th14, Th17;

end;
cluster compl-closed all-open-containing closed_for_countable_unions -> all-closed-containing closed_for_countable_meets for Element of bool (bool the carrier of T);

coherence for b

( b

cluster compl-closed all-closed-containing closed_for_countable_meets -> all-open-containing closed_for_countable_unions for Element of bool (bool the carrier of T);

coherence for b

( b

begin

registration
end;

registration

let T be TopSpace;

coherence

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

( b_{1} is open & b_{1} is closed )

end;
coherence

for b

( b

proof end;

registration

let T be TopSpace;

existence

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

( b_{1} is countable & b_{1} is open & b_{1} is closed )

end;
existence

ex b

( b

proof end;

begin

theorem Th19: :: TOPGEN_4:19

for T being non empty TopSpace

for A being Subset of T

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

( A is open iff F is open )

for A being Subset of T

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

( A is open iff F is open )

proof end;

theorem Th20: :: TOPGEN_4:20

for T being non empty TopSpace

for A being Subset of T

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

( A is closed iff F is closed )

for A being Subset of T

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

( A is closed iff F is closed )

proof end;

definition

let T be set ;

let F, G be Subset-Family of T;

:: original: INTERSECTION

redefine func INTERSECTION (F,G) -> Subset-Family of T;

coherence

INTERSECTION (F,G) is Subset-Family of T

redefine func UNION (F,G) -> Subset-Family of T;

coherence

UNION (F,G) is Subset-Family of T

end;
let F, G be Subset-Family of T;

:: original: INTERSECTION

redefine func INTERSECTION (F,G) -> Subset-Family of T;

coherence

INTERSECTION (F,G) is Subset-Family of T

proof end;

:: original: UNIONredefine func UNION (F,G) -> Subset-Family of T;

coherence

UNION (F,G) is Subset-Family of T

proof end;

theorem Th21: :: TOPGEN_4:21

for T being non empty TopSpace

for F, G being Subset-Family of T st F is closed & G is closed holds

INTERSECTION (F,G) is closed

for F, G being Subset-Family of T st F is closed & G is closed holds

INTERSECTION (F,G) is closed

proof end;

theorem Th22: :: TOPGEN_4:22

for T being non empty TopSpace

for F, G being Subset-Family of T st F is closed & G is closed holds

UNION (F,G) is closed

for F, G being Subset-Family of T st F is closed & G is closed holds

UNION (F,G) is closed

proof end;

theorem Th23: :: TOPGEN_4:23

for T being non empty TopSpace

for F, G being Subset-Family of T st F is open & G is open holds

INTERSECTION (F,G) is open

for F, G being Subset-Family of T st F is open & G is open holds

INTERSECTION (F,G) is open

proof end;

theorem Th24: :: TOPGEN_4:24

for T being non empty TopSpace

for F, G being Subset-Family of T st F is open & G is open holds

UNION (F,G) is open

for F, G being Subset-Family of T st F is open & G is open holds

UNION (F,G) is open

proof end;

begin

definition

let T be TopSpace;

let A be Subset of T;

end;
let A be Subset of T;

attr A is F_sigma means :Def6: :: TOPGEN_4:def 6

ex F being countable closed Subset-Family of T st A = union F;

ex F being countable closed Subset-Family of T st A = union F;

:: deftheorem Def6 defines F_sigma TOPGEN_4:def 6 :

for T being TopSpace

for A being Subset of T holds

( A is F_sigma iff ex F being countable closed Subset-Family of T st A = union F );

for T being TopSpace

for A being Subset of T holds

( A is F_sigma iff ex F being countable closed Subset-Family of T st A = union F );

definition

let T be TopSpace;

let A be Subset of T;

end;
let A be Subset of T;

attr A is G_delta means :Def7: :: TOPGEN_4:def 7

ex F being countable open Subset-Family of T st A = meet F;

ex F being countable open Subset-Family of T st A = meet F;

:: deftheorem Def7 defines G_delta TOPGEN_4:def 7 :

for T being TopSpace

for A being Subset of T holds

( A is G_delta iff ex F being countable open Subset-Family of T st A = meet F );

for T being TopSpace

for A being Subset of T holds

( A is G_delta iff ex F being countable open Subset-Family of T st A = meet F );

registration

let T be non empty TopSpace;

coherence

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

( b_{1} is F_sigma & b_{1} is G_delta )

end;
coherence

for b

( b

proof end;

registration
end;

theorem :: TOPGEN_4:39

for T being non empty TopSpace

for A, B being Subset of T st A is F_sigma & B is F_sigma holds

A /\ B is F_sigma

for A, B being Subset of T st A is F_sigma & B is F_sigma holds

A /\ B is F_sigma

proof end;

theorem :: TOPGEN_4:40

for T being non empty TopSpace

for A, B being Subset of T st A is F_sigma & B is F_sigma holds

A \/ B is F_sigma

for A, B being Subset of T st A is F_sigma & B is F_sigma holds

A \/ B is F_sigma

proof end;

theorem :: TOPGEN_4:41

for T being non empty TopSpace

for A, B being Subset of T st A is G_delta & B is G_delta holds

A \/ B is G_delta

for A, B being Subset of T st A is G_delta & B is G_delta holds

A \/ B is G_delta

proof end;

theorem :: TOPGEN_4:42

for T being non empty TopSpace

for A, B being Subset of T st A is G_delta & B is G_delta holds

A /\ B is G_delta

for A, B being Subset of T st A is G_delta & B is G_delta holds

A /\ B is G_delta

proof end;

begin

:: deftheorem Def8 defines T_1/2 TOPGEN_4:def 8 :

for T being TopSpace holds

( T is T_1/2 iff for A being Subset of T holds Der A is closed );

for T being TopSpace holds

( T is T_1/2 iff for A being Subset of T holds Der A is closed );

registration

coherence

for b_{1} being TopSpace st b_{1} is T_1/2 holds

b_{1} is T_0

for b_{1} being TopSpace st b_{1} is T_1 holds

b_{1} is T_1/2
by Th46;

end;
for b

b

proof end;

coherence for b

b

begin

:: Page 77 - 1.7.11

definition

let T be non empty TopSpace;

let A be Subset of T;

let x be Point of T;

end;
let A be Subset of T;

let x be Point of T;

pred x is_a_condensation_point_of A means :Def9: :: TOPGEN_4:def 9

for N being a_neighborhood of x holds not N /\ A is countable ;

for N being a_neighborhood of x holds not N /\ A is countable ;

:: deftheorem Def9 defines is_a_condensation_point_of TOPGEN_4:def 9 :

for T being non empty TopSpace

for A being Subset of T

for x being Point of T holds

( x is_a_condensation_point_of A iff for N being a_neighborhood of x holds not N /\ A is countable );

for T being non empty TopSpace

for A being Subset of T

for x being Point of T holds

( x is_a_condensation_point_of A iff for N being a_neighborhood of x holds not N /\ A is countable );

theorem Th48: :: TOPGEN_4:48

for T being non empty TopSpace

for A, B being Subset of T

for x being Point of T st x is_a_condensation_point_of A & A c= B holds

x is_a_condensation_point_of B

for A, B being Subset of T

for x being Point of T st x is_a_condensation_point_of A & A c= B holds

x is_a_condensation_point_of B

proof end;

definition

let T be non empty TopSpace;

let A be Subset of T;

ex b_{1} being Subset of T st

for x being Point of T holds

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

for b_{1}, b_{2} being Subset of T st ( for x being Point of T holds

( x in b_{1} iff x is_a_condensation_point_of A ) ) & ( for x being Point of T holds

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

b_{1} = b_{2}

end;
let A be Subset of T;

func A ^0 -> Subset of T means :Def10: :: TOPGEN_4:def 10

for x being Point of T holds

( x in it iff x is_a_condensation_point_of A );

existence for x being Point of T holds

( x in it iff x is_a_condensation_point_of A );

ex b

for x being Point of T holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def10 defines ^0 TOPGEN_4:def 10 :

for T being non empty TopSpace

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

( b_{3} = A ^0 iff for x being Point of T holds

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

for T being non empty TopSpace

for A, b

( b

( x in b

theorem Th49: :: TOPGEN_4:49

for T being non empty TopSpace

for A being Subset of T

for p being Point of T st p is_a_condensation_point_of A holds

p is_an_accumulation_point_of A

for A being Subset of T

for p being Point of T st p is_a_condensation_point_of A holds

p is_an_accumulation_point_of A

proof end;

theorem Th53: :: TOPGEN_4:53

for T being non empty TopSpace

for A, B being Subset of T

for x being Point of T holds

( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )

for A, B being Subset of T

for x being Point of T holds

( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )

proof end;

theorem Th55: :: TOPGEN_4:55

for T being non empty TopSpace

for A being Subset of T st A is countable holds

for x being Point of T holds not x is_a_condensation_point_of A

for A being Subset of T st A is countable holds

for x being Point of T holds not x is_a_condensation_point_of A

proof end;

registration
end;

theorem :: TOPGEN_4:57

for T being non empty TopSpace st T is second-countable holds

ex B being Basis of T st B is countable

ex B being Basis of T st B is countable

proof end;

registration
end;

begin

registration

let T be non empty TopSpace;

coherence

( not TotFam T is empty & TotFam T is all-open-containing & TotFam T is compl-closed & TotFam T is closed_for_countable_unions )

end;
coherence

( not TotFam T is empty & TotFam T is all-open-containing & TotFam T is compl-closed & TotFam T is closed_for_countable_unions )

proof end;

theorem Th59: :: TOPGEN_4:59

for T being non empty TopSpace

for F, G being Subset-Family of T st F is all-open-containing & F c= G holds

G is all-open-containing

for F, G being Subset-Family of T st F is all-open-containing & F c= G holds

G is all-open-containing

proof end;

theorem :: TOPGEN_4:60

for T being non empty TopSpace

for F, G being Subset-Family of T st F is all-closed-containing & F c= G holds

G is all-closed-containing

for F, G being Subset-Family of T st F is all-closed-containing & F c= G holds

G is all-closed-containing

proof end;

registration

let T be non empty TopSpace;

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

( b_{1} is compl-closed & b_{1} is closed_for_countable_unions & b_{1} is closed_for_countable_meets & b_{1} is all-closed-containing & b_{1} is all-open-containing )

end;
cluster compl-closed all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets for Element of bool (bool the carrier of T);

existence ex b

( b

proof end;

theorem Th61: :: TOPGEN_4:61

for T being non empty TopSpace holds

( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )

( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions )

proof end;

registration

let T be non empty TopSpace;

coherence

( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions ) by Th61;

end;
coherence

( sigma (TotFam T) is all-open-containing & sigma (TotFam T) is compl-closed & sigma (TotFam T) is closed_for_countable_unions ) by Th61;

registration

let T be non empty 1-sorted ;

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

( b_{1} is sigma-additive & b_{1} is compl-closed & b_{1} is closed_for_countable_unions & not b_{1} is empty )

end;
cluster non empty compl-closed sigma-additive closed_for_countable_unions for Element of bool (bool the carrier of T);

existence ex b

( b

proof end;

registration

let T be non empty TopSpace;

for b_{1} being SigmaField of T holds b_{1} is closed_for_countable_unions
;

end;
cluster non empty compl-closed sigma-multiplicative -> closed_for_countable_unions for Element of bool (bool the carrier of T);

coherence for b

theorem :: TOPGEN_4:62

for T being non empty TopSpace

for F being Subset-Family of T st F is compl-closed & F is closed_for_countable_unions holds

F is SigmaField of T by Th13;

for F being Subset-Family of T st F is compl-closed & F is closed_for_countable_unions holds

F is SigmaField of T by Th13;

registration

let T be non empty TopSpace;

ex b_{1} being SigmaField of T st b_{1} is all-open-containing

end;
cluster non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive all-open-containing closed_for_countable_unions for Element of bool (bool the carrier of T);

existence ex b

proof end;

registration

let T be non empty TopSpace;

coherence

( Topology_of T is open & Topology_of T is all-open-containing )

end;
coherence

( Topology_of T is open & Topology_of T is all-open-containing )

proof end;

theorem Th63: :: TOPGEN_4:63

for T being non empty TopSpace

for X being Subset-Family of T ex Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st

( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds

Y c= Z ) )

for X being Subset-Family of T ex Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st

( X c= Y & ( for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st X c= Z holds

Y c= Z ) )

proof end;

definition

let T be non empty TopSpace;

ex b_{1} being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st

for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b_{1} c= G

for b_{1}, b_{2} being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b_{1} c= G ) & ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b_{2} c= G ) holds

b_{1} = b_{2}

end;
func BorelSets T -> compl-closed all-open-containing closed_for_countable_unions Subset-Family of T means :Def11: :: TOPGEN_4:def 11

for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds it c= G;

existence for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds it c= G;

ex b

for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines BorelSets TOPGEN_4:def 11 :

for T being non empty TopSpace

for b_{2} being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds

( b_{2} = BorelSets T iff for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b_{2} c= G );

for T being non empty TopSpace

for b

( b

:: deftheorem Def12 defines Borel TOPGEN_4:def 12 :

for T being non empty TopSpace

for A being Subset of T holds

( A is Borel iff A in BorelSets T );

for T being non empty TopSpace

for A being Subset of T holds

( A is Borel iff A in BorelSets T );

registration

let T be non empty TopSpace;

coherence

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

b_{1} is Borel

end;
coherence

for b

b

proof end;

registration

let T be non empty TopSpace;

coherence

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

b_{1} is Borel

end;
coherence

for b

b

proof end;