:: by Karol P\c{a}k

::

:: Received March 31, 2009

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

:: deftheorem defines are_homeomorphic METRIZTS:def 1 :

for T1, T2 being TopSpace

for A1 being Subset of T1

for A2 being Subset of T2 holds

( A1,A2 are_homeomorphic iff T1 | A1,T2 | A2 are_homeomorphic );

for T1, T2 being TopSpace

for A1 being Subset of T1

for A2 being Subset of T2 holds

( A1,A2 are_homeomorphic iff T1 | A1,T2 | A2 are_homeomorphic );

Lm1: for T1, T2 being empty TopSpace holds T1,T2 are_homeomorphic

proof end;

theorem Th2: :: METRIZTS:2

for T1, T2 being TopSpace

for A1 being Subset of T1

for f being Function of T1,T2 st f is being_homeomorphism holds

for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds

g is being_homeomorphism

for A1 being Subset of T1

for f being Function of T1,T2 st f is being_homeomorphism holds

for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds

g is being_homeomorphism

proof end;

theorem :: METRIZTS:3

for T1, T2 being TopSpace

for A1 being Subset of T1

for f being Function of T1,T2 st f is being_homeomorphism holds

A1,f .: A1 are_homeomorphic

for A1 being Subset of T1

for f being Function of T1,T2 st f is being_homeomorphism holds

A1,f .: A1 are_homeomorphic

proof end;

Lm2: for T1, T2 being non empty TopSpace st T1,T2 are_homeomorphic holds

weight T2 c= weight T1

proof end;

Lm3: for T being empty TopSpace holds weight T is empty

proof end;

registration

coherence

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

b_{1} is metrizable

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

b_{1} is T_4

coherence

TopSpaceMetr M is metrizable

end;
for b

b

proof end;

coherence for b

b

proof end;

let M be MetrSpace;coherence

TopSpaceMetr M is metrizable

proof end;

registration
end;

registration
end;

registration
end;

theorem Th6: :: METRIZTS:6

for T1, T2 being TopSpace st not T1 is empty & not T2 is empty holds

( weight T1 c= weight [:T1,T2:] & weight T2 c= weight [:T1,T2:] )

( weight T1 c= weight [:T1,T2:] & weight T2 c= weight [:T1,T2:] )

proof end;

registration
end;

theorem Th7: :: METRIZTS:7

for T being TopSpace

for A being Subset of T

for F being Subset-Family of T holds card (F | A) c= card F

for A being Subset of T

for F being Subset-Family of T holds card (F | A) c= card F

proof end;

theorem Th8: :: METRIZTS:8

for T being TopSpace

for A being Subset of T

for Bas being Basis of T holds Bas | A is Basis of (T | A)

for A being Subset of T

for Bas being Basis of T holds Bas | A is Basis of (T | A)

proof end;

registration

let T be second-countable TopSpace;

let A be Subset of T;

coherence

T | A is second-countable

end;
let A be Subset of T;

coherence

T | A is second-countable

proof end;

registration

let M be non empty MetrSpace;

let A be non empty Subset of (TopSpaceMetr M);

coherence

dist_min A is continuous

end;
let A be non empty Subset of (TopSpaceMetr M);

coherence

dist_min A is continuous

proof end;

theorem :: METRIZTS:9

for T being TopSpace

for A, B being Subset of T

for F being Subset of (T | A) st F = B holds

(T | A) | F = T | B

for A, B being Subset of T

for F being Subset of (T | A) st F = B holds

(T | A) | F = T | B

proof end;

Lm4: for M being non empty MetrSpace

for A being non empty Subset of (TopSpaceMetr M)

for r being Real holds { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } is open Subset of (TopSpaceMetr M)

proof end;

:: F_sigma and G_delta Types of Subsets

registration

let TM be metrizable TopSpace;

coherence

for b_{1} being Subset of TM st b_{1} is open holds

b_{1} is F_sigma

for b_{1} being Subset of TM st b_{1} is closed holds

b_{1} is G_delta

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

theorem :: METRIZTS:10

