:: Paracompact and Metrizable Spaces
:: by Leszek Borys
::
:: Received June 8, 1991
:: Copyright (c) 1991-2021 Association of Mizar Users

theorem Th1: :: PCOMPS_1:1

for PM being MetrStruct
for x being Element of PM
for r, p being Real st r <= p holds
Ball (x,r) c= Ball (x,p)

proof end;

theorem Th2: :: PCOMPS_1:2

for T being TopSpace
for A being Subset of T holds
( Cl A <> {} iff A <> {} )

proof end;

theorem Th3: :: PCOMPS_1:3

for T being non empty TopSpace
for FX being Subset-Family of T st FX is Cover of T holds
for x being Point of T ex W being Subset of T st
( x in W & W in FX )

proof end;

theorem :: PCOMPS_1:4

for a being set holds the topology of (1TopSp a) = bool a ;

theorem :: PCOMPS_1:5

for a being set holds the carrier of (1TopSp a) = a ;

theorem :: PCOMPS_1:6

for a being set holds 1TopSp {a} is compact ;

theorem :: PCOMPS_1:7

for T being non empty TopSpace
for x being Point of T st T is T_2 holds
{x} is closed ;

definition

let T be TopStruct ;
let IT be Subset-Family of T;

attr IT is locally_finite means :: PCOMPS_1:def 1
for x being Point of T ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in IT & V meets W ) } is finite );

end;

:: deftheorem defines locally_finite PCOMPS_1:def 1 :
for T being TopStruct
for IT being Subset-Family of T holds
( IT is locally_finite iff for x being Point of T ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in IT & V meets W ) } is finite ) );

theorem Th8: :: PCOMPS_1:8

for T being non empty TopSpace
for FX being Subset-Family of T
for W being Subset of T holds { V where V is Subset of T : ( V in FX & V meets W ) } c= FX

proof end;

theorem Th9: :: PCOMPS_1:9

for T being non empty TopSpace
for FX, GX being Subset-Family of T st FX c= GX & GX is locally_finite holds
FX is locally_finite

proof end;

theorem Th10: :: PCOMPS_1:10

for T being non empty TopSpace
for FX being Subset-Family of T st FX is finite holds
FX is locally_finite

proof end;

definition

let T be TopStruct ;
let FX be Subset-Family of T;

func clf FX -> Subset-Family of T means :Def2: :: PCOMPS_1:def 2
for Z being Subset of T holds
( Z in it iff ex W being Subset of T st
( Z = Cl W & W in FX ) );

