let f be Function of R^1,R^1; ( ex a, b being Real st
for x being Real holds f . x = (a * x) + b implies f is continuous )
given a, b being Real such that A1:
for x being Real holds f . x = (a * x) + b
; f is continuous
for W being Point of R^1
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
proof
let W be
Point of
R^1;
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= Glet G be
a_neighborhood of
f . W;
ex H being a_neighborhood of W st f .: H c= G
reconsider Y =
f . W as
Point of
RealSpace ;
A2:
f . W in Int G
by CONNSP_2:def 1;
then consider Q being
Subset of
R^1 such that A3:
Q is
open
and A4:
Q c= G
and A5:
f . W in Q
by TOPS_1:22;
consider r being
Real such that A6:
r > 0
and A7:
Ball (
Y,
r)
c= Q
by A3, A5, Th15;
now ex H being a_neighborhood of W st f .: H c= Gper cases
( a = 0 or a <> 0 )
;
suppose A14:
a <> 0
;
ex H being a_neighborhood of W st f .: H c= Greconsider W9 =
W as
Point of
RealSpace ;
set d =
r / (2 * |.a.|);
reconsider H =
Ball (
W9,
(r / (2 * |.a.|))) as
Subset of
R^1 ;
H is
open
by Th14;
then A15:
Int H = H
by TOPS_1:23;
|.a.| > 0
by A14, COMPLEX1:47;
then
2
* |.a.| > 0
by XREAL_1:129;
then
W in Int H
by A6, A15, TBSP_1:11, XREAL_1:139;
then reconsider H =
H as
a_neighborhood of
W by CONNSP_2:def 1;
A16:
f .: H c= Ball (
Y,
r)
proof
reconsider W99 =
W9 as
Real ;
let y be
object ;
TARSKI:def 3 ( not y in f .: H or y in Ball (Y,r) )
reconsider Y9 =
Y as
Real ;
assume
y in f .: H
;
y in Ball (Y,r)
then consider x being
object such that A17:
x in dom f
and A18:
x in H
and A19:
y = f . x
by FUNCT_1:def 6;
reconsider x9 =
x as
Point of
RealSpace by A18;
reconsider y9 =
y as
Element of
REAL by A17, A19, FUNCT_2:5;
reconsider x99 =
x9 as
Real ;
reconsider yy =
y9 as
Point of
RealSpace ;
A20:
|.a.| > 0
by A14, COMPLEX1:47;
dist (
W9,
x9)
< r / (2 * |.a.|)
by A18, METRIC_1:11;
then
|.(W99 - x99).| < r / (2 * |.a.|)
by Th11;
then
|.a.| * |.(W99 - x99).| < |.a.| * (r / (2 * |.a.|))
by A20, XREAL_1:68;
then
|.(a * (W99 - x99)).| < |.a.| * (r / (2 * |.a.|))
by COMPLEX1:65;
then
|.(((a * W99) + b) - ((a * x99) + b)).| < |.a.| * (r / (2 * |.a.|))
;
then
|.(Y9 - ((a * x99) + b)).| < |.a.| * (r / (2 * |.a.|))
by A1;
then A21:
|.(Y9 - y9).| < |.a.| * (r / (2 * |.a.|))
by A1, A19;
|.a.| <> 0
by A14, ABSVALUE:2;
then A22:
|.a.| * (r / (2 * |.a.|)) = r / 2
by XCMPLX_1:92;
(
(r / 2) + (r / 2) = r &
r / 2
>= 0 )
by A6, XREAL_1:136;
then
|.(Y9 - y9).| < r
by A21, A22, Lm2;
then
dist (
Y,
yy)
< r
by Th11;
hence
y in Ball (
Y,
r)
by METRIC_1:11;
verum
end;
Ball (
Y,
r)
c= G
by A4, A7;
hence
ex
H being
a_neighborhood of
W st
f .: H c= G
by A16, XBOOLE_1:1;
verum end;
hence
ex
H being
a_neighborhood of
W st
f .: H c= G
;
verum
end;
hence
f is continuous
by BORSUK_1:def 1; verum