for T being TopSpace

for A, B being Subset of T

for F being Subset of (T | B) st A is F_sigma & F = A /\ B holds

F is F_sigma

for A, B being Subset of T

for F being Subset of (T | B) st A is F_sigma & F = A /\ B holds

F is F_sigma

proof end;

theorem :: METRIZTS:11

for T being TopSpace

for A, B being Subset of T

for F being Subset of (T | B) st A is G_delta & F = A /\ B holds

F is G_delta

for A, B being Subset of T

for F being Subset of (T | B) st A is G_delta & F = A /\ B holds

F is G_delta

proof end;

theorem Th12: :: METRIZTS:12

for T being TopSpace

for A being Subset of T st T is T_1 & A is discrete holds

A is open Subset of (T | (Cl A))

for A being Subset of T st T is T_1 & A is discrete holds

A is open Subset of (T | (Cl A))

proof end;

Lm5: for iC being infinite Cardinal holds omega *` iC = iC

proof end;

theorem Th13: :: METRIZTS:13

for C being Cardinal

for T being TopSpace st ( for F being Subset-Family of T st F is open & F is Cover of T holds

ex G being Subset-Family of T st

( G c= F & G is Cover of T & card G c= C ) ) holds

for A being Subset of T st A is closed & A is discrete holds

card A c= C

for T being TopSpace st ( for F being Subset-Family of T st F is open & F is Cover of T holds

ex G being Subset-Family of T st

( G c= F & G is Cover of T & card G c= C ) ) holds

for A being Subset of T st A is closed & A is discrete holds

card A c= C

proof end;

theorem Th14: :: METRIZTS:14

for iC being infinite Cardinal

for TM being metrizable TopSpace st ( for Am being Subset of TM st Am is closed & Am is discrete holds

card Am c= iC ) holds

for Am being Subset of TM st Am is discrete holds

card Am c= iC

for TM being metrizable TopSpace st ( for Am being Subset of TM st Am is closed & Am is discrete holds

card Am c= iC ) holds

for Am being Subset of TM st Am is discrete holds

card Am c= iC

proof end;

theorem Th15: :: METRIZTS:15

for C being Cardinal

for T being TopSpace st ( for A being Subset of T st A is discrete holds

card A c= C ) holds

for F being Subset-Family of T st F is open & not {} in F & ( for A, B being Subset of T st A in F & B in F & A <> B holds

A misses B ) holds

card F c= C

for T being TopSpace st ( for A being Subset of T st A is discrete holds

card A c= C ) holds

for F being Subset-Family of T st F is open & not {} in F & ( for A, B being Subset of T st A in F & B in F & A <> B holds

A misses B ) holds

card F c= C

proof end;

theorem Th16: :: METRIZTS:16

for T being TopSpace

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

ex G being Subset-Family of T st

( G c= F & G is Cover of T & card G c= card ([#] T) )

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

ex G being Subset-Family of T st

( G c= F & G is Cover of T & card G c= card ([#] T) )

proof end;

Lm6: for TM being metrizable TopSpace

for iC being infinite Cardinal st ( for Fm being Subset-Family of TM st Fm is open & not {} in Fm & ( for Am, Bm being Subset of TM st Am in Fm & Bm in Fm & Am <> Bm holds

Am misses Bm ) holds

card Fm c= iC ) holds

density TM c= iC

proof end;

theorem Th17: :: METRIZTS:17

for TM being metrizable TopSpace

for Am being Subset of TM st Am is dense holds

weight TM c= omega *` (card Am)

for Am being Subset of TM st Am is dense holds

