let X be non empty TopSpace; for n being Nat
for p being Point of (TOP-REAL n)
for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )
let n be Nat; for p being Point of (TOP-REAL n)
for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )
let p be Point of (TOP-REAL n); for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )
let f be Function of X,R^1; ( f is continuous implies ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous ) )
assume A1:
f is continuous
; ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )
defpred S1[ set , set ] means $2 = (f . $1) * p;
A2:
for x being Element of X ex y being Element of (TOP-REAL n) st S1[x,y]
;
ex g being Function of the carrier of X, the carrier of (TOP-REAL n) st
for x being Element of X holds S1[x,g . x]
from FUNCT_2:sch 3(A2);
then consider g being Function of the carrier of X, the carrier of (TOP-REAL n) such that
A3:
for x being Element of X holds S1[x,g . x]
;
reconsider g = g as Function of X,(TOP-REAL n) ;
for r0 being Point of X
for V being Subset of (TOP-REAL n) st g . r0 in V & V is open holds
ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )
proof
let r0 be
Point of
X;
for V being Subset of (TOP-REAL n) st g . r0 in V & V is open holds
ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )let V be
Subset of
(TOP-REAL n);
( g . r0 in V & V is open implies ex W being Subset of X st
( r0 in W & W is open & g .: W c= V ) )
assume that A4:
g . r0 in V
and A5:
V is
open
;
ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )
A6:
g . r0 in Int V
by A4, A5, TOPS_1:23;
reconsider u =
g . r0 as
Point of
(Euclid n) by TOPREAL3:8;
consider s being
Real such that A7:
s > 0
and A8:
Ball (
u,
s)
c= V
by A6, GOBOARD6:5;
now ( ( p <> 0. (TOP-REAL n) & ex W being Subset of X st
( r0 in W & W is open & g .: W c= V ) ) or ( p = 0. (TOP-REAL n) & ex W being Subset of X st
( r0 in W & W is open & g .: W c= V ) ) )per cases
( p <> 0. (TOP-REAL n) or p = 0. (TOP-REAL n) )
;
case A9:
p <> 0. (TOP-REAL n)
;
ex W being Subset of X st
( r0 in W & W is open & g .: W c= V )then A10:
|.p.| <> 0
by TOPRNS_1:24;
set r2 =
s / |.p.|;
reconsider G1 =
].((f . r0) - (s / |.p.|)),((f . r0) + (s / |.p.|)).[ as
Subset of
R^1 by TOPMETR:17;
A11:
f . r0 < (f . r0) + (s / |.p.|)
by A7, A10, XREAL_1:29, XREAL_1:139;
then
(f . r0) - (s / |.p.|) < f . r0
by XREAL_1:19;
then A12:
f . r0 in G1
by A11, XXREAL_1:4;
G1 is
open
by JORDAN6:35;
then consider W2 being
Subset of
X such that A13:
r0 in W2
and A14:
W2 is
open
and A15:
f .: W2 c= G1
by A1, A12, JGRAPH_2:10;
g .: W2 c= V
proof
let y be
object ;
TARSKI:def 3 ( not y in g .: W2 or y in V )
assume
y in g .: W2
;
y in V
then consider r being
object such that A16:
r in dom g
and A17:
r in W2
and A18:
y = g . r
by FUNCT_1:def 6;
reconsider r =
r as
Point of
X by A16;
dom f = the
carrier of
X
by FUNCT_2:def 1;
then
f . r in f .: W2
by A17, FUNCT_1:def 6;
then A19:
|.((f . r) - (f . r0)).| < s / |.p.|
by A15, RCOMP_1:1;
reconsider t =
f . r,
t0 =
f . r0 as
Real ;
A20:
|.(t0 - t).| = |.(t - t0).|
by UNIFORM1:11;
reconsider v =
g . r as
Point of
(Euclid n) by TOPREAL3:8;
g . r0 = (f . r0) * p
by A3;
then A21:
|.((g . r0) - (g . r)).| =
|.(((f . r0) * p) - ((f . r) * p)).|
by A3
.=
|.(((f . r0) - (f . r)) * p).|
by RLVECT_1:35
.=
|.(t0 - t).| * |.p.|
by TOPRNS_1:7
;
|.((f . r) - (f . r0)).| * |.p.| < (s / |.p.|) * |.p.|
by A10, A19, XREAL_1:68;
then
|.((g . r0) - (g . r)).| < s
by A9, A20, A21, TOPRNS_1:24, XCMPLX_1:87;
then
dist (
u,
v)
< s
by JGRAPH_1:28;
then
g . r in Ball (
u,
s)
by METRIC_1:11;
hence
y in V
by A8, A18;
verum
end; hence
ex
W being
Subset of
X st
(
r0 in W &
W is
open &
g .: W c= V )
by A13, A14;
verum end; end; end;
hence
ex
W being
Subset of
X st
(
r0 in W &
W is
open &
g .: W c= V )
;
verum
end;
then
g 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 = (f . r) * p ) & g is continuous )
by A3; verum