begin
Lm1:
for T1, T2 being empty TopSpace holds T1,T2 are_homeomorphic
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
Lm4:
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)
Lm5:
for iC being infinite Cardinal holds omega *` iC = iC
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
Lm7:
for TM being metrizable TopSpace
for iC being infinite Cardinal st density TM c= iC holds
weight TM c= iC
begin
begin
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 ) )
Lm9:
for TM being metrizable TopSpace holds
( TM is Lindelof iff TM is second-countable )
Lm10:
for TM being metrizable TopSpace holds
( TM is Lindelof iff TM is separable )
Lm11:
TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is second-countable
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)
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 )