:: by Grzegorz Bancerek

::

:: Received December 10, 2004

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

::<DESC name="baza w punkcie a baza" monograph="topology"/>

theorem Th1: :: TOPGEN_2:1

for T being non empty TopSpace

for B being Basis of T

for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x

for B being Basis of T

for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x

proof end;

::<DESC name="baza w punkcie a baza" monograph="topology"/>

theorem Th2: :: TOPGEN_2:2

for T being non empty TopSpace

for B being ManySortedSet of T st ( for x being Element of T holds B . x is Basis of x ) holds

Union B is Basis of T

for B being ManySortedSet of T st ( for x being Element of T holds B . x is Basis of x ) holds

Union B is Basis of T

proof end;

definition

let T be non empty TopStruct ;

let x be Element of T;

ex b_{1} being cardinal number st

( ex B being Basis of x st b_{1} = card B & ( for B being Basis of x holds b_{1} c= card B ) )

for b_{1}, b_{2} being cardinal number st ex B being Basis of x st b_{1} = card B & ( for B being Basis of x holds b_{1} c= card B ) & ex B being Basis of x st b_{2} = card B & ( for B being Basis of x holds b_{2} c= card B ) holds

b_{1} = b_{2}

end;
let x be Element of T;

func Chi (x,T) -> cardinal number means :Def1: :: TOPGEN_2:def 1

( ex B being Basis of x st it = card B & ( for B being Basis of x holds it c= card B ) );

existence ( ex B being Basis of x st it = card B & ( for B being Basis of x holds it c= card B ) );

ex b

( ex B being Basis of x st b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Chi TOPGEN_2:def 1 :

for T being non empty TopStruct

for x being Element of T

for b_{3} being cardinal number holds

( b_{3} = Chi (x,T) iff ( ex B being Basis of x st b_{3} = card B & ( for B being Basis of x holds b_{3} c= card B ) ) );

for T being non empty TopStruct

for x being Element of T

for b

( b

::<DESC name="charakter punktu" monograph="topology"/>

theorem Th3: :: TOPGEN_2:3

for X being set st ( for a being set st a in X holds

a is cardinal number ) holds

union X is cardinal number

a is cardinal number ) holds

union X is cardinal number

proof end;

Lm1: now :: thesis: for T being non empty TopStruct holds

( union { (Chi (x,T)) where x is Point of T : verum } is cardinal number & ( for m being cardinal number st m = union { (Chi (x,T)) where x is Point of T : verum } holds

( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

m c= M ) ) ) )

( union { (Chi (x,T)) where x is Point of T : verum } is cardinal number & ( for m being cardinal number st m = union { (Chi (x,T)) where x is Point of T : verum } holds

( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

m c= M ) ) ) )

let T be non empty TopStruct ; :: thesis: ( union { (Chi (x,T)) where x is Point of T : verum } is cardinal number & ( for m being cardinal number st m = union { (Chi (x,T)) where x is Point of T : verum } holds

( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

m c= M ) ) ) )

set X = { (Chi (x,T)) where x is Point of T : verum } ;

( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

m c= M ) )

let m be cardinal number ; :: thesis: ( m = union { (Chi (x,T)) where x is Point of T : verum } implies ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

m c= M ) ) )

assume A1: m = union { (Chi (x,T)) where x is Point of T : verum } ; :: thesis: ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

m c= M ) )

assume A2: for x being Point of T holds Chi (x,T) c= M ; :: thesis: m c= M

end;
( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

m c= M ) ) ) )

set X = { (Chi (x,T)) where x is Point of T : verum } ;

now :: thesis: for a being set st a in { (Chi (x,T)) where x is Point of T : verum } holds

a is cardinal number

hence
union { (Chi (x,T)) where x is Point of T : verum } is cardinal number
by Th3; :: thesis: for m being cardinal number st m = union { (Chi (x,T)) where x is Point of T : verum } holds a is cardinal number

let a be set ; :: thesis: ( a in { (Chi (x,T)) where x is Point of T : verum } implies a is cardinal number )

assume a in { (Chi (x,T)) where x is Point of T : verum } ; :: thesis: a is cardinal number

then ex x being Point of T st a = Chi (x,T) ;