existence
ex b₁ being Subset-Family of T st
for Z being Subset of T holds
( Z in b₁ iff ex W being Subset of T st
( Z = Cl W & W in FX ) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of T st ( for Z being Subset of T holds
( Z in b₁ iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) & ( for Z being Subset of T holds
( Z in b₂ iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines clf PCOMPS_1:def 2 :
for T being TopStruct
for FX, b₃ being Subset-Family of T holds
( b₃ = clf FX iff for Z being Subset of T holds
( Z in b₃ iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) );

theorem :: PCOMPS_1:11

for T being TopSpace
for FX being Subset-Family of T holds clf FX is closed

proof end;

theorem Th12: :: PCOMPS_1:12

for T being TopSpace
for FX being Subset-Family of T st FX = {} holds
clf FX = {}

proof end;

theorem Th13: :: PCOMPS_1:13

for T being non empty TopSpace
for V being Subset of T
for FX being Subset-Family of T st FX = {V} holds
clf FX = {(Cl V)}

proof end;

theorem Th14: :: PCOMPS_1:14

for T being non empty TopSpace
for FX, GX being Subset-Family of T st FX c= GX holds
clf FX c= clf GX

proof end;

theorem Th15: :: PCOMPS_1:15

for T being non empty TopSpace
for FX, GX being Subset-Family of T holds clf (FX \/ GX) = (clf FX) \/ (clf GX)

proof end;

theorem Th16: :: PCOMPS_1:16

for T being non empty TopSpace
for FX being Subset-Family of T st FX is finite holds
Cl (union FX) = union (clf FX)

proof end;

theorem Th17: :: PCOMPS_1:17

for T being non empty TopSpace
for FX being Subset-Family of T holds FX is_finer_than clf FX

proof end;

scheme :: PCOMPS_1:sch 1
Lambda1top{ F₁() -> TopSpace, F₂() -> Subset-Family of F₁(), F₃() -> Subset-Family of F₁(), F₄( object ) -> Subset of F₁() } :

ex f being Function of F₂(),F₃() st
for Z being Subset of F₁() st Z in F₂() holds
f . Z = F₄(Z)

provided

A1: for Z being Subset of F₁() st Z in F₂() holds
F₄(Z) in F₃()

proof end;

theorem :: PCOMPS_1:18

for T being non empty TopSpace
for FX being Subset-Family of T st FX is locally_finite holds
clf FX is locally_finite

proof end;

theorem :: PCOMPS_1:19

for T being non empty TopSpace
for FX being Subset-Family of T holds union FX c= union (clf FX) by Th17, SETFAM_1:13;

theorem Th20: :: PCOMPS_1:20

for T being non empty TopSpace
for FX being Subset-Family of T st FX is locally_finite holds
Cl (union FX) = union (clf FX)

proof end;

theorem :: PCOMPS_1:21

for T being non empty TopSpace
for FX being Subset-Family of T st FX is locally_finite & FX is closed holds
union FX is closed

proof end;

definition

let IT be TopStruct ;

attr IT is paracompact means :: PCOMPS_1:def 3
for FX being Subset-Family of IT st FX is Cover of IT & FX is open holds
ex GX being Subset-Family of IT st
( GX is open & GX is Cover of IT & GX is_finer_than FX & GX is locally_finite );

end;

:: deftheorem defines paracompact PCOMPS_1:def 3 :
for IT being TopStruct holds
( IT is paracompact iff for FX being Subset-Family of IT st FX is Cover of IT & FX is open holds
ex GX being Subset-Family of IT st
( GX is open & GX is Cover of IT & GX is_finer_than FX & GX is locally_finite ) );

registration

cluster non empty TopSpace-like paracompact for TopStruct ;

existence
ex b₁ being non empty TopSpace st b₁ is paracompact

proof end;

end;

theorem :: PCOMPS_1:22

for T being non empty TopSpace st T is compact holds
T is paracompact

proof end;

theorem Th23: :: PCOMPS_1:23

for T being non empty TopSpace
for A, B being Subset of T st T is paracompact & B is closed & ( for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ) holds
ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )

proof end;

theorem Th24: :: PCOMPS_1:24

for T being non empty TopSpace st T is T_2 & T is paracompact holds
T is regular

proof end;

theorem :: PCOMPS_1:25

for T being non empty TopSpace st T is T_2 & T is paracompact holds
T is normal

proof end;

definition

let PM be MetrStruct ;

func Family_open_set PM -> Subset-Family of PM means :Def4: :: PCOMPS_1:def 4
for V being Subset of PM holds
( V in it iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) );

existence
ex b₁ being Subset-Family of PM st
for V being Subset of PM holds
( V in b₁ iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of PM st ( for V being Subset of PM holds
( V in b₁ iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) & ( for V being Subset of PM holds
( V in b₂ iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Family_open_set PCOMPS_1:def 4 :
for PM being MetrStruct
for b₂ being Subset-Family of PM holds
( b₂ = Family_open_set PM iff for V being Subset of PM holds
( V in b₂ iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) );

theorem Th26: :: PCOMPS_1:26

for PM being MetrStruct
for x being Element of PM ex r being Real st
( r > 0 & Ball (x,r) c= the carrier of PM )

proof end;

theorem Th27: :: PCOMPS_1:27

for PM being MetrStruct
for x, y being Element of PM
for r being Real st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )

proof end;

theorem :: PCOMPS_1:28

for PM being MetrStruct
for r, p being Real
for x, y, z being Element of PM st PM is triangle & y in (Ball (x,r)) /\ (Ball (z,p)) holds
ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) )

proof end;

theorem Th29: :: PCOMPS_1:29

for PM being MetrStruct
for x being Element of PM
for r being Real st PM is triangle holds
Ball (x,r) in Family_open_set PM

proof end;

theorem Th30: :: PCOMPS_1:30

for PM being MetrStruct holds the carrier of PM in Family_open_set PM

proof end;

theorem Th31: :: PCOMPS_1:31

for PM being MetrStruct
for V, W being Subset of PM st V in Family_open_set PM & W in Family_open_set PM holds
V /\ W in Family_open_set PM

proof end;

theorem Th32: :: PCOMPS_1:32

for PM being MetrStruct
for A being Subset-Family of PM st A c= Family_open_set PM holds
union A in Family_open_set PM

proof end;

theorem Th33: :: PCOMPS_1:33

for PM being MetrStruct holds TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopSpace

proof end;

definition

let PM be MetrStruct ;

func TopSpaceMetr PM -> TopStruct equals :: PCOMPS_1:def 5
TopStruct(# the carrier of PM,(Family_open_set PM) #);

coherence
TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopStruct ;

end;

:: deftheorem defines TopSpaceMetr PCOMPS_1:def 5 :
for PM being MetrStruct holds TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #);

registration

let PM be MetrStruct ;

cluster TopSpaceMetr PM -> strict TopSpace-like ;

coherence
( TopSpaceMetr PM is strict & TopSpaceMetr PM is TopSpace-like ) by Th33;

end;

registration

let PM be non empty MetrStruct ;

cluster TopSpaceMetr PM -> non empty ;

coherence
not TopSpaceMetr PM is empty ;

end;

theorem Th34: :: PCOMPS_1:34

for PM being non empty MetrSpace holds TopSpaceMetr PM is T_2

proof end;

registration

cluster non empty strict TopSpace-like T_2 for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is T_2 & not b₁ is empty & b₁ is strict )

proof end;

end;

:: Metric on a set

definition

let D be set ;
let f be Function of [:D,D:],REAL;

pred f is_metric_of D means :: PCOMPS_1:def 6
for a, b, c being Element of D holds
( ( f . (a,b) = 0 implies a = b ) & ( a = b implies f . (a,b) = 0 ) & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) );

end;

:: deftheorem defines is_metric_of PCOMPS_1:def 6 :
for D being set
for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff for a, b, c being Element of D holds
( ( f . (a,b) = 0 implies a = b ) & ( a = b implies f . (a,b) = 0 ) & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) );

theorem Th35: :: PCOMPS_1:35

for D being set
for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )

