let T be non empty TopSpace; :: thesis: for r being Real
for f being RealMap of T st f is continuous holds
min r,f is continuous
let r be Real; :: thesis: for f being RealMap of T st f is continuous holds
min r,f is continuous
let f be RealMap of T; :: thesis: ( f is continuous implies min r,f is continuous )
assume A1: f is continuous ; :: thesis: min r,f is continuous
reconsider f9 = f, mf9 = min r,f as Function of T,R^1 by TOPMETR:24;
A2: f9 is continuous by A1, TOPREAL6:83;

now

let t be Point of T; :: thesis: mf9 is_continuous_at t
for R being Subset of R^1 st R is open & mf9 . t in R holds
ex U being Subset of T st
( U is open & t in U & mf9 .: U c= R )

proof

reconsider ft = f . t as Point of RealSpace by METRIC_1:def 14;
let R be Subset of R^1 ; :: thesis: ( R is open & mf9 . t in R implies ex U being Subset of T st
( U is open & t in U & mf9 .: U c= R ) )
assume that
A3: R is open and
A4: mf9 . t in R ; :: thesis: ex U being Subset of T st
( U is open & t in U & mf9 .: U c= R )

now

per cases ( f . t <= r or f . t > r ) ;

suppose A5: f . t <= r ; :: thesis: ex U being Subset of T st
( U is open & t in U & (min r,f) .: U c= R )

then f . t = min r,(f . t) by XXREAL_0:def 9;
then ft in R by A4, Def9;
then consider s being real number such that
A6: s > 0 and
A7: Ball ft,s c= R by A3, TOPMETR:22, TOPMETR:def 7;
reconsider s9 = s as Real by XREAL_0:def 1;
reconsider B = Ball ft,s9 as Subset of R^1 by METRIC_1:def 14, TOPMETR:24;
dist ft,ft < s9 by A6, METRIC_1:1;
then A8: ft in B by METRIC_1:12;
( B is open & f9 is_continuous_at t ) by A2, TMAP_1:55, TOPMETR:21, TOPMETR:def 7;
then consider U being Subset of T such that
A9: ( U is open & t in U ) and
A10: f9 .: U c= B by A8, TMAP_1:48;
(min r,f) .: U c= R

proof

let mfx be set ; :: according to TARSKI:def 3 :: thesis: ( not mfx in (min r,f) .: U or mfx in R )
assume mfx in (min r,f) .: U ; :: thesis: mfx in R
then consider x being set such that
A11: x in dom (min r,f) and
A12: x in U and
A13: mfx = (min r,f) . x by FUNCT_1:def 12;
reconsider x = x as Point of T by A11;
reconsider fx = f . x, r9 = r as Point of RealSpace by METRIC_1:def 14;
dom (min r,f) = the carrier of T by FUNCT_2:def 1;
then x in dom f by A11, FUNCT_2:def 1;
then A14: f . x in f .: U by A12, FUNCT_1:def 12;
then A15: f . x in B by A10;

now

per cases ( f . x <= r or f . x > r ) ;

suppose f . x <= r ; :: thesis: mfx in R

then min r,(f . x) = f . x by XXREAL_0:def 9;
then mfx = f . x by A13, Def9;
hence mfx in R by A7, A15; :: thesis: verum

end;

suppose A16: f . x > r ; :: thesis: mfx in R

dist fx,ft < s by A10, A14, METRIC_1:12;
then A17: abs ((f . x) - (f . t)) < s by TOPMETR:15;
A18: r - (f . t) <= (f . x) - (f . t) by A16, XREAL_1:11;
f . x >= f . t by A5, A16, XXREAL_0:2;
then (f . x) - (f . t) >= 0 by XREAL_1:50;
then (f . x) - (f . t) < s by A17, ABSVALUE:def 1;
then A19: r - (f . t) < s by A18, XXREAL_0:2;
r - (f . t) >= 0 by A5, XREAL_1:50;
then abs (r - (f . t)) < s by A19, ABSVALUE:def 1;
then dist ft,r9 < s by TOPMETR:15;
then A20: r in B by METRIC_1:12;
min r,(f . x) = r by A16, XXREAL_0:def 9;
then mfx = r by A13, Def9;
hence mfx in R by A7, A20; :: thesis: verum

end;

end;

end;

hence mfx in R ; :: thesis: verum

end;

hence ex U being Subset of T st
( U is open & t in U & (min r,f) .: U c= R ) by A9; :: thesis: verum

end;

suppose A21: f . t > r ; :: thesis: ex U being Subset of T st
( U is open & t in U & (min r,f) .: U c= R )

set s = (f . t) - r;
reconsider B = Ball ft,((f . t) - r) as Subset of R^1 by METRIC_1:def 14, TOPMETR:24;
(f . t) - r > 0 by A21, XREAL_1:52;
then dist ft,ft < (f . t) - r by METRIC_1:1;
then A22: ft in B by METRIC_1:12;
( B is open & f9 is_continuous_at t ) by A2, TMAP_1:55, TOPMETR:21, TOPMETR:def 7;
then consider U being Subset of T such that
A23: ( U is open & t in U ) and
A24: f9 .: U c= B by A22, TMAP_1:48;
(min r,f) .: U c= R

proof

let mfx be set ; :: according to TARSKI:def 3 :: thesis: ( not mfx in (min r,f) .: U or mfx in R )
assume mfx in (min r,f) .: U ; :: thesis: mfx in R
then consider x being set such that
A25: x in dom (min r,f) and
A26: x in U and
A27: mfx = (min r,f) . x by FUNCT_1:def 12;
reconsider x = x as Point of T by A25;
reconsider fx = f . x as Point of RealSpace by METRIC_1:def 14;
dom (min r,f) = the carrier of T by FUNCT_2:def 1;
then x in dom f by A25, FUNCT_2:def 1;
then f . x in f .: U by A26, FUNCT_1:def 12;
then dist ft,fx < (f . t) - r by A24, METRIC_1:12;
then abs ((f . t) - (f . x)) < (f . t) - r by TOPMETR:15;
then (f . t) + (- (f . x)) <= (f . t) + (- r) by ABSVALUE:12;
then - (f . x) <= - r by XREAL_1:8;
then r <= f . x by XREAL_1:26;
then A28: min r,(f . x) = r by XXREAL_0:def 9;
min r,(f . t) = r by A21, XXREAL_0:def 9;
then (min r,f) . t = r by Def9;
hence mfx in R by A4, A27, A28, Def9; :: thesis: verum

end;

hence ex U being Subset of T st
( U is open & t in U & (min r,f) .: U c= R ) by A23; :: thesis: verum

end;

end;

end;

hence ex U being Subset of T st
( U is open & t in U & mf9 .: U c= R ) ; :: thesis: verum

end;

hence mf9 is_continuous_at t by TMAP_1:48; :: thesis: verum

end;

then mf9 is continuous by TMAP_1:55;
hence min r,f is continuous by TOPREAL6:83; :: thesis: verum