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 f' = f, mf' = min r,f as Function of T,R^1 by TOPMETR:24;
A2: f' is continuous by A1, TOPREAL6:83;

now

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

proof

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

now

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

suppose A4: 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 A3, Def9;
then consider s being real number such that
A5: ( s > 0 & Ball ft,s c= R ) by A3, TOPMETR:22, TOPMETR:def 7;
reconsider s' = s as Real by XREAL_0:def 1;
reconsider B = Ball ft,s' as Subset of R^1 by METRIC_1:def 14, TOPMETR:24;
dist ft,ft < s' by A5, METRIC_1:1;
then ( ft in B & B is open & f' is_continuous_at t ) by A2, METRIC_1:12, TMAP_1:55, TOPMETR:21, TOPMETR:def 7;
then consider U being Subset of T such that
A6: ( U is open & t in U & f' .: U c= B ) by 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 A7: mfx in (min r,f) .: U ; :: thesis: mfx in R
consider x being set such that
A8: ( x in dom (min r,f) & x in U & mfx = (min r,f) . x ) by A7, FUNCT_1:def 12;
reconsider x = x as Point of T by A8;
reconsider fx = f . x, r' = 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 A8, FUNCT_2:def 1;
then A9: f . x in f .: U by A8, FUNCT_1:def 12;
then A10: f . x in B by A6;

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 A8, Def9;
hence mfx in R by A5, A10; :: thesis: verum

end;

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

then ( f . x >= f . t & dist fx,ft < s ) by A4, A6, A9, METRIC_1:12, XXREAL_0:2;
then ( (f . x) - (f . t) >= 0 & abs ((f . x) - (f . t)) < s ) by TOPMETR:15, XREAL_1:50;
then ( (f . x) - (f . t) < s & r - (f . t) <= (f . x) - (f . t) ) by A11, ABSVALUE:def 1, XREAL_1:11;
then ( r - (f . t) < s & r - (f . t) >= 0 ) by A4, XREAL_1:50, XXREAL_0:2;
then abs (r - (f . t)) < s by ABSVALUE:def 1;
then ( dist ft,r' < s & min r,(f . x) = r ) by A11, TOPMETR:15, XXREAL_0:def 9;
then ( r in B & mfx = r ) by A8, Def9, METRIC_1:12;
hence mfx in R by A5; :: 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 A6; :: thesis: verum

end;

suppose A12: 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 A12, XREAL_1:52;
then dist ft,ft < (f . t) - r by METRIC_1:1;
then ( ft in B & B is open & f' is_continuous_at t ) by A2, METRIC_1:12, TMAP_1:55, TOPMETR:21, TOPMETR:def 7;
then consider U being Subset of T such that
A13: ( U is open & t in U & f' .: U c= B ) by 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 A14: mfx in (min r,f) .: U ; :: thesis: mfx in R
consider x being set such that
A15: ( x in dom (min r,f) & x in U & mfx = (min r,f) . x ) by A14, FUNCT_1:def 12;
reconsider x = x as Point of T by A15;
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 A15, FUNCT_2:def 1;
then f . x in f .: U by A15, FUNCT_1:def 12;
then dist ft,fx < (f . t) - r by A13, 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 & min r,(f . t) = r ) by A12, XREAL_1:26, XXREAL_0:def 9;
then ( min r,(f . x) = r & (min r,f) . t = r ) by Def9, XXREAL_0:def 9;
hence mfx in R by A3, A15, 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 A13; :: thesis: verum

end;

end;

end;

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

end;

hence mf' is_continuous_at t by TMAP_1:48; :: thesis: verum

end;

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