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 A1, JORDAN5A:27;

hence min (r,f) is continuous by JORDAN5A:27; :: thesis: verum

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 A1, JORDAN5A:27;

now :: thesis: for t being Point of T holds mf9 is_continuous_at t

then
mf9 is continuous
by TMAP_1:50;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 )

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

hence
mf9 is_continuous_at t
by TMAP_1:43; :: thesis: verum
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 )

( U is open & t in U & mf9 .: U c= R ) ; :: thesis: verum

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

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

end;

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 )

( 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 such that

A6: s > 0 and

A7: Ball (ft,s) c= R by A3, TOPMETR:15, TOPMETR:def 6;

reconsider s9 = s as Real ;

reconsider B = Ball (ft,s9) as Subset of R^1 by METRIC_1:def 13, TOPMETR:17;

dist (ft,ft) < s9 by A6, METRIC_1:1;

then A8: ft in B by METRIC_1:11;

( B is open & f9 is_continuous_at t ) by A2, TMAP_1:50, TOPMETR:14, TOPMETR:def 6;

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

(min (r,f)) .: U c= R

( U is open & t in U & (min (r,f)) .: U c= R ) by A9; :: thesis: verum

end;then ft in R by A4, Def9;

then consider s being Real such that

A6: s > 0 and

A7: Ball (ft,s) c= R by A3, TOPMETR:15, TOPMETR:def 6;

reconsider s9 = s as Real ;

reconsider B = Ball (ft,s9) as Subset of R^1 by METRIC_1:def 13, TOPMETR:17;

dist (ft,ft) < s9 by A6, METRIC_1:1;

then A8: ft in B by METRIC_1:11;

( B is open & f9 is_continuous_at t ) by A2, TMAP_1:50, TOPMETR:14, TOPMETR:def 6;

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

(min (r,f)) .: U c= R

proof

hence
ex U being Subset of T st
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 A11, FUNCT_2:def 1;

then A14: f . x in f .: U by A12, FUNCT_1:def 6;

then A15: f . x in B by A10;

end;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 A11, FUNCT_2:def 1;

then A14: f . x in f .: U by A12, FUNCT_1:def 6;

then A15: f . x in B by A10;

now :: thesis: mfx in Rend;

hence
mfx in R
; :: thesis: verumper cases
( f . x <= r or f . x > r )
;

end;

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;then mfx = f . x by A13, Def9;

hence mfx in R by A7, A15; :: thesis: verum

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

dist (fx,ft) < s
by A10, A14, METRIC_1:11;

then A17: |.((f . x) - (f . t)).| < s by TOPMETR:11;

A18: r - (f . t) <= (f . x) - (f . t) by A16, XREAL_1:9;

f . x >= f . t by A5, A16, XXREAL_0:2;

then (f . x) - (f . t) >= 0 by XREAL_1:48;

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

then |.(r - (f . t)).| < s by A19, ABSVALUE:def 1;

then dist (ft,r9) < s by TOPMETR:11;

then A20: r in B by METRIC_1:11;

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;then A17: |.((f . x) - (f . t)).| < s by TOPMETR:11;

A18: r - (f . t) <= (f . x) - (f . t) by A16, XREAL_1:9;

f . x >= f . t by A5, A16, XXREAL_0:2;

then (f . x) - (f . t) >= 0 by XREAL_1:48;

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

then |.(r - (f . t)).| < s by A19, ABSVALUE:def 1;

then dist (ft,r9) < s by TOPMETR:11;

then A20: r in B by METRIC_1:11;

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

( U is open & t in U & (min (r,f)) .: U c= R ) by A9; :: thesis: verum

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 )

( 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 13, TOPMETR:17;

(f . t) - r > 0 by A21, XREAL_1:50;

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 A2, TMAP_1:50, TOPMETR:14, TOPMETR:def 6;

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

(min (r,f)) .: U c= R

( U is open & t in U & (min (r,f)) .: U c= R ) by A23; :: thesis: verum

end;reconsider B = Ball (ft,((f . t) - r)) as Subset of R^1 by METRIC_1:def 13, TOPMETR:17;

(f . t) - r > 0 by A21, XREAL_1:50;

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 A2, TMAP_1:50, TOPMETR:14, TOPMETR:def 6;

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

(min (r,f)) .: U c= R

proof

hence
ex U being Subset of T st
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 A25, FUNCT_2:def 1;

then f . x in f .: U by A26, FUNCT_1:def 6;

then dist (ft,fx) < (f . t) - r by A24, METRIC_1:11;

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 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;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 A25, FUNCT_2:def 1;

then f . x in f .: U by A26, FUNCT_1:def 6;

then dist (ft,fx) < (f . t) - r by A24, METRIC_1:11;

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 A21, XXREAL_0:def 9;

then (min (r,f)) . t = r by Def9;

hence mfx in R by A4, A27, A28, Def9; :: thesis: verum

( U is open & t in U & (min (r,f)) .: U c= R ) by A23; :: thesis: verum

( U is open & t in U & mf9 .: U c= R ) ; :: thesis: verum

hence min (r,f) is continuous by JORDAN5A:27; :: thesis: verum