let y be real number ; :: thesis: for n being Element of NAT
for X being non empty TopSpace
for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds
g is continuous
let n be Element of NAT ; :: thesis: for X being non empty TopSpace
for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds
g is continuous
let X be non empty TopSpace; :: thesis: for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds
g is continuous
let f, g be Function of X,(TOP-REAL n); :: thesis: ( f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) implies g is continuous )
assume that
A1:
f is continuous
and
A2:
for p being Point of X holds g . p = y * (f . p)
; :: 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 A3:
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 A4:
r0 > 0
and A5:
Ball r,
r0 c= V
by A3, GOBOARD6:8;
reconsider r1 =
f . p as
Point of
(Euclid n) by TOPREAL3:13;
reconsider G1 =
Ball r1,
(r0 / (abs y)) as
Subset of
(TOP-REAL n) by TOPREAL3:13;
per cases
( y <> 0 or y = 0 )
;
suppose A6:
y <> 0
;
:: thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )then A7:
0 < abs y
by COMPLEX1:133;
then A8:
r1 in G1
by A4, GOBOARD6:4, XREAL_1:141;
G1 is
open
by GOBOARD6:6;
then consider W1 being
Subset of
X such that A9:
p in W1
and A10:
W1 is
open
and A11:
f .: W1 c= G1
by A1, A8, JGRAPH_2:20;
take
W1
;
:: thesis: ( p in W1 & W1 is open & g .: W1 c= V )thus
p in W1
by A9;
:: thesis: ( W1 is open & g .: W1 c= V )thus
W1 is
open
by A10;
:: thesis: g .: W1 c= V
g .: W1 c= Ball r,
r0
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in g .: W1 or x in Ball r,r0 )
assume
x in g .: W1
;
:: thesis: x in Ball r,r0
then consider z being
set such that A12:
z in dom g
and A13:
z in W1
and A14:
g . z = x
by FUNCT_1:def 12;
reconsider z =
z as
Point of
X by A12;
z in the
carrier of
X
;
then
z in dom f
by FUNCT_2:def 1;
then A15:
f . z in f .: W1
by A13, FUNCT_1:def 12;
reconsider ea1 =
f . z as
Point of
(Euclid n) by TOPREAL3:13;
A16:
x = y * (f . z)
by A2, A14;
then reconsider e1x =
x as
Point of
(Euclid n) by TOPREAL3:13;
A17:
dist r1,
ea1 < r0 / (abs y)
by A11, A15, METRIC_1:12;
r = y * (f . p)
by A2;
then
dist r,
e1x < (abs y) * (r0 / (abs y))
by A6, A16, A17, Th13;
then
dist r,
e1x < r0
by A7, XCMPLX_1:88;
hence
x in Ball r,
r0
by METRIC_1:12;
:: thesis: verum
end; hence
g .: W1 c= V
by A5, XBOOLE_1:1;
:: thesis: verum end;
end;
hence
g is continuous
by JGRAPH_2:20; :: thesis: verum