let M be non empty MetrSpace; :: thesis: for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds
dist_max X is continuous
let X be Subset of (TopSpaceMetr M); :: thesis: ( X <> {} & X is compact implies dist_max X is continuous )
assume A1:
( X <> {} & X is compact )
; :: thesis: dist_max X is continuous
for P being Subset of R^1 st P is open holds
(dist_max X) " P is open
proof
let P be
Subset of
R^1 ;
:: thesis: ( P is open implies (dist_max X) " P is open )
assume A2:
P is
open
;
:: thesis: (dist_max X) " P is open
for
p being
Point of
M st
p in (dist_max X) " P holds
ex
r being
real number st
(
r > 0 &
Ball p,
r c= (dist_max X) " P )
proof
let p be
Point of
M;
:: thesis: ( p in (dist_max X) " P implies ex r being real number st
( r > 0 & Ball p,r c= (dist_max X) " P ) )
assume
p in (dist_max X) " P
;
:: thesis: ex r being real number st
( r > 0 & Ball p,r c= (dist_max X) " P )
then A3:
(
p in dom (dist_max X) &
(dist_max X) . p in P )
by FUNCT_1:def 13;
consider y being
Point of
RealSpace such that A4:
y = upper_bound ((dist p) .: X)
by METRIC_1:def 14;
reconsider P =
P as
Subset of
(TopSpaceMetr RealSpace ) by TOPMETR:def 7;
y in P
by A3, A4, Def7;
then consider r being
real number such that A5:
(
r > 0 &
Ball y,
r c= P )
by A2, TOPMETR:22, TOPMETR:def 7;
reconsider r =
r as
Real by XREAL_0:def 1;
A6:
Ball p,
r c= (dist_max X) " P
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in Ball p,r or z in (dist_max X) " P )
assume A7:
z in Ball p,
r
;
:: thesis: z in (dist_max X) " P
then reconsider z =
z as
Point of
M ;
dist p,
z < r
by A7, METRIC_1:12;
then
(abs ((upper_bound ((dist p) .: X)) - (upper_bound ((dist z) .: X)))) + (dist p,z) < r + (dist p,z)
by A1, Th26, XREAL_1:10;
then A8:
abs ((upper_bound ((dist p) .: X)) - (upper_bound ((dist z) .: X))) < r
by XREAL_1:8;
consider q being
Point of
RealSpace such that A9:
q = upper_bound ((dist z) .: X)
by METRIC_1:def 14;
A10:
q = (dist_max X) . z
by A9, Def7;
dist y,
q < r
by A4, A8, A9, TOPMETR:15;
then A11:
q in Ball y,
r
by METRIC_1:12;
dom (dist_max X) = the
carrier of
(TopSpaceMetr M)
by FUNCT_2:def 1;
then
dom (dist_max X) = the
carrier of
M
by TOPMETR:16;
hence
z in (dist_max X) " P
by A5, A10, A11, FUNCT_1:def 13;
:: thesis: verum
end;
take
r
;
:: thesis: ( r > 0 & Ball p,r c= (dist_max X) " P )
thus
(
r > 0 &
Ball p,
r c= (dist_max X) " P )
by A5, A6;
:: thesis: verum
end;
hence
(dist_max X) " P is
open
by TOPMETR:22;
:: thesis: verum
end;
hence
dist_max X is continuous
by Lm2, TOPS_2:55; :: thesis: verum