hence a is cardinal number ; :: thesis: verum

end;
assume a in { (Chi (x,T)) where x is Point of T : verum } ; :: thesis: a is cardinal number

then ex x being Point of T st a = Chi (x,T) ;

hence a is cardinal number ; :: thesis: verum

( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

m c= M ) )

let m be cardinal number ; :: thesis: ( m = union { (Chi (x,T)) where x is Point of T : verum } implies ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

m c= M ) ) )

assume A1: m = union { (Chi (x,T)) where x is Point of T : verum } ; :: thesis: ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

m c= M ) )

hereby :: thesis: for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

m c= M

let M be cardinal number ; :: thesis: ( ( for x being Point of T holds Chi (x,T) c= M ) implies m c= M )m c= M

let x be Point of T; :: thesis: Chi (x,T) c= m

Chi (x,T) in { (Chi (x,T)) where x is Point of T : verum } ;

hence Chi (x,T) c= m by A1, ZFMISC_1:74; :: thesis: verum

end;
Chi (x,T) in { (Chi (x,T)) where x is Point of T : verum } ;

hence Chi (x,T) c= m by A1, ZFMISC_1:74; :: thesis: verum

assume A2: for x being Point of T holds Chi (x,T) c= M ; :: thesis: m c= M

now :: thesis: for a being set st a in { (Chi (x,T)) where x is Point of T : verum } holds

a c= M

hence
m c= M
by A1, ZFMISC_1:76; :: thesis: veruma c= M

let a be set ; :: thesis: ( a in { (Chi (x,T)) where x is Point of T : verum } implies a c= M )

assume a in { (Chi (x,T)) where x is Point of T : verum } ; :: thesis: a c= M

then ex x being Point of T st a = Chi (x,T) ;

hence a c= M by A2; :: thesis: verum

end;
assume a in { (Chi (x,T)) where x is Point of T : verum } ; :: thesis: a c= M

then ex x being Point of T st a = Chi (x,T) ;

hence a c= M by A2; :: thesis: verum

definition

let T be non empty TopStruct ;

ex b_{1} being cardinal number st

( ( for x being Point of T holds Chi (x,T) c= b_{1} ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

b_{1} c= M ) )

for b_{1}, b_{2} being cardinal number st ( for x being Point of T holds Chi (x,T) c= b_{1} ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

b_{1} c= M ) & ( for x being Point of T holds Chi (x,T) c= b_{2} ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

b_{2} c= M ) holds

b_{1} = b_{2}

end;
func Chi T -> cardinal number means :Def2: :: TOPGEN_2:def 2

( ( for x being Point of T holds Chi (x,T) c= it ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

it c= M ) );

existence ( ( for x being Point of T holds Chi (x,T) c= it ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

it c= M ) );

ex b

