let X be non empty TopSpace; for n being Nat
for g1, g2 being Function of X,(TOP-REAL n) st g1 is continuous & g2 is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous )
let n be Nat; for g1, g2 being Function of X,(TOP-REAL n) st g1 is continuous & g2 is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous )
let g1, g2 be Function of X,(TOP-REAL n); ( g1 is continuous & g2 is continuous implies ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous ) )
assume that
A1:
g1 is continuous
and
A2:
g2 is continuous
; ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous )
defpred S1[ set , set ] means for r1, r2 being Element of (TOP-REAL n) st g1 . $1 = r1 & g2 . $1 = r2 holds
$2 = r1 + r2;
A3:
for x being Element of X ex y being Element of (TOP-REAL n) st S1[x,y]
ex f being Function of the carrier of X, the carrier of (TOP-REAL n) st
for x being Element of X holds S1[x,f . x]
from FUNCT_2:sch 3(A3);
then consider f being Function of the carrier of X, the carrier of (TOP-REAL n) such that
A4:
for x being Element of X
for r1, r2 being Element of (TOP-REAL n) st g1 . x = r1 & g2 . x = r2 holds
f . x = r1 + r2
;
reconsider g0 = f as Function of X,(TOP-REAL n) ;
A5:
for r being Point of X holds g0 . r = (g1 . r) + (g2 . r)
by A4;
for p being Point of X
for V being Subset of (TOP-REAL n) st g0 . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
proof
let p be
Point of
X;
for V being Subset of (TOP-REAL n) st g0 . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )let V be
Subset of
(TOP-REAL n);
( g0 . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) )
assume that A6:
g0 . p in V
and A7:
V is
open
;
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
A8:
g0 . p in Int V
by A6, A7, TOPS_1:23;
reconsider r =
g0 . p as
Point of
(Euclid n) by TOPREAL3:8;
consider r0 being
Real such that A9:
r0 > 0
and A10:
Ball (
r,
r0)
c= V
by A8, GOBOARD6:5;
reconsider r01 =
g1 . p as
Point of
(Euclid n) by TOPREAL3:8;
reconsider G1 =
Ball (
r01,
(r0 / 2)) as
Subset of
(TOP-REAL n) by TOPREAL3:8;
reconsider r02 =
g2 . p as
Point of
(Euclid n) by TOPREAL3:8;
reconsider G2 =
Ball (
r02,
(r0 / 2)) as
Subset of
(TOP-REAL n) by TOPREAL3:8;
A11:
g1 . p in G1
by A9, GOBOARD6:1, XREAL_1:215;
A12:
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider GG1 =
G1,
GG2 =
G2 as
Subset of
(TopSpaceMetr (Euclid n)) ;
GG1 is
open
by TOPMETR:14;
then
G1 is
open
by A12, PRE_TOPC:30;
then consider W1 being
Subset of
X such that A13:
p in W1
and A14:
W1 is
open
and A15:
g1 .: W1 c= G1
by A1, A11, JGRAPH_2:10;
A16:
g2 . p in G2
by A9, GOBOARD6:1, XREAL_1:215;
GG2 is
open
by TOPMETR:14;
then
G2 is
open
by A12, PRE_TOPC:30;
then consider W2 being
Subset of
X such that A17:
p in W2
and A18:
W2 is
open
and A19:
g2 .: W2 c= G2
by A2, A16, JGRAPH_2:10;
set W =
W1 /\ W2;
A20:
p in W1 /\ W2
by A13, A17, XBOOLE_0:def 4;
g0 .: (W1 /\ W2) c= Ball (
r,
r0)
proof
let x be
object ;
TARSKI:def 3 ( not x in g0 .: (W1 /\ W2) or x in Ball (r,r0) )
assume
x in g0 .: (W1 /\ W2)
;
x in Ball (r,r0)
then consider z being
object such that A21:
z in dom g0
and A22:
z in W1 /\ W2
and A23:
g0 . z = x
by FUNCT_1:def 6;
A24:
z in W1
by A22, XBOOLE_0:def 4;
reconsider pz =
z as
Point of
X by A21;
dom g1 = the
carrier of
X
by FUNCT_2:def 1;
then A25:
g1 . pz in g1 .: W1
by A24, FUNCT_1:def 6;
reconsider aa1 =
g1 . pz as
Point of
(TOP-REAL n) ;
reconsider bb1 =
aa1 as
Point of
(Euclid n) by TOPREAL3:8;
dist (
r01,
bb1)
< r0 / 2
by A15, A25, METRIC_1:11;
then A26:
|.((g1 . p) - (g1 . pz)).| < r0 / 2
by JGRAPH_1:28;
A27:
z in W2
by A22, XBOOLE_0:def 4;
dom g2 = the
carrier of
X
by FUNCT_2:def 1;
then A28:
g2 . pz in g2 .: W2
by A27, FUNCT_1:def 6;
reconsider aa2 =
g2 . pz as
Point of
(TOP-REAL n) ;
reconsider bb2 =
aa2 as
Point of
(Euclid n) by TOPREAL3:8;
dist (
r02,
bb2)
< r0 / 2
by A19, A28, METRIC_1:11;
then A29:
|.((g2 . p) - (g2 . pz)).| < r0 / 2
by JGRAPH_1:28;
A30:
aa1 + aa2 = x
by A4, A23;
reconsider bb0 =
aa1 + aa2 as
Point of
(Euclid n) by TOPREAL3:8;
A31:
g0 . pz = (g1 . pz) + (g2 . pz)
by A4;
((g1 . p) + (g2 . p)) - ((g1 . pz) + (g2 . pz)) =
(((g1 . p) + (g2 . p)) - (g1 . pz)) - (g2 . pz)
by RLVECT_1:27
.=
(((g1 . p) + (g2 . p)) + (- (g1 . pz))) - (g2 . pz)
.=
(((g1 . p) + (g2 . p)) + (- (g1 . pz))) + (- (g2 . pz))
.=
(((g1 . p) + (- (g1 . pz))) + (g2 . p)) + (- (g2 . pz))
by RLVECT_1:def 3
.=
((g1 . p) + (- (g1 . pz))) + ((g2 . p) + (- (g2 . pz)))
by RLVECT_1:def 3
.=
((g1 . p) - (g1 . pz)) + ((g2 . p) + (- (g2 . pz)))
.=
((g1 . p) - (g1 . pz)) + ((g2 . p) - (g2 . pz))
;
then A32:
|.(((g1 . p) + (g2 . p)) - ((g1 . pz) + (g2 . pz))).| <= |.((g1 . p) - (g1 . pz)).| + |.((g2 . p) - (g2 . pz)).|
by TOPRNS_1:29;
|.((g1 . p) - (g1 . pz)).| + |.((g2 . p) - (g2 . pz)).| < (r0 / 2) + (r0 / 2)
by A26, A29, XREAL_1:8;
then
|.(((g1 . p) + (g2 . p)) - ((g1 . pz) + (g2 . pz))).| < r0
by A32, XXREAL_0:2;
then
|.((g0 . p) - (g0 . pz)).| < r0
by A4, A31;
then
dist (
r,
bb0)
< r0
by A23, A30, JGRAPH_1:28;
hence
x in Ball (
r,
r0)
by A30, METRIC_1:11;
verum
end;
hence
ex
W being
Subset of
X st
(
p in W &
W is
open &
g0 .: W c= V )
by A10, A14, A18, A20, XBOOLE_1:1;
verum
end;
then
g0 is continuous
by JGRAPH_2:10;
hence
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous )
by A5; verum