let n be Nat; for X being non empty SubSpace 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 a being Point of X
for b being Point of (TOP-REAL n)
for r being Real st a = b & f . a = r holds
g . b = r * b ) & g is continuous )
let X be non empty SubSpace 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 a being Point of X
for b being Point of (TOP-REAL n)
for r being Real st a = b & f . a = r holds
g . b = r * b ) & 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 a being Point of X
for b being Point of (TOP-REAL n)
for r being Real st a = b & f . a = r holds
g . b = r * b ) & g is continuous ) )
assume A1:
f is continuous
; ex g being Function of X,(TOP-REAL n) st
( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being Real st a = b & f . a = r holds
g . b = r * b ) & g is continuous )
defpred S1[ set , set ] means for b being Point of (TOP-REAL n)
for r being Real st $1 = b & f . $1 = r holds
$2 = r * b;
A2:
for x being Element of X ex y being Point 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 X,(TOP-REAL n) such that
A3:
for x being Element of X
for b being Point of (TOP-REAL n)
for r being Real st x = b & f . x = r holds
g . x = r * b
;
take
g
; ( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being Real st a = b & f . a = r holds
g . b = r * b ) & 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 n1 =
n as
Element of
NAT by ORDINAL1:def 12;
reconsider gp =
g . p as
Point of
(Euclid n) by TOPREAL3:8;
[#] X c= [#] (TOP-REAL n)
by PRE_TOPC:def 4;
then reconsider pp =
p as
Point of
(TOP-REAL n1) ;
reconsider fp =
f . p as
Real ;
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 A4:
r0 > 0
and A5:
Ball (
gp,
r0)
c= V
by GOBOARD6:5;
per cases
( fp = 0 or fp <> 0 )
;
suppose A6:
fp = 0
;
ex W being Subset of X st
( p in W & W is open & g .: W c= V )reconsider W2 =
(Ball (pp,(r0 / 2))) /\ ([#] X) as
Subset of
X ;
Ball (
pp,
(r0 / 2))
in the
topology of
(TOP-REAL n1)
by PRE_TOPC:def 2;
then
W2 in the
topology of
X
by PRE_TOPC:def 4;
then A7:
W2 is
open
by PRE_TOPC:def 2;
p in Ball (
pp,
(r0 / 2))
by A4, JORDAN:16;
then A8:
p in W2
by XBOOLE_0:def 4;
set WW2 =
{ |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ;
A9:
|.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 }
by A8;
for
x being
object st
x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds
x is
real
then reconsider WW2 =
{ |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } as non
empty real-membered set by A9, MEMBERED:def 3;
for
x being
ExtReal st
x in WW2 holds
x <= |.pp.| + (r0 / 2)
then
|.pp.| + (r0 / 2) is
UpperBound of
WW2
by XXREAL_2:def 1;
then
WW2 is
bounded_above
by XXREAL_2:def 10;
then reconsider m =
sup WW2 as
Real ;
A13:
m >= 0
per cases
( m = 0 or m > 0 )
by A13;
suppose A16:
m = 0
;
ex W being Subset of X st
( p in W & W is open & g .: W c= V )set G1 =
REAL ;
REAL in the
topology of
R^1
by PRE_TOPC:def 1, TOPMETR:17;
then reconsider G1 =
REAL as
open Subset of
R^1 by PRE_TOPC:def 2;
fp in G1
by XREAL_0:def 1;
then consider W1 being
Subset of
X such that A17:
p in W1
and A18:
W1 is
open
and
f .: W1 c= G1
by A1, JGRAPH_2:10;
reconsider W3 =
W1 /\ W2 as
Subset of
X ;
take
W3
;
( p in W3 & W3 is open & g .: W3 c= V )thus
p in W3
by A17, A8, XBOOLE_0:def 4;
( W3 is open & g .: W3 c= V )thus
W3 is
open
by A18, A7;
g .: W3 c= V
g .: W3 c= Ball (
gp,
r0)
proof
let x be
object ;
TARSKI:def 3 ( not x in g .: W3 or x in Ball (gp,r0) )
assume
x in g .: W3
;
x in Ball (gp,r0)
then consider q being
object such that A19:
q in dom g
and A20:
q in W3
and A21:
g . q = x
by FUNCT_1:def 6;
reconsider q =
q as
Point of
X by A19;
[#] X c= [#] (TOP-REAL n)
by PRE_TOPC:def 4;
then reconsider qq =
q as
Point of
(TOP-REAL n1) ;
reconsider fq =
f . q as
Real ;
A22:
x = fq * qq
by A3, A21;
then reconsider gq =
x as
Point of
(Euclid n) by TOPREAL3:8;
reconsider gpp =
gp as
Point of
(TOP-REAL n1) ;
reconsider gqq =
gq as
Point of
(TOP-REAL n1) by A22;
A23:
gpp = fp * pp
by A3;
reconsider r2 =
fq - fp as
Real ;
A24:
|.(fq - fp).| * |.qq.| =
|.r2.| * |.qq.|
.=
|.((fq - fp) * qq).|
by TOPRNS_1:7
;
qq in W2
by A20, XBOOLE_0:def 4;
then
|.qq.| in WW2
;
then A25:
|.qq.| <= m
by XXREAL_2:4;
A26:
gpp = 0. (TOP-REAL n1)
by A23, A6, RLVECT_1:10;
|.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).|
by EUCLID_2:52;
then
|.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).|
by A26, JGRAPH_5:10;
then
|.(gqq + (- gpp)).| <= |.gqq.| + 0
by EUCLID_2:39;
then
|.(gqq - gpp).| < r0
by A3, A21, A6, A25, A24, A4, A16;
then
gqq in Ball (
gpp,
r0)
;
hence
x in Ball (
gp,
r0)
by TOPREAL9:13;
verum
end; hence
g .: W3 c= V
by A5;
verum end; suppose A27:
m > 0
;
ex W being Subset of X st
( p in W & W is open & g .: W c= V )set G1 =
].(fp - (r0 / m)),(fp + (r0 / m)).[;
reconsider G1 =
].(fp - (r0 / m)),(fp + (r0 / m)).[ as
open Subset of
R^1 by JORDAN6:35, TOPMETR:17, XXREAL_1:225;
A28:
0 + fp < (r0 / m) + fp
by A27, A4, XREAL_1:6;
(- (r0 / m)) + fp < 0 + fp
by A27, A4, XREAL_1:6;
then consider W1 being
Subset of
X such that A29:
p in W1
and A30:
W1 is
open
and A31:
f .: W1 c= G1
by A1, JGRAPH_2:10, A28, XXREAL_1:4;
reconsider W3 =
W1 /\ W2 as
Subset of
X ;
take
W3
;
( p in W3 & W3 is open & g .: W3 c= V )thus
p in W3
by A29, A8, XBOOLE_0:def 4;
( W3 is open & g .: W3 c= V )thus
W3 is
open
by A30, A7;
g .: W3 c= V
g .: W3 c= Ball (
gp,
r0)
proof
let x be
object ;
TARSKI:def 3 ( not x in g .: W3 or x in Ball (gp,r0) )
assume
x in g .: W3
;
x in Ball (gp,r0)
then consider q being
object such that A32:
q in dom g
and A33:
q in W3
and A34:
g . q = x
by FUNCT_1:def 6;
reconsider q =
q as
Point of
X by A32;
A35:
q in the
carrier of
X
;
[#] X c= [#] (TOP-REAL n)
by PRE_TOPC:def 4;
then reconsider qq =
q as
Point of
(TOP-REAL n1) ;
reconsider fq =
f . q as
Real ;
A36:
x = fq * qq
by A3, A34;
then reconsider gq =
x as
Point of
(Euclid n) by TOPREAL3:8;
reconsider gpp =
gp as
Point of
(TOP-REAL n1) ;
reconsider gqq =
gq as
Point of
(TOP-REAL n1) by A36;
A37:
gpp = fp * pp
by A3;
reconsider r2 =
fq as
Real ;
A38:
|.fq.| * |.qq.| =
|.r2.| * |.qq.|
.=
|.(fq * qq).|
by TOPRNS_1:7
;
A39:
q in dom f
by A35, FUNCT_2:def 1;
q in W1
by A33, XBOOLE_0:def 4;
then
f . q in f .: W1
by A39, FUNCT_1:def 6;
then
|.(fq - fp).| < r0 / m
by A31, RCOMP_1:1;
then
|.fq.| * m < (r0 / m) * m
by A6, A27, XREAL_1:68;
then
|.fq.| * m < r0 / (m / m)
by XCMPLX_1:82;
then A40:
|.fq.| * m < r0 / 1
by A27, XCMPLX_1:60;
qq in W2
by A33, XBOOLE_0:def 4;
then
|.qq.| in WW2
;
then
|.qq.| <= m
by XXREAL_2:4;
then A41:
|.qq.| * |.fq.| <= m * |.fq.|
by XREAL_1:64;
A42:
gpp = 0. (TOP-REAL n1)
by A37, A6, RLVECT_1:10;
A43:
|.gqq.| < r0
by A36, A41, A38, A40, XXREAL_0:2;
|.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).|
by EUCLID_2:52;
then
|.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).|
by A42, JGRAPH_5:10;
then
|.(gqq + (- gpp)).| <= |.gqq.| + 0
by EUCLID_2:39;
then
|.(gqq - gpp).| < r0
by A43, XXREAL_0:2;
then
gqq in Ball (
gpp,
r0)
;
hence
x in Ball (
gp,
r0)
by TOPREAL9:13;
verum
end; hence
g .: W3 c= V
by A5;
verum end; end; suppose A44:
fp <> 0
;
ex W being Subset of X st
( p in W & W is open & g .: W c= V )reconsider W2 =
(Ball (pp,((r0 / 2) / |.fp.|))) /\ ([#] X) as
Subset of
X ;
Ball (
pp,
((r0 / 2) / |.fp.|))
in the
topology of
(TOP-REAL n1)
by PRE_TOPC:def 2;
then
W2 in the
topology of
X
by PRE_TOPC:def 4;
then A45:
W2 is
open
by PRE_TOPC:def 2;
p in Ball (
pp,
((r0 / 2) / |.fp.|))
by A44, A4, JORDAN:16;
then A46:
p in W2
by XBOOLE_0:def 4;
set WW2 =
{ |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ;
A47:
|.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 }
by A46;
for
x being
object st
x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds
x is
real
then reconsider WW2 =
{ |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } as non
empty real-membered set by A47, MEMBERED:def 3;
for
x being
ExtReal st
x in WW2 holds
x <= |.pp.| + ((r0 / 2) / |.fp.|)
then
|.pp.| + ((r0 / 2) / |.fp.|) is
UpperBound of
WW2
by XXREAL_2:def 1;
then
WW2 is
bounded_above
by XXREAL_2:def 10;
then reconsider m =
sup WW2 as
Real ;
A51:
m >= 0
per cases
( m = 0 or m > 0 )
by A51;
suppose A54:
m = 0
;
ex W being Subset of X st
( p in W & W is open & g .: W c= V )set G1 =
REAL ;
REAL in the
topology of
R^1
by PRE_TOPC:def 1, TOPMETR:17;
then reconsider G1 =
REAL as
open Subset of
R^1 by PRE_TOPC:def 2;
fp in G1
by XREAL_0:def 1;
then consider W1 being
Subset of
X such that A55:
p in W1
and A56:
W1 is
open
and
f .: W1 c= G1
by A1, JGRAPH_2:10;
reconsider W3 =
W1 /\ W2 as
Subset of
X ;
take
W3
;
( p in W3 & W3 is open & g .: W3 c= V )thus
p in W3
by A55, A46, XBOOLE_0:def 4;
( W3 is open & g .: W3 c= V )thus
W3 is
open
by A56, A45;
g .: W3 c= V
g .: W3 c= Ball (
gp,
r0)
proof
let x be
object ;
TARSKI:def 3 ( not x in g .: W3 or x in Ball (gp,r0) )
assume
x in g .: W3
;
x in Ball (gp,r0)
then consider q being
object such that A57:
q in dom g
and A58:
q in W3
and A59:
g . q = x
by FUNCT_1:def 6;
reconsider q =
q as
Point of
X by A57;
[#] X c= [#] (TOP-REAL n)
by PRE_TOPC:def 4;
then reconsider qq =
q as
Point of
(TOP-REAL n1) ;
reconsider fq =
f . q as
Real ;
A60:
x = fq * qq
by A3, A59;
then reconsider gq =
x as
Point of
(Euclid n) by TOPREAL3:8;
reconsider gpp =
gp as
Point of
(TOP-REAL n1) ;
reconsider gqq =
gq as
Point of
(TOP-REAL n1) by A60;
A61:
gpp = fp * pp
by A3;
reconsider r2 =
fq - fp as
Real ;
reconsider r3 =
fp as
Real ;
A62:
|.(fq - fp).| * |.qq.| =
|.r2.| * |.qq.|
.=
|.((fq - fp) * qq).|
by TOPRNS_1:7
;
qq in W2
by A58, XBOOLE_0:def 4;
then
|.qq.| in WW2
;
then A63:
|.qq.| <= m
by XXREAL_2:4;
A64:
|.fp.| * |.(qq - pp).| =
|.r3.| * |.(qq - pp).|
.=
|.(fp * (qq - pp)).|
by TOPRNS_1:7
;
qq in W2
by A58, XBOOLE_0:def 4;
then
qq in Ball (
pp,
((r0 / 2) / |.fp.|))
by XBOOLE_0:def 4;
then
|.fp.| * |.(qq - pp).| < |.fp.| * ((r0 / 2) / |.fp.|)
by A44, XREAL_1:68, TOPREAL9:7;
then
|.fp.| * |.(qq - pp).| < (r0 / 2) / (|.fp.| / |.fp.|)
by XCMPLX_1:81;
then A65:
|.fp.| * |.(qq - pp).| < (r0 / 2) / 1
by A44, XCMPLX_1:60;
A66:
|.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2)
by A63, A65, A64, A62, A54, XREAL_1:8;
|.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).|
by EUCLID_2:52;
then A67:
|.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0
by A66, XXREAL_0:2;
((fq - fp) * qq) + (fp * (qq - pp)) =
((fq * qq) - (fp * qq)) + (fp * (qq - pp))
by RLVECT_1:35
.=
((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp))
by RLVECT_1:34
.=
(((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp)
by RLVECT_1:def 3
.=
(fq * qq) - (fp * pp)
by RLVECT_4:1
;
then
gqq in Ball (
gpp,
r0)
by A60, A67, A61;
hence
x in Ball (
gp,
r0)
by TOPREAL9:13;
verum
end; hence
g .: W3 c= V
by A5;
verum end; suppose A68:
m > 0
;
ex W being Subset of X st
( p in W & W is open & g .: W c= V )set G1 =
].(fp - ((r0 / 2) / m)),(fp + ((r0 / 2) / m)).[;
reconsider G1 =
].(fp - ((r0 / 2) / m)),(fp + ((r0 / 2) / m)).[ as
open Subset of
R^1 by JORDAN6:35, TOPMETR:17, XXREAL_1:225;
A69:
0 + fp < ((r0 / 2) / m) + fp
by A68, A4, XREAL_1:6;
(- ((r0 / 2) / m)) + fp < 0 + fp
by A68, A4, XREAL_1:6;
then consider W1 being
Subset of
X such that A70:
p in W1
and A71:
W1 is
open
and A72:
f .: W1 c= G1
by A1, JGRAPH_2:10, A69, XXREAL_1:4;
reconsider W3 =
W1 /\ W2 as
Subset of
X ;
take
W3
;
( p in W3 & W3 is open & g .: W3 c= V )thus
p in W3
by A70, A46, XBOOLE_0:def 4;
( W3 is open & g .: W3 c= V )thus
W3 is
open
by A71, A45;
g .: W3 c= V
g .: W3 c= Ball (
gp,
r0)
proof
let x be
object ;
TARSKI:def 3 ( not x in g .: W3 or x in Ball (gp,r0) )
assume
x in g .: W3
;
x in Ball (gp,r0)
then consider q being
object such that A73:
q in dom g
and A74:
q in W3
and A75:
g . q = x
by FUNCT_1:def 6;
reconsider q =
q as
Point of
X by A73;
A76:
q in the
carrier of
X
;
[#] X c= [#] (TOP-REAL n)
by PRE_TOPC:def 4;
then reconsider qq =
q as
Point of
(TOP-REAL n1) ;
reconsider fq =
f . q as
Real ;
A77:
x = fq * qq
by A3, A75;
then reconsider gq =
x as
Point of
(Euclid n) by TOPREAL3:8;
reconsider gpp =
gp as
Point of
(TOP-REAL n1) ;
reconsider gqq =
gq as
Point of
(TOP-REAL n1) by A77;
A78:
gpp = fp * pp
by A3;
reconsider r2 =
fq - fp as
Real ;
reconsider r3 =
fp as
Real ;
A79:
|.(fq - fp).| * |.qq.| =
|.r2.| * |.qq.|
.=
|.((fq - fp) * qq).|
by TOPRNS_1:7
;
A80:
q in dom f
by A76, FUNCT_2:def 1;
q in W1
by A74, XBOOLE_0:def 4;
then
f . q in f .: W1
by A80, FUNCT_1:def 6;
then
|.(fq - fp).| * m < ((r0 / 2) / m) * m
by A68, XREAL_1:68, A72, RCOMP_1:1;
then
|.(fq - fp).| * m < (r0 / 2) / (m / m)
by XCMPLX_1:82;
then A81:
|.(fq - fp).| * m < (r0 / 2) / 1
by A68, XCMPLX_1:60;
qq in W2
by A74, XBOOLE_0:def 4;
then
|.qq.| in WW2
;
then
|.qq.| <= m
by XXREAL_2:4;
then
|.qq.| * |.(fq - fp).| <= m * |.(fq - fp).|
by XREAL_1:64;
then A82:
|.((fq - fp) * qq).| < r0 / 2
by A79, A81, XXREAL_0:2;
A83:
|.fp.| * |.(qq - pp).| =
|.r3.| * |.(qq - pp).|
.=
|.(fp * (qq - pp)).|
by TOPRNS_1:7
;
qq in W2
by A74, XBOOLE_0:def 4;
then
qq in Ball (
pp,
((r0 / 2) / |.fp.|))
by XBOOLE_0:def 4;
then
|.fp.| * |.(qq - pp).| < |.fp.| * ((r0 / 2) / |.fp.|)
by A44, XREAL_1:68, TOPREAL9:7;
then
|.fp.| * |.(qq - pp).| < (r0 / 2) / (|.fp.| / |.fp.|)
by XCMPLX_1:81;
then A84:
|.fp.| * |.(qq - pp).| < (r0 / 2) / 1
by A44, XCMPLX_1:60;
A85:
|.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2)
by A82, A84, A83, XREAL_1:8;
|.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).|
by EUCLID_2:52;
then A86:
|.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0
by A85, XXREAL_0:2;
((fq - fp) * qq) + (fp * (qq - pp)) =
((fq * qq) - (fp * qq)) + (fp * (qq - pp))
by RLVECT_1:35
.=
((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp))
by RLVECT_1:34
.=
(((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp)
by RLVECT_1:def 3
.=
(fq * qq) - (fp * pp)
by RLVECT_4:1
;
then
gqq in Ball (
gpp,
r0)
by A77, A78, A86;
hence
x in Ball (
gp,
r0)
by TOPREAL9:13;
verum
end; hence
g .: W3 c= V
by A5;
verum end; end;
end;
hence
( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being Real st a = b & f . a = r holds
g . b = r * b ) & g is continuous )
by A3, JGRAPH_2:10; verum