( ( for x being Point of T holds Chi (x,T) c= b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines Chi TOPGEN_2:def 2 :

for T being non empty TopStruct

for b_{2} being cardinal number holds

( b_{2} = Chi T iff ( ( for x being Point of T holds Chi (x,T) c= b_{2} ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds

b_{2} c= M ) ) );

for T being non empty TopStruct

for b

( b

b

::<DESC name="charakter przestrzeni" monograph="topology"/>

::<DESC name="pierwszy aksjomat przeliczalno/sci" monograph="topology"/>

definition

let T be non empty TopSpace;

ex b_{1} being ManySortedSet of T st

for x being Element of T holds b_{1} . x is Basis of x

end;
mode Neighborhood_System of T -> ManySortedSet of T means :Def3: :: TOPGEN_2:def 3

for x being Element of T holds it . x is Basis of x;

existence for x being Element of T holds it . x is Basis of x;

ex b

for x being Element of T holds b

proof end;

:: deftheorem Def3 defines Neighborhood_System TOPGEN_2:def 3 :

for T being non empty TopSpace

for b_{2} being ManySortedSet of T holds

( b_{2} is Neighborhood_System of T iff for x being Element of T holds b_{2} . x is Basis of x );

for T being non empty TopSpace

for b

( b

::<DESC name="uk/lad otocze/n" monograph="topology"/>

definition

let T be non empty TopSpace;

let N be Neighborhood_System of T;

:: original: Union

redefine func Union N -> Basis of T;

coherence

Union N is Basis of T

:: original: .

redefine func N . x -> Basis of x;

coherence

N . x is Basis of x by Def3;

end;
let N be Neighborhood_System of T;

:: original: Union

redefine func Union N -> Basis of T;

coherence

Union N is Basis of T

proof end;

let x be Point of T;:: original: .

redefine func N . x -> Basis of x;

coherence

N . x is Basis of x by Def3;

::<DESC name="uk/lad otocze/n: (BP1)" monograph="topology"/>

:: for T being non empty TopSpace

:: for N being Neighborhood_System of T

:: for x being Element of T holds N.x is non empty &

:: for U being set st U in N.x holds x in U

:: by YELLOW_8:21; :: and clusters YELLOW12

::<DESC name="uk/lad otocze/n: (BP2)" monograph="topology"/>

:: for T being non empty TopSpace

:: for N being Neighborhood_System of T

:: for x being Element of T holds N.x is non empty &

:: for U being set st U in N.x holds x in U

:: by YELLOW_8:21; :: and clusters YELLOW12

::<DESC name="uk/lad otocze/n: (BP2)" monograph="topology"/>

theorem :: TOPGEN_2:7

for T being non empty TopSpace

for x, y being Point of T

for B1 being Basis of x

for B2 being Basis of y

for U being set st x in U & U in B2 holds

ex V being open Subset of T st

( V in B1 & V c= U )

for x, y being Point of T

for B1 being Basis of x

for B2 being Basis of y

for U being set st x in U & U in B2 holds

ex V being open Subset of T st

( V in B1 & V c= U )

proof end;

::<DESC name="uk/lad otocze/n: (BP3)" monograph="topology"/>

theorem :: TOPGEN_2:8

for T being non empty TopSpace

for x being Point of T

for B being Basis of x

for U1, U2 being set st U1 in B & U2 in B holds

ex V being open Subset of T st

( V in B & V c= U1 /\ U2 )

for x being Point of T

for B being Basis of x

for U1, U2 being set st U1 in B & U2 in B holds

ex V being open Subset of T st

( V in B & V c= U1 /\ U2 )

proof end;

Lm2: now :: thesis: for T being non empty TopSpace

for A being Subset of T

for x being Element of T st x in Cl A holds

for B being Basis of x

for U being set st U in B holds

U meets A

for A being Subset of T

for x being Element of T st x in Cl A holds

for B being Basis of x

for U being set st U in B holds

U meets A

let T be non empty TopSpace; :: thesis: for A being Subset of T

for x being Element of T st x in Cl A holds

for B being Basis of x

for U being set st U in B holds

U meets A

let A be Subset of T; :: thesis: for x being Element of T st x in Cl A holds

for B being Basis of x

for U being set st U in B holds

U meets A

let x be Element of T; :: thesis: ( x in Cl A implies for B being Basis of x

for U being set st U in B holds

U meets A )

assume A1: x in Cl A ; :: thesis: for B being Basis of x

for U being set st U in B holds

U meets A

let B be Basis of x; :: thesis: for U being set st U in B holds

U meets A

let U be set ; :: thesis: ( U in B implies U meets A )

assume A2: U in B ; :: thesis: U meets A

then x in U by YELLOW_8:12;

then U meets Cl A by A1, XBOOLE_0:3;

hence U meets A by A2, TSEP_1:36, YELLOW_8:12; :: thesis: verum

end;
for x being Element of T st x in Cl A holds

for B being Basis of x

for U being set st U in B holds

U meets A

let A be Subset of T; :: thesis: for x being Element of T st x in Cl A holds

for B being Basis of x

for U being set st U in B holds

U meets A

let x be Element of T; :: thesis: ( x in Cl A implies for B being Basis of x

for U being set st U in B holds

U meets A )

assume A1: x in Cl A ; :: thesis: for B being Basis of x

for U being set st U in B holds

U meets A

let B be Basis of x; :: thesis: for U being set st U in B holds

U meets A

let U be set ; :: thesis: ( U in B implies U meets A )

assume A2: U in B ; :: thesis: U meets A

then x in U by YELLOW_8:12;

then U meets Cl A by A1, XBOOLE_0:3;

hence U meets A by A2, TSEP_1:36, YELLOW_8:12; :: thesis: verum

Lm3: now :: thesis: for T being non empty TopSpace

for A being Subset of T

for x being Element of T st ex B being Basis of x st

for U being set st U in B holds

U meets A holds

x in Cl A

for A being Subset of T

for x being Element of T st ex B being Basis of x st

for U being set st U in B holds

U meets A holds

x in Cl A

let T be non empty TopSpace; :: thesis: for A being Subset of T

for x being Element of T st ex B being Basis of x st

for U being set st U in B holds

U meets A holds

x in Cl A

let A be Subset of T; :: thesis: for x being Element of T st ex B being Basis of x st

for U being set st U in B holds

U meets A holds

x in Cl A

let x be Element of T; :: thesis: ( ex B being Basis of x st

for U being set st U in B holds

U meets A implies x in Cl A )

given B being Basis of x such that A1: for U being set st U in B holds

U meets A ; :: thesis: x in Cl A

end;
for x being Element of T st ex B being Basis of x st

for U being set st U in B holds

U meets A holds

x in Cl A

let A be Subset of T; :: thesis: for x being Element of T st ex B being Basis of x st

for U being set st U in B holds

U meets A holds

x in Cl A

let x be Element of T; :: thesis: ( ex B being Basis of x st

for U being set st U in B holds

U meets A implies x in Cl A )

given B being Basis of x such that A1: for U being set st U in B holds

U meets A ; :: thesis: x in Cl A

now :: thesis: for U being Subset of T st U is open & x in U holds

A meets U

hence
x in Cl A
by PRE_TOPC:def 7; :: thesis: verumA meets U

let U be Subset of T; :: thesis: ( U is open & x in U implies A meets U )

assume that

A2: U is open and

A3: x in U ; :: thesis: A meets U

ex V being Subset of T st

( V in B & V c= U ) by A2, A3, YELLOW_8:def 1;

hence A meets U by A1, XBOOLE_1:63; :: thesis: verum

end;
assume that

A2: U is open and

A3: x in U ; :: thesis: A meets U

ex V being Subset of T st

( V in B & V c= U ) by A2, A3, YELLOW_8:def 1;

hence A meets U by A1, XBOOLE_1:63; :: thesis: verum

::<DESC name="1.1.1. Twierdzenie: Cl a baza w punkcie" monograph="topology"/>

theorem :: TOPGEN_2:9

for T being non empty TopSpace

for A being Subset of T

for x being Element of T holds

( x in Cl A iff for B being Basis of x

for U being set st U in B holds

U meets A )

for A being Subset of T

for x being Element of T holds

( x in Cl A iff for B being Basis of x

for U being set st U in B holds

U meets A )

proof end;

::<DESC name="1.1.1. Twierdzenie: Cl a baza w punkcie" monograph="topology"/>

theorem :: TOPGEN_2:10

for T being non empty TopSpace

for A being Subset of T

for x being Element of T holds

( x in Cl A iff ex B being Basis of x st

for U being set st U in B holds

U meets A )

for A being Subset of T

for x being Element of T holds

( x in Cl A iff ex B being Basis of x st

for U being set st U in B holds

U meets A )

proof end;

registration

let T be TopSpace;

existence

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

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

end;
existence

ex b

( b

proof end;

::<DESC name="1.1.14. Twierdzenie: istnienie podrodziny mocy niewi/ekszej od wagi przestrzeni i o unii r/ownej" monograph="topology"/>

theorem Th11: :: TOPGEN_2:11

for T being non empty TopSpace

for S being open Subset-Family of T ex G being open Subset-Family of T st

( G c= S & union G = union S & card G c= weight T )

for S being open Subset-Family of T ex G being open Subset-Family of T st

( G c= S & union G = union S & card G c= weight T )

proof end;

definition
end;

:: deftheorem Def4 defines finite-weight TOPGEN_2:def 4 :

for T being TopStruct holds

( T is finite-weight iff weight T is finite );

for T being TopStruct holds

( T is finite-weight iff weight T is finite );

registration

coherence

for b_{1} being TopStruct st b_{1} is finite holds

b_{1} is finite-weight

for b_{1} being TopStruct st b_{1} is infinite-weight holds

b_{1} is infinite
;

end;
for b

b

proof end;

coherence for b

b

theorem Th13: :: TOPGEN_2:13

for T being non empty discrete TopStruct holds

( SmallestPartition the carrier of T is Basis of T & ( for B being Basis of T holds SmallestPartition the carrier of T c= B ) )

( SmallestPartition the carrier of T is Basis of T & ( for B being Basis of T holds SmallestPartition the carrier of T c= B ) )

proof end;

Lm4: for T being infinite-weight TopSpace

for B being Basis of T ex B1 being Basis of T st

( B1 c= B & card B1 = weight T )

proof end;

theorem Th15: :: TOPGEN_2:15

for T being non empty finite-weight TopSpace ex B0 being Basis of T ex f being Function of the carrier of T, the topology of T st

( B0 = rng f & ( for x being Point of T holds

( x in f . x & ( for U being open Subset of T st x in U holds

f . x c= U ) ) ) )

( B0 = rng f & ( for x being Point of T holds

( x in f . x & ( for U being open Subset of T st x in U holds

f . x c= U ) ) ) )

proof end;

theorem Th16: :: TOPGEN_2:16

for T being TopSpace

for B0, B being Basis of T

for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds

( x in f . x & ( for U being open Subset of T st x in U holds

f . x c= U ) ) ) holds

B0 c= B

for B0, B being Basis of T

for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds

( x in f . x & ( for U being open Subset of T st x in U holds

f . x c= U ) ) ) holds

B0 c= B

proof end;

theorem Th17: :: TOPGEN_2:17

for T being TopSpace

for B0 being Basis of T

for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds

( x in f . x & ( for U being open Subset of T st x in U holds

f . x c= U ) ) ) holds

weight T = card B0

for B0 being Basis of T

for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds

( x in f . x & ( for U being open Subset of T st x in U holds

f . x c= U ) ) ) holds

weight T = card B0

proof end;

Lm5: for T being non empty finite-weight TopSpace

for B being Basis of T ex B1 being Basis of T st

( B1 c= B & card B1 = weight T )

proof end;

::<DESC name="1.1.15. Twierdzenie: o istnieniu bazy bed/acej podrodzin/a bazy i maj/acej moc r/own/a wadze przestrzeni" monograph="topology"/>

theorem :: TOPGEN_2:18

for T being non empty TopSpace

for B being Basis of T ex B1 being Basis of T st

( B1 c= B & card B1 = weight T )

for B being Basis of T ex B1 being Basis of T st

( B1 c= B & card B1 = weight T )

proof end;

definition

let X, x0 be set ;

for b_{1}, b_{2} being strict TopStruct st the carrier of b_{1} = X & the topology of b_{1} = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } & the carrier of b_{2} = X & the topology of b_{2} = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } holds

