let n be Element of NAT ; :: thesis: for f being Function of (TOP-REAL n),R^1
for i being Element of NAT st i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = Proj p,i ) holds
f is continuous
let f be Function of (TOP-REAL n),R^1 ; :: thesis: for i being Element of NAT st i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = Proj p,i ) holds
f is continuous
let i be Element of NAT ; :: thesis: ( i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = Proj p,i ) implies f is continuous )
assume A1:
( i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = Proj p,i ) )
; :: thesis: f is continuous
reconsider f1 = f as Function of (TOP-REAL n),(TopSpaceMetr RealSpace ) by TOPMETR:def 7;
for r being real number
for u being Element of the carrier of RealSpace
for P being Subset of (TopSpaceMetr RealSpace ) st r > 0 & P = Ball u,r holds
f1 " P is open
proof
let r be
real number ;
:: thesis: for u being Element of the carrier of RealSpace
for P being Subset of (TopSpaceMetr RealSpace ) st r > 0 & P = Ball u,r holds
f1 " P is openlet u be
Element of the
carrier of
RealSpace ;
:: thesis: for P being Subset of (TopSpaceMetr RealSpace ) st r > 0 & P = Ball u,r holds
f1 " P is openlet P be
Subset of
(TopSpaceMetr RealSpace );
:: thesis: ( r > 0 & P = Ball u,r implies f1 " P is open )
assume A2:
(
r > 0 &
P = Ball u,
r )
;
:: thesis: f1 " P is open
reconsider u1 =
u as
Real by METRIC_1:def 14;
Ball u,
r = { s where s is Real : ( u1 - r < s & s < u1 + r ) }
by A2, Th21;
then
f " (Ball u,r) = { p where p is Element of (TOP-REAL n) : ( u1 - r < Proj p,i & Proj p,i < u1 + r ) }
by A1, Th19;
hence
f1 " P is
open
by A1, A2, Th18;
:: thesis: verum
end;
hence
f is continuous
by Th20, TOPMETR:def 7; :: thesis: verum