weight TM c= omega *` (card Am)

proof end;

Lm7: for TM being metrizable TopSpace

for iC being infinite Cardinal st density TM c= iC holds

weight TM c= iC

proof end;

:: General Topology Th 4.1.15 (a) <=> (c)

theorem Th18: :: METRIZTS:18

for TM being metrizable TopSpace

for iC being infinite Cardinal holds

( weight TM c= iC iff for Fm being Subset-Family of TM st Fm is open & Fm is Cover of TM holds

ex Gm being Subset-Family of TM st

( Gm c= Fm & Gm is Cover of TM & card Gm c= iC ) )

for iC being infinite Cardinal holds

( weight TM c= iC iff for Fm being Subset-Family of TM st Fm is open & Fm is Cover of TM holds

ex Gm being Subset-Family of TM st

( Gm c= Fm & Gm is Cover of TM & card Gm c= iC ) )

proof end;

:: General Topology Th 4.1.15 (a) <=> (d)

theorem Th19: :: METRIZTS:19

for TM being metrizable TopSpace

for iC being infinite Cardinal holds

( weight TM c= iC iff for Am being Subset of TM st Am is closed & Am is discrete holds

card Am c= iC )

for iC being infinite Cardinal holds

( weight TM c= iC iff for Am being Subset of TM st Am is closed & Am is discrete holds

card Am c= iC )

proof end;

:: General Topology Th 4.1.15 (a) <=> (e)

theorem Th20: :: METRIZTS:20

for TM being metrizable TopSpace

for iC being infinite Cardinal holds

( weight TM c= iC iff for Am being Subset of TM st Am is discrete holds

card Am c= iC )

for iC being infinite Cardinal holds

( weight TM c= iC iff for Am being Subset of TM st Am is discrete holds

card Am c= iC )

proof end;

:: General Topology Th 4.1.15 (a) <=> (f)

theorem Th21: :: METRIZTS:21

for TM being metrizable TopSpace

for iC being infinite Cardinal holds

( weight TM c= iC iff for Fm being Subset-Family of TM st Fm is open & not {} in Fm & ( for Am, Bm being Subset of TM st Am in Fm & Bm in Fm & Am <> Bm holds

Am misses Bm ) holds

card Fm c= iC )

for iC being infinite Cardinal holds

( weight TM c= iC iff for Fm being Subset-Family of TM st Fm is open & not {} in Fm & ( for Am, Bm being Subset of TM st Am in Fm & Bm in Fm & Am <> Bm holds

Am misses Bm ) holds

card Fm c= iC )

proof end;

:: General Topology Th 4.1.15 (a) <=> (g)

theorem Th22: :: METRIZTS:22

for TM being metrizable TopSpace

for iC being infinite Cardinal holds

( weight TM c= iC iff density TM c= iC )

for iC being infinite Cardinal holds

( weight TM c= iC iff density TM c= iC )

proof end;

theorem Th23: :: METRIZTS:23

for TM being metrizable TopSpace

for iC being infinite Cardinal

for B being Basis of TM st ( for Fm being Subset-Family of TM st Fm is open & Fm is Cover of TM holds

ex Gm being Subset-Family of TM st

( Gm c= Fm & Gm is Cover of TM & card Gm c= iC ) ) holds

ex underB being Basis of TM st

( underB c= B & card underB c= iC )

for iC being infinite Cardinal

for B being Basis of TM st ( for Fm being Subset-Family of TM st Fm is open & Fm is Cover of TM holds

ex Gm being Subset-Family of TM st

( Gm c= Fm & Gm is Cover of TM & card Gm c= iC ) ) holds

ex underB being Basis of TM st

( underB c= B & card underB c= iC )

proof end;

definition

let T be TopSpace;

end;
attr T is Lindelof means :Def2: :: METRIZTS:def 2

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

ex G being Subset-Family of T st

( G c= F & G is Cover of T & G is countable );

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

ex G being Subset-Family of T st

( G c= F & G is Cover of T & G is countable );

:: deftheorem Def2 defines Lindelof METRIZTS:def 2 :

for T being TopSpace holds

( T is Lindelof iff for F being Subset-Family of T st F is open & F is Cover of T holds

ex G being Subset-Family of T st

( G c= F & G is Cover of T & G is countable ) );

for T being TopSpace holds

( T is Lindelof iff for F being Subset-Family of T st F is open & F is Cover of T holds

ex G being Subset-Family of T st

( G c= F & G is Cover of T & G is countable ) );

Lm8: for T being TopSpace holds

( T is Lindelof iff for F being Subset-Family of T st F is open & F is Cover of T holds

ex G being Subset-Family of T st

( G c= F & G is Cover of T & card G c= omega ) )

proof end;

theorem :: METRIZTS:24

for TM being metrizable TopSpace

for B being Basis of TM st TM is Lindelof holds

ex B9 being Basis of TM st

( B9 c= B & B9 is countable )

for B being Basis of TM st TM is Lindelof holds

ex B9 being Basis of TM st

( B9 c= B & B9 is countable )

proof end;

Lm9: for TM being metrizable TopSpace holds

( TM is Lindelof iff TM is second-countable )

proof end;

registration

coherence

for b_{1} being metrizable TopSpace st b_{1} is Lindelof holds

b_{1} is second-countable
by Lm9;

end;
for b

b

Lm10: for TM being metrizable TopSpace holds

( TM is Lindelof iff TM is separable )

proof end;

registration

coherence

for b_{1} being metrizable TopSpace st b_{1} is Lindelof holds

b_{1} is separable
by Lm10;

coherence

for b_{1} being metrizable TopSpace st b_{1} is separable holds

b_{1} is Lindelof
by Lm10;

end;
for b

b

coherence

for b

b

registration

existence

ex b_{1} being non empty TopSpace st

( b_{1} is Lindelof & b_{1} is metrizable )

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

b_{1} is Lindelof

for b_{1} being TopSpace st b_{1} is regular & b_{1} is Lindelof holds

b_{1} is normal

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

b_{1} is Lindelof

end;
ex b

( b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

Lm11: TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is second-countable

proof end;

registration

let n be Nat;

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is second-countable

end;
cluster TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) -> second-countable ;

coherence TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is second-countable

proof end;

registration
end;

registration
end;

:: deftheorem defines separates METRIZTS:def 3 :

for T being TopSpace

for A, B, L being Subset of T holds

( L separates A,B iff ex U, W being open Subset of T st

( A c= U & B c= W & U misses W & L = (U \/ W) ` ) );