b_{1} = b_{2}
;

existence

ex b_{1} being strict TopStruct st

( the carrier of b_{1} = X & the topology of b_{1} = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } )

end;
func DiscrWithInfin (X,x0) -> strict TopStruct means :Def5: :: TOPGEN_2:def 5

( the carrier of it = X & the topology of it = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } );

uniqueness ( the carrier of it = X & the topology of it = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } );

for b

b

existence

ex b

( the carrier of b

proof end;

:: deftheorem Def5 defines DiscrWithInfin TOPGEN_2:def 5 :

for X, x0 being set

for b_{3} being strict TopStruct holds

( b_{3} = DiscrWithInfin (X,x0) iff ( the carrier of b_{3} = X & the topology of b_{3} = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ) );

for X, x0 being set

for b

( b

registration
end;

theorem Th19: :: TOPGEN_2:19

for X, x0 being set

for A being Subset of (DiscrWithInfin (X,x0)) holds

( A is open iff ( not x0 in A or A ` is finite ) )

for A being Subset of (DiscrWithInfin (X,x0)) holds

( A is open iff ( not x0 in A or A ` is finite ) )

proof end;

theorem Th20: :: TOPGEN_2:20

for X, x0 being set

for A being Subset of (DiscrWithInfin (X,x0)) holds

( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) )

for A being Subset of (DiscrWithInfin (X,x0)) holds

( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) )

