let T be non empty TopSpace; for F, G being RealMap of T st F is continuous & G is continuous holds
F + G is continuous
let F, G be RealMap of T; ( F is continuous & G is continuous implies F + G is continuous )
assume that
A1:
F is continuous
and
A2:
G is continuous
; F + G is continuous
reconsider F9 = F, G9 = G, FG9 = F + G as Function of T,R^1 by TOPMETR:17;
A3:
G9 is continuous
by A2, JORDAN5A:27;
A4:
F9 is continuous
by A1, JORDAN5A:27;
now for t being Point of T holds FG9 is_continuous_at tlet t be
Point of
T;
FG9 is_continuous_at t
for
R being
Subset of
R^1 st
R is
open &
FG9 . t in R holds
ex
H being
Subset of
T st
(
H is
open &
t in H &
FG9 .: H c= R )
proof
reconsider Ft =
F . t,
Gt =
G . t,
FGt =
(F + G) . t as
Point of
RealSpace by METRIC_1:def 13;
let R be
Subset of
R^1;
( R is open & FG9 . t in R implies ex H being Subset of T st
( H is open & t in H & FG9 .: H c= R ) )
assume
(
R is
open &
FG9 . t in R )
;
ex H being Subset of T st
( H is open & t in H & FG9 .: H c= R )
then consider r being
Real such that A5:
r > 0
and A6:
Ball (
FGt,
r)
c= R
by TOPMETR:15, TOPMETR:def 6;
reconsider r9 =
r as
Real ;
reconsider A =
Ball (
Ft,
(r9 / 2)),
B =
Ball (
Gt,
(r9 / 2)) as
Subset of
R^1 by METRIC_1:def 13, TOPMETR:17;
A7:
(
A is
open &
F9 is_continuous_at t )
by A4, TMAP_1:50, TOPMETR:14, TOPMETR:def 6;
F9 . t in A
by A5, Lm7, XREAL_1:139;
then consider AT being
Subset of
T such that A8:
AT is
open
and A9:
t in AT
and A10:
F9 .: AT c= A
by A7, TMAP_1:43;
A11:
(
B is
open &
G9 is_continuous_at t )
by A3, TMAP_1:50, TOPMETR:14, TOPMETR:def 6;
G . t in B
by A5, Lm7, XREAL_1:139;
then consider BT being
Subset of
T such that A12:
BT is
open
and A13:
t in BT
and A14:
G9 .: BT c= B
by A11, TMAP_1:43;
A15:
(F + G) .: (AT /\ BT) c= R
proof
let FGx be
object ;
TARSKI:def 3 ( not FGx in (F + G) .: (AT /\ BT) or FGx in R )
assume
FGx in (F + G) .: (AT /\ BT)
;
FGx in R
then consider x being
object such that A16:
x in dom (F + G)
and A17:
x in AT /\ BT
and A18:
FGx = (F + G) . x
by FUNCT_1:def 6;
reconsider x =
x as
Point of
T by A16;
reconsider Fx =
F . x,
Gx =
G . x,
FGx9 =
(F + G) . x as
Point of
RealSpace by METRIC_1:def 13;
(
dom G = the
carrier of
T &
x in BT )
by A17, FUNCT_2:def 1, XBOOLE_0:def 4;
then
G . x in G .: BT
by FUNCT_1:def 6;
then
dist (
Gx,
Gt)
< r9 / 2
by A14, METRIC_1:11;
then A19:
|.((G . x) - (G . t)).| < r9 / 2
by TOPMETR:11;
then A20:
- (r9 / 2) < (G . x) - (G . t)
by SEQ_2:1;
(
dom F = the
carrier of
T &
x in AT )
by A17, FUNCT_2:def 1, XBOOLE_0:def 4;
then
F . x in F .: AT
by FUNCT_1:def 6;
then
dist (
Fx,
Ft)
< r9 / 2
by A10, METRIC_1:11;
then A21:
|.((F . x) - (F . t)).| < r9 / 2
by TOPMETR:11;
then
- (r9 / 2) < (F . x) - (F . t)
by SEQ_2:1;
then
(- (r9 / 2)) + (- (r9 / 2)) < ((F . x) - (F . t)) + ((G . x) - (G . t))
by A20, XREAL_1:8;
then A22:
- r9 < ((F . x) + (G . x)) - ((F . t) + (G . t))
;
A23:
(G . x) - (G . t) < r9 / 2
by A19, SEQ_2:1;
(F . x) - (F . t) < r9 / 2
by A21, SEQ_2:1;
then
((F . x) - (F . t)) + ((G . x) - (G . t)) < (r9 / 2) + (r9 / 2)
by A23, XREAL_1:8;
then
|.(((F . x) + (G . x)) - ((F . t) + (G . t))).| < r9
by A22, SEQ_2:1;
then
|.(((F + G) . x) - ((F . t) + (G . t))).| < r9
by Def7;
then
|.(((F + G) . x) - ((F + G) . t)).| < r9
by Def7;
then
dist (
FGt,
FGx9)
< r9
by TOPMETR:11;
then
FGx9 in Ball (
FGt,
r)
by METRIC_1:11;
hence
FGx in R
by A6, A18;
verum
end;
t in AT /\ BT
by A9, A13, XBOOLE_0:def 4;
hence
ex
H being
Subset of
T st
(
H is
open &
t in H &
FG9 .: H c= R )
by A8, A12, A15;
verum
end; hence
FG9 is_continuous_at t
by TMAP_1:43;
verum end;
then
FG9 is continuous
by TMAP_1:50;
hence
F + G is continuous
by JORDAN5A:27; verum