for T being TopSpace

for A, B, L being Subset of T holds

( L separates A,B iff ex U, W being open Subset of T st

( A c= U & B c= W & U misses W & L = (U \/ W) ` ) );

Lm12: for M being non empty MetrSpace

for A, B being non empty Subset of (TopSpaceMetr M) holds { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } is open Subset of (TopSpaceMetr M)

proof end;

Lm13: for TM being metrizable TopSpace

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

ex U, W being open Subset of TM st

( A c= U & B c= W & U misses W )

proof end;

:: Teoria wymiaru Lm 1.2.8

theorem :: METRIZTS:25

for TM being metrizable TopSpace

for Am, Bm being Subset of TM st Am,Bm are_separated holds

ex L being Subset of TM st L separates Am,Bm

for Am, Bm being Subset of TM st Am,Bm are_separated holds

ex L being Subset of TM st L separates Am,Bm

proof end;

:: Teoria wymiaru Lm 1.2.9

theorem :: METRIZTS:26

for TM being metrizable TopSpace

for M being Subset of TM

for A1, A2 being closed Subset of TM

for V1, V2 being open Subset of TM st A1 c= V1 & A2 c= V2 & Cl V1 misses Cl V2 holds

for mV1, mV2, mL being Subset of (TM | M) st mV1 = M /\ (Cl V1) & mV2 = M /\ (Cl V2) & mL separates mV1,mV2 holds

ex L being Subset of TM st

( L separates A1,A2 & M /\ L c= mL )

for M being Subset of TM

for A1, A2 being closed Subset of TM

for V1, V2 being open Subset of TM st A1 c= V1 & A2 c= V2 & Cl V1 misses Cl V2 holds

for mV1, mV2, mL being Subset of (TM | M) st mV1 = M /\ (Cl V1) & mV2 = M /\ (Cl V2) & mL separates mV1,mV2 holds

ex L being Subset of TM st

( L separates A1,A2 & M /\ L c= mL )

proof end;