let x, y be real number ; :: thesis: for n being Element of NAT
for X being non empty TopSpace
for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds
g is continuous
let n be Element of NAT ; :: thesis: for X being non empty TopSpace
for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds
g is continuous
let X be non empty TopSpace; :: thesis: for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds
g is continuous
let f1, f2, g be Function of X,(TOP-REAL n); :: thesis: ( f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) implies g is continuous )
assume that
A1:
f1 is continuous
and
A2:
f2 is continuous
and
A3:
for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p))
; :: thesis: g is continuous
per cases
( ( x <> 0 & y <> 0 ) or x = 0 or y = 0 )
;
suppose that A4:
x <> 0
and A5:
y <> 0
;
:: thesis: g is continuous
for
p being
Point of
X for
V being
Subset of
(TOP-REAL n) st
g . p in V &
V is
open holds
ex
W being
Subset of
X st
(
p in W &
W is
open &
g .: W c= V )
proof
let p be
Point of
X;
:: thesis: for V being Subset of (TOP-REAL n) st g . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g .: W c= V )let V be
Subset of
(TOP-REAL n);
:: thesis: ( g . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & g .: W c= V ) )
assume
(
g . p in V &
V is
open )
;
:: thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )
then A6:
g . p in Int V
by TOPS_1:55;
reconsider r =
g . p as
Point of
(Euclid n) by TOPREAL3:13;
consider r0 being
real number such that A7:
r0 > 0
and A8:
Ball r,
r0 c= V
by A6, GOBOARD6:8;
A9:
r0 / 2
> 0
by A7, XREAL_1:217;
reconsider r1 =
f1 . p as
Point of
(Euclid n) by TOPREAL3:13;
reconsider G1 =
Ball r1,
((r0 / 2) / (abs x)) as
Subset of
(TOP-REAL n) by TOPREAL3:13;
A10:
abs x > 0
by A4, COMPLEX1:133;
A11:
abs y > 0
by A5, COMPLEX1:133;
A12:
r1 in G1
by A9, A10, GOBOARD6:4, XREAL_1:141;
G1 is
open
by GOBOARD6:6;
then consider W1 being
Subset of
X such that A13:
p in W1
and A14:
W1 is
open
and A15:
f1 .: W1 c= G1
by A1, A12, JGRAPH_2:20;
reconsider r2 =
f2 . p as
Point of
(Euclid n) by TOPREAL3:13;
reconsider G2 =
Ball r2,
((r0 / 2) / (abs y)) as
Subset of
(TOP-REAL n) by TOPREAL3:13;
A16:
r2 in G2
by A9, A11, GOBOARD6:4, XREAL_1:141;
G2 is
open
by GOBOARD6:6;
then consider W2 being
Subset of
X such that A17:
p in W2
and A18:
W2 is
open
and A19:
f2 .: W2 c= G2
by A2, A16, JGRAPH_2:20;
take W =
W1 /\ W2;
:: thesis: ( p in W & W is open & g .: W c= V )
thus
p in W
by A13, A17, XBOOLE_0:def 4;
:: thesis: ( W is open & g .: W c= V )
thus
W is
open
by A14, A18, TOPS_1:38;
:: thesis: g .: W c= V
g .: W c= Ball r,
r0
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in g .: W or a in Ball r,r0 )
assume
a in g .: W
;
:: thesis: a in Ball r,r0
then consider z being
set such that A20:
z in dom g
and A21:
z in W
and A22:
g . z = a
by FUNCT_1:def 12;
A23:
z in W1
by A21, XBOOLE_0:def 4;
reconsider z =
z as
Point of
X by A20;
A24:
z in the
carrier of
X
;
then
z in dom f1
by FUNCT_2:def 1;
then A25:
f1 . z in f1 .: W1
by A23, FUNCT_1:def 12;
reconsider ea1 =
f1 . z as
Point of
(Euclid n) by TOPREAL3:13;
A26:
z in W2
by A21, XBOOLE_0:def 4;
z in dom f2
by A24, FUNCT_2:def 1;
then A27:
f2 . z in f2 .: W2
by A26, FUNCT_1:def 12;
reconsider ea2 =
f2 . z as
Point of
(Euclid n) by TOPREAL3:13;
A28:
a = (x * (f1 . z)) + (y * (f2 . z))
by A3, A22;
then reconsider e1x =
a as
Point of
(Euclid n) by TOPREAL3:13;
A29:
dist r1,
ea1 < (r0 / 2) / (abs x)
by A15, A25, METRIC_1:12;
A30:
dist r2,
ea2 < (r0 / 2) / (abs y)
by A19, A27, METRIC_1:12;
r = (x * (f1 . p)) + (y * (f2 . p))
by A3;
then
dist r,
e1x < ((abs x) * ((r0 / 2) / (abs x))) + ((abs y) * ((r0 / 2) / (abs y)))
by A4, A5, A28, A29, A30, Th14;
then
dist r,
e1x < ((abs x) * ((r0 / (abs x)) / 2)) + ((abs y) * ((r0 / 2) / (abs y)))
by XCMPLX_1:48;
then
dist r,
e1x < ((abs x) * ((r0 / (abs x)) / 2)) + ((abs y) * ((r0 / (abs y)) / 2))
by XCMPLX_1:48;
then
dist r,
e1x < (r0 / 2) + ((abs y) * ((r0 / (abs y)) / 2))
by A10, XCMPLX_1:98;
then
dist r,
e1x < (r0 / 2) + (r0 / 2)
by A11, XCMPLX_1:98;
hence
a in Ball r,
r0
by METRIC_1:12;
:: thesis: verum
end;
hence
g .: W c= V
by A8, XBOOLE_1:1;
:: thesis: verum
end; hence
g is
continuous
by JGRAPH_2:20;
:: thesis: verum