let n be Nat; for f being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds f . q = |.q.| ) holds
f is continuous
let f be Function of (TOP-REAL n),R^1; ( ( for q being Point of (TOP-REAL n) holds f . q = |.q.| ) implies f is continuous )
A1:
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider f1 = f as Function of (TopSpaceMetr (Euclid n)),(TopSpaceMetr RealSpace) by TOPMETR:def 6;
assume A2:
for q being Point of (TOP-REAL n) holds f . q = |.q.|
; f is continuous
now for r being Real
for u being Element of (Euclid n)
for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being Real st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )let r be
Real;
for u being Element of (Euclid n)
for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being Real st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )let u be
Element of
(Euclid n);
for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being Real st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )let u1 be
Element of
RealSpace;
( r > 0 & u1 = f1 . u implies ex s being Real st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) )assume that A3:
r > 0
and A4:
u1 = f1 . u
;
ex s being Real st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )set s1 =
r;
for
w being
Element of
(Euclid n) for
w1 being
Element of
RealSpace st
w1 = f1 . w &
dist (
u,
w)
< r holds
dist (
u1,
w1)
< r
proof
let w be
Element of
(Euclid n);
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < r holds
dist (u1,w1) < rlet w1 be
Element of
RealSpace;
( w1 = f1 . w & dist (u,w) < r implies dist (u1,w1) < r )
assume that A5:
w1 = f1 . w
and A6:
dist (
u,
w)
< r
;
dist (u1,w1) < r
reconsider tu =
u1,
tw =
w1 as
Real ;
reconsider qw =
w,
qu =
u as
Point of
(TOP-REAL n) by TOPREAL3:8;
A7:
dist (
u1,
w1) =
the
distance of
RealSpace . (
u1,
w1)
.=
|.(tu - tw).|
by METRIC_1:def 12
;
A8:
tu = |.qu.|
by A2, A4;
w1 = |.qw.|
by A2, A5;
then
(
dist (
u,
w)
= |.(qu - qw).| &
dist (
u1,
w1)
<= |.(qu - qw).| )
by A7, A8, Th3, JGRAPH_1:28;
hence
dist (
u1,
w1)
< r
by A6, XXREAL_0:2;
verum
end; hence
ex
s being
Real st
(
s > 0 & ( for
w being
Element of
(Euclid n) for
w1 being
Element of
RealSpace st
w1 = f1 . w &
dist (
u,
w)
< s holds
dist (
u1,
w1)
< r ) )
by A3;
verum end;
then
f1 is continuous
by UNIFORM1:3;
hence
f is continuous
by A1, PRE_TOPC:32, TOPMETR:def 6; verum