proof end;

definition

let D be set ;
let f be Function of [:D,D:],REAL;
assume A1: f is_metric_of D ;

func SpaceMetr (D,f) -> strict MetrSpace equals :Def7: :: PCOMPS_1:def 7
MetrStruct(# D,f #);

coherence
MetrStruct(# D,f #) is strict MetrSpace by A1, Th35;

end;

:: deftheorem Def7 defines SpaceMetr PCOMPS_1:def 7 :
for D being set
for f being Function of [:D,D:],REAL st f is_metric_of D holds
SpaceMetr (D,f) = MetrStruct(# D,f #);

:: Metrizable topological spaces

definition

let IT be TopStruct ;

attr IT is metrizable means :: PCOMPS_1:def 8
ex f being Function of [: the carrier of IT, the carrier of IT:],REAL st
( f is_metric_of the carrier of IT & Family_open_set (SpaceMetr ( the carrier of IT,f)) = the topology of IT );

end;

:: deftheorem defines metrizable PCOMPS_1:def 8 :
for IT being TopStruct holds
( IT is metrizable iff ex f being Function of [: the carrier of IT, the carrier of IT:],REAL st
( f is_metric_of the carrier of IT & Family_open_set (SpaceMetr ( the carrier of IT,f)) = the topology of IT ) );

registration

cluster non empty strict TopSpace-like metrizable for TopStruct ;

existence
ex b₁ being non empty TopSpace st
( b₁ is strict & b₁ is metrizable )

proof end;

end;

theorem :: PCOMPS_1:36

for D being non empty set
for f being Function of [:D,D:],REAL st f is_metric_of D holds
not SpaceMetr (D,f) is empty

proof end;