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:17;
A2: f9 is continuous by ;
now :: thesis: for t being Point of T holds mf9 is_continuous_at t
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 13;
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 :: thesis: ex U being Subset of T st
( U is open & t in U & (min (r,f)) .: U c= R )
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 ;
then consider s being Real such that
A6: s > 0 and
A7: Ball (ft,s) c= R by ;
reconsider s9 = s as Real ;
reconsider B = Ball (ft,s9) as Subset of R^1 by ;
dist (ft,ft) < s9 by ;
then A8: ft in B by METRIC_1:11;
( B is open & f9 is_continuous_at t ) by ;
then consider U being Subset of T such that
A9: ( U is open & t in U ) and
A10: f9 .: U c= B by ;
(min (r,f)) .: U c= R
proof
let mfx be object ; :: 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 object 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 6;
reconsider x = x as Point of T by A11;
( f . x in REAL & r in REAL ) by XREAL_0:def 1;
then reconsider fx = f . x, r9 = r as Point of RealSpace by METRIC_1:def 13;
dom (min (r,f)) = the carrier of T by FUNCT_2:def 1;
then x in dom f by ;
then A14: f . x in f .: U by ;
then A15: f . x in B by A10;
now :: thesis: mfx in R
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 ;
hence mfx in R by ; :: thesis: verum
end;
suppose A16: f . x > r ; :: thesis: mfx in R
dist (fx,ft) < s by ;
then A17: |.((f . x) - (f . t)).| < s by TOPMETR:11;
A18: r - (f . t) <= (f . x) - (f . t) by ;
f . x >= f . t by ;
then (f . x) - (f . t) >= 0 by XREAL_1:48;
then (f . x) - (f . t) < s by ;
then A19: r - (f . t) < s by ;
r - (f . t) >= 0 by ;
then |.(r - (f . t)).| < s by ;
then dist (ft,r9) < s by TOPMETR:11;
then A20: r in B by METRIC_1:11;
min (r,(f . x)) = r by ;
then mfx = r by ;
hence mfx in R by ; :: 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 ;
(f . t) - r > 0 by ;
then dist (ft,ft) < (f . t) - r by METRIC_1:1;
then A22: ft in B by METRIC_1:11;
( B is open & f9 is_continuous_at t ) by ;
then consider U being Subset of T such that
A23: ( U is open & t in U ) and
A24: f9 .: U c= B by ;
(min (r,f)) .: U c= R
proof
let mfx be object ; :: 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 object 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 6;
reconsider x = x as Point of T by A25;
reconsider fx = f . x as Point of RealSpace by METRIC_1:def 13;
dom (min (r,f)) = the carrier of T by FUNCT_2:def 1;
then x in dom f by ;
then f . x in f .: U by ;
then dist (ft,fx) < (f . t) - r by ;
then |.((f . t) - (f . x)).| < (f . t) - r by TOPMETR:11;
then (f . t) + (- (f . x)) <= (f . t) + (- r) by ABSVALUE:5;
then - (f . x) <= - r by XREAL_1:6;
then r <= f . x by XREAL_1:24;
then A28: min (r,(f . x)) = r by XXREAL_0:def 9;
min (r,(f . t)) = r by ;
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:43; :: thesis: verum
end;
then mf9 is continuous by TMAP_1:50;
hence min (r,f) is continuous by JORDAN5A:27; :: thesis: verum