proof end;

theorem :: TOPGEN_2:23

for X, x0 being set st X is infinite holds

for U being Subset of (DiscrWithInfin (X,x0)) st U = {x0} holds

not U is open

for U being Subset of (DiscrWithInfin (X,x0)) st U = {x0} holds

not U is open

proof end;

theorem Th25: :: TOPGEN_2:25

for T being non empty TopSpace

for A being Subset of T st not A is closed holds

for a being Point of T st A \/ {a} is closed holds

Cl A = A \/ {a}

for A being Subset of T st not A is closed holds

for a being Point of T st A \/ {a} is closed holds

Cl A = A \/ {a}

proof end;

theorem Th26: :: TOPGEN_2:26

for X, x0 being set st x0 in X holds

for A being Subset of (DiscrWithInfin (X,x0)) st A is infinite holds

Cl A = A \/ {x0}

for A being Subset of (DiscrWithInfin (X,x0)) st A is infinite holds

Cl A = A \/ {x0}

proof end;

theorem :: TOPGEN_2:28

for X, x0 being set st x0 in X holds

for A being Subset of (DiscrWithInfin (X,x0)) st A ` is infinite holds

Int A = A \ {x0}

for A being Subset of (DiscrWithInfin (X,x0)) st A ` is infinite holds

Int A = A \ {x0}

