let f, g be Function of REAL,REAL; for a being Real st g is continuous & ( for x being Real holds f . x = min (a,(g . x)) ) holds
f is continuous
let a be Real; ( g is continuous & ( for x being Real holds f . x = min (a,(g . x)) ) implies f is continuous )
assume A1a:
g is continuous
; ( ex x being Real st not f . x = min (a,(g . x)) or f is continuous )
assume A0:
for x being Real holds f . x = min (a,(g . x))
; f is continuous
reconsider f = f as PartFunc of REAL,REAL ;
for x0 being Real st x0 in dom f holds
f is_continuous_in x0
proof
let x0 be
Real;
( x0 in dom f implies f is_continuous_in x0 )
assume A2:
x0 in dom f
;
f is_continuous_in x0
A3a:
(
dom f = REAL &
dom g = REAL )
by FUNCT_2:def 1;
for
r being
Real st
0 < r holds
ex
s being
Real st
(
0 < s & ( for
x1 being
Real st
x1 in dom f &
|.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) )
proof
let r be
Real;
( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) ) )
assume A4:
0 < r
;
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) )
consider s being
Real such that S1:
0 < s
and S2:
for
x1 being
Real st
x1 in dom g &
|.(x1 - x0).| < s holds
|.((g . x1) - (g . x0)).| < r
by A3a, FCONT_1:3, A1a, A2, A4;
take
s
;
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) )
for
x1 being
Real st
x1 in dom f &
|.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r
proof
let x1 be
Real;
( x1 in dom f & |.(x1 - x0).| < s implies |.((f . x1) - (f . x0)).| < r )
assume S6:
x1 in dom f
;
( not |.(x1 - x0).| < s or |.((f . x1) - (f . x0)).| < r )
S8a:
(
dom f = REAL &
dom g = REAL )
by FUNCT_2:def 1;
assume S7:
|.(x1 - x0).| < s
;
|.((f . x1) - (f . x0)).| < r
S5: 2
* |.((f . x1) - (f . x0)).| =
2
* |.((f . x1) - (min (a,(g . x0)))).|
by A0
.=
2
* |.((min (a,(g . x1))) - (min (a,(g . x0)))).|
by A0
.=
2
* |.((min (a,(g . x1))) - (((a + (g . x0)) - |.(a - (g . x0)).|) / 2)).|
by COMPLEX1:73
.=
2
* |.((((a + (g . x1)) - |.(a - (g . x1)).|) / 2) - (((a + (g . x0)) - |.(a - (g . x0)).|) / 2)).|
by COMPLEX1:73
.=
2
* |.((((a + (g . x1)) - |.(a - (g . x1)).|) - ((a + (g . x0)) - |.(a - (g . x0)).|)) / 2).|
.=
2
* (|.(((a + (g . x1)) - |.(a - (g . x1)).|) - ((a + (g . x0)) - |.(a - (g . x0)).|)).| / |.2.|)
by COMPLEX1:67
.=
2
* (|.(((a + (g . x1)) - |.(a - (g . x1)).|) - ((a + (g . x0)) - |.(a - (g . x0)).|)).| / 2)
by COMPLEX1:43
.=
|.(((g . x1) - (g . x0)) + (|.(a - (g . x0)).| - |.(a - (g . x1)).|)).|
;
|.((g . x1) - (g . x0)).| < r
by S2, S7, S8a, S6;
then S4:
|.((g . x1) - (g . x0)).| + |.((g . x1) - (g . x0)).| < r + r
by XREAL_1:8;
S3:
|.(((g . x1) - (g . x0)) + (|.(a - (g . x0)).| - |.(a - (g . x1)).|)).| <= |.((g . x1) - (g . x0)).| + |.(|.(a - (g . x0)).| - |.(a - (g . x1)).|).|
by COMPLEX1:56;
|.(|.(a - (g . x0)).| - |.(a - (g . x1)).|).| <= |.((a - (g . x0)) - (a - (g . x1))).|
by COMPLEX1:64;
then
|.((g . x1) - (g . x0)).| + |.(|.(a - (g . x0)).| - |.(a - (g . x1)).|).| <= |.((g . x1) - (g . x0)).| + |.((- (g . x0)) + (g . x1)).|
by XREAL_1:7;
then
|.((g . x1) - (g . x0)).| + |.(|.(a - (g . x0)).| - |.(a - (g . x1)).|).| < 2
* r
by S4, XXREAL_0:2;
then
2
* |.((f . x1) - (f . x0)).| < 2
* r
by S5, S3, XXREAL_0:2;
then
(2 * |.((f . x1) - (f . x0)).|) / 2
< (2 * r) / 2
by XREAL_1:74;
hence
|.((f . x1) - (f . x0)).| < r
;
verum
end;
hence
(
0 < s & ( for
x1 being
Real st
x1 in dom f &
|.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) )
by S1;
verum
end;
hence
f is_continuous_in x0
by FCONT_1:3;
verum
end;
hence
f is continuous
; verum