:: Basic Properties of Metrizable Topological Spaces
:: by Karol P\c{a}k
::
:: Received March 31, 2009
:: Copyright (c) 2009 Association of Mizar Users
:: deftheorem Def1 defines are_homeomorphic METRIZTS:def 1 :
Lm1:
for T1, T2 being empty TopSpace holds T1,T2 are_homeomorphic
theorem :: METRIZTS:1
theorem Th2: :: METRIZTS:2
theorem :: METRIZTS:3
Lm2:
for T1, T2 being non empty TopSpace st T1,T2 are_homeomorphic holds
weight T2 c= weight T1
Lm3:
for T being empty TopSpace holds weight T is empty
theorem Th4: :: METRIZTS:4
theorem Th5: :: METRIZTS:5
theorem Th6: :: METRIZTS:6
theorem Th7: :: METRIZTS:7
theorem Th8: :: METRIZTS:8
theorem :: METRIZTS:9
Lm5:
for M being non empty MetrSpace
for A being non empty Subset of (TopSpaceMetr M)
for r being real number holds { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } is open Subset of (TopSpaceMetr M)
theorem :: METRIZTS:10
theorem :: METRIZTS:11
theorem Th13: :: METRIZTS:12
Lm6:
for iC being infinite Cardinal holds omega *` iC = iC
theorem Th14: :: METRIZTS:13
theorem Th15: :: METRIZTS:14
theorem Th16: :: METRIZTS:15
theorem Th27: :: METRIZTS:16
Lm7:
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
theorem Th17: :: METRIZTS:17
Lm8:
for TM being metrizable TopSpace
for iC being infinite Cardinal st density TM c= iC holds
weight TM c= iC
theorem Th18: :: METRIZTS:18
theorem Th19: :: METRIZTS:19
theorem Th20: :: METRIZTS:20
theorem Th21: :: METRIZTS:21
theorem Th22: :: METRIZTS:22
theorem Th23: :: METRIZTS:23
:: deftheorem Def2 defines Lindelof METRIZTS:def 2 :
Lm9:
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 ) )
theorem :: METRIZTS:24
Th25:
for TM being metrizable TopSpace holds
( TM is Lindelof iff TM is second-countable )
Th26:
for TM being metrizable TopSpace holds
( TM is Lindelof iff TM is separable )
Lm10:
TopStruct(# the carrier of (TOP-REAL 1),the topology of (TOP-REAL 1) #) is second-countable
:: deftheorem Def3 defines separates METRIZTS:def 3 :
Lm11:
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)
Lm12:
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 )
theorem :: METRIZTS:25
theorem :: METRIZTS:26