proof end;

theorem Th29: :: TOPGEN_2:29

for X, x0 being set ex B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite }

proof end;

theorem Th32: :: TOPGEN_2:32

for X being infinite set

for x0 being set

for B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } holds

card B0 = card X

for x0 being set

for B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } holds

card B0 = card X

proof end;

theorem Th33: :: TOPGEN_2:33

for X being infinite set

for x0 being set

for B being Basis of (DiscrWithInfin (X,x0)) holds card X c= card B

for x0 being set

for B being Basis of (DiscrWithInfin (X,x0)) holds card X c= card B

proof end;

theorem :: TOPGEN_2:35

for X being non empty set

for x0 being set ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum }

for x0 being set ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum }

proof end;

::<DSCR name="Exercise 1.1.B" monograph="topology"/>

theorem :: TOPGEN_2:36

for T being TopSpace

for F being Subset-Family of T

for I being non empty Subset-Family of F st ( for G being set st G in I holds

F \ G is finite ) holds

Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } )

for F being Subset-Family of T

for I being non empty Subset-Family of F st ( for G being set st G in I holds

F \ G is finite ) holds

Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } )

proof end;

::<DSCR name="Exercise 1.1.B" monograph="topology"/>

theorem :: TOPGEN_2:37

for T being TopSpace

for F being Subset-Family of T holds Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } )

for F being Subset-Family of T holds Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } )

proof end;

::<DSCR name="Exercise 1.1.D" monograph="topology"/>

theorem :: TOPGEN_2:38

for X being set

for O being Subset-Family of (bool X) st ( for o being Subset-Family of X st o in O holds

TopStruct(# X,o #) is TopSpace ) holds

ex B being Subset-Family of X st

( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds

TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds

TopStruct(# X,o #) is TopExtension of T ) holds

TopStruct(# X,B #) is TopExtension of T ) )

for O being Subset-Family of (bool X) st ( for o being Subset-Family of X st o in O holds

TopStruct(# X,o #) is TopSpace ) holds

ex B being Subset-Family of X st

( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds

TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds

TopStruct(# X,o #) is TopExtension of T ) holds

TopStruct(# X,B #) is TopExtension of T ) )

proof end;

::<DSCR name="Exercise 1.1.D" monograph="topology"/>

theorem :: TOPGEN_2:39

for X being set

for O being Subset-Family of (bool X) ex B being Subset-Family of X st

( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds

TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds

T is TopExtension of TopStruct(# X,o #) ) holds

T is TopExtension of TopStruct(# X,B #) ) )

for O being Subset-Family of (bool X) ex B being Subset-Family of X st

( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds

TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds

T is TopExtension of TopStruct(# X,o #) ) holds

T is TopExtension of TopStruct(# X,B #) ) )

proof end;