:: by Leszek Borys

::

:: Received June 8, 1991

:: Copyright (c) 1991-2012 Association of Mizar Users

begin

theorem Th1: :: PCOMPS_1:1

for PM being MetrStruct

for x being Element of PM

for r, p being real number st r <= p holds

Ball (x,r) c= Ball (x,p)

for x being Element of PM

for r, p being real number st r <= p holds

Ball (x,r) c= Ball (x,p)

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 )

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:7

:: deftheorem Def1 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 ) );

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

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

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

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;

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

for Z being Subset of T holds

( Z in b_{1} iff ex W being Subset of T st

( Z = Cl W & W in FX ) )

for b_{1}, b_{2} being Subset-Family of T st ( for Z being Subset of T holds

( Z in b_{1} iff ex W being Subset of T st

( Z = Cl W & W in FX ) ) ) & ( for Z being Subset of T holds

( Z in b_{2} iff ex W being Subset of T st

( Z = Cl W & W in FX ) ) ) holds

b_{1} = b_{2}

end;
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 for Z being Subset of T holds

( Z in it iff ex W being Subset of T st

( Z = Cl W & W in FX ) );

ex b

for Z being Subset of T holds

( Z in b

( Z = Cl W & W in FX ) )

proof end;

uniqueness for b

( Z in b

( Z = Cl W & W in FX ) ) ) & ( for Z being Subset of T holds

( Z in b

( Z = Cl W & W in FX ) ) ) holds

b

proof end;

:: deftheorem Def2 defines clf PCOMPS_1:def 2 :

for T being TopStruct

for FX, b_{3} being Subset-Family of T holds

( b_{3} = clf FX iff for Z being Subset of T holds

( Z in b_{3} iff ex W being Subset of T st

( Z = Cl W & W in FX ) ) );

for T being TopStruct

for FX, b

( b

( Z in b

( Z = Cl W & W in FX ) ) );

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)}

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

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)

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)

for FX being Subset-Family of T st FX is finite holds

Cl (union FX) = union (clf FX)

proof end;

scheme :: PCOMPS_1:sch 1

Lambda1top{ F_{1}() -> TopSpace, F_{2}() -> Subset-Family of F_{1}(), F_{3}() -> Subset-Family of F_{1}(), F_{4}( set ) -> Subset of F_{1}() } :

Lambda1top{ F

ex f being Function of F_{2}(),F_{3}() st

for Z being Subset of F_{1}() st Z in F_{2}() holds

f . Z = F_{4}(Z)

provided
for Z being Subset of F

f . Z = 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

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;

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)

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

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 ;

end;
attr IT is paracompact means :Def3: :: 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 );

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 );

:: deftheorem Def3 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 ) );

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 ) );

theorem Th23: :: PCOMPS_1:23

for T being non empty TopSpace

for B, A 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 )

for B, A 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;

definition

let PM be MetrStruct ;

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

for V being Subset of PM holds

( V in b_{1} 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 b_{1}, b_{2} being Subset-Family of PM st ( for V being Subset of PM holds

( V in b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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 ) );

ex b

for V being Subset of PM holds

( V in b

ex r being Real st

( r > 0 & Ball (x,r) c= V ) )

proof end;

uniqueness for b

( V in b

ex r being Real st

( r > 0 & Ball (x,r) c= V ) ) ) & ( for V being Subset of PM holds

( V in b

ex r being Real st

( r > 0 & Ball (x,r) c= V ) ) ) holds

b

proof end;

:: deftheorem Def4 defines Family_open_set PCOMPS_1:def 4 :

for PM being MetrStruct

for b_{2} being Subset-Family of PM holds

( b_{2} = Family_open_set PM iff for V being Subset of PM holds

( V in b_{2} 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 PM being MetrStruct

for b

( b

( V in b

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 )

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 y, x being Element of PM

for r being real number st PM is triangle & y in Ball (x,r) holds

ex p being Real st

( p > 0 & Ball (y,p) c= Ball (x,r) )

for y, x being Element of PM

for r being real number 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 y, x, 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) )

for r, p being Real

for y, x, 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 number st PM is triangle holds

Ball (x,r) in Family_open_set PM

for x being Element of PM

for r being real number st PM is triangle holds

Ball (x,r) 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

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

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

union A in Family_open_set PM

proof end;

definition

let PM be MetrStruct ;

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

end;
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) #);

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

:: deftheorem defines TopSpaceMetr PCOMPS_1:def 5 :

for PM being MetrStruct holds TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #);

for PM being MetrStruct holds TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #);

registration

let PM be MetrStruct ;

coherence

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

end;
coherence

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

registration

existence

ex b_{1} being TopSpace st

( b_{1} is T_2 & not b_{1} is empty & b_{1} is strict )

end;
ex b

( b

proof end;

:: Metric on a set

:: deftheorem Def6 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)) ) );

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 )

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 ;

coherence

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

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

assume A1: f is_metric_of D ;

coherence

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

:: 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 #);

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 ;

end;
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 );

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 );

:: 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 ) );

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
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

for f being Function of [:D,D:],REAL st f is_metric_of D holds

not SpaceMetr (D,f) is empty

proof end;