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