let x, y be Real; for n being 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 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 X be 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 f1, f2, g be Function of X,(TOP-REAL n); ( 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))
; g is continuous
per cases
( ( x <> 0 & y <> 0 ) or x = 0 or y = 0 )
;
suppose that A4:
x <> 0
and A5:
y <> 0
;
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;
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);
( 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 ) )
reconsider r =
g . p as
Point of
(Euclid n) by TOPREAL3:8;
assume
(
g . p in V &
V is
open )
;
ex W being Subset of X st
( p in W & W is open & g .: W c= V )
then
g . p in Int V
by TOPS_1:23;
then consider r0 being
Real such that A6:
r0 > 0
and A7:
Ball (
r,
r0)
c= V
by GOBOARD6:5;
A8:
r0 / 2
> 0
by A6, XREAL_1:215;
reconsider r2 =
f2 . p as
Point of
(Euclid n) by TOPREAL3:8;
reconsider G2 =
Ball (
r2,
((r0 / 2) / |.y.|)) as
Subset of
(TOP-REAL n) by TOPREAL3:8;
A9:
G2 is
open
by GOBOARD6:3;
reconsider r1 =
f1 . p as
Point of
(Euclid n) by TOPREAL3:8;
reconsider G1 =
Ball (
r1,
((r0 / 2) / |.x.|)) as
Subset of
(TOP-REAL n) by TOPREAL3:8;
A10:
G1 is
open
by GOBOARD6:3;
A11:
|.y.| > 0
by A5, COMPLEX1:47;
then
r2 in G2
by A8, GOBOARD6:1, XREAL_1:139;
then consider W2 being
Subset of
X such that A12:
p in W2
and A13:
W2 is
open
and A14:
f2 .: W2 c= G2
by A2, A9, JGRAPH_2:10;
A15:
|.x.| > 0
by A4, COMPLEX1:47;
then
r1 in G1
by A8, GOBOARD6:1, XREAL_1:139;
then consider W1 being
Subset of
X such that A16:
p in W1
and A17:
W1 is
open
and A18:
f1 .: W1 c= G1
by A1, A10, JGRAPH_2:10;
take W =
W1 /\ W2;
( p in W & W is open & g .: W c= V )
thus
p in W
by A16, A12, XBOOLE_0:def 4;
( W is open & g .: W c= V )
thus
W is
open
by A17, A13;
g .: W c= V
g .: W c= Ball (
r,
r0)
proof
let a be
object ;
TARSKI:def 3 ( not a in g .: W or a in Ball (r,r0) )
assume
a in g .: W
;
a in Ball (r,r0)
then consider z being
object such that A19:
z in dom g
and A20:
z in W
and A21:
g . z = a
by FUNCT_1:def 6;
A22:
z in W1
by A20, XBOOLE_0:def 4;
reconsider z =
z as
Point of
X by A19;
reconsider ea2 =
f2 . z as
Point of
(Euclid n) by TOPREAL3:8;
reconsider ea1 =
f1 . z as
Point of
(Euclid n) by TOPREAL3:8;
A23:
z in the
carrier of
X
;
then A24:
z in dom f2
by FUNCT_2:def 1;
z in W2
by A20, XBOOLE_0:def 4;
then
f2 . z in f2 .: W2
by A24, FUNCT_1:def 6;
then A25:
dist (
r2,
ea2)
< (r0 / 2) / |.y.|
by A14, METRIC_1:11;
z in dom f1
by A23, FUNCT_2:def 1;
then
f1 . z in f1 .: W1
by A22, FUNCT_1:def 6;
then A26:
dist (
r1,
ea1)
< (r0 / 2) / |.x.|
by A18, METRIC_1:11;
A27:
a = (x * (f1 . z)) + (y * (f2 . z))
by A3, A21;
then reconsider e1x =
a as
Point of
(Euclid n) by TOPREAL3:8;
r = (x * (f1 . p)) + (y * (f2 . p))
by A3;
then
dist (
r,
e1x)
< (|.x.| * ((r0 / 2) / |.x.|)) + (|.y.| * ((r0 / 2) / |.y.|))
by A4, A5, A27, A26, A25, Th14;
then
dist (
r,
e1x)
< (|.x.| * ((r0 / |.x.|) / 2)) + (|.y.| * ((r0 / 2) / |.y.|))
by XCMPLX_1:48;
then
dist (
r,
e1x)
< (|.x.| * ((r0 / |.x.|) / 2)) + (|.y.| * ((r0 / |.y.|) / 2))
by XCMPLX_1:48;
then
dist (
r,
e1x)
< (r0 / 2) + (|.y.| * ((r0 / |.y.|) / 2))
by A15, XCMPLX_1:97;
then
dist (
r,
e1x)
< (r0 / 2) + (r0 / 2)
by A11, XCMPLX_1:97;
hence
a in Ball (
r,
r0)
by METRIC_1:11;
verum
end;
hence
g .: W c= V
by A7;
verum
end; hence
g is
continuous
by JGRAPH_2:10;
verum