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 = 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 = 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 = p /. i ) implies f is continuous )
assume that
A1: i in Seg n and
A2: for p being Element of (TOP-REAL n) holds f . p = p /. i ; :: thesis: f is continuous
reconsider f1 = f as Function of (TOP-REAL n),(TopSpaceMetr RealSpace) by TOPMETR:def 6;
for r being Real
for u being Element 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; :: thesis: for u being Element of RealSpace
for P being Subset of (TopSpaceMetr RealSpace) st r > 0 & P = Ball (u,r) holds
f1 " P is open
let u be Element of RealSpace; :: thesis: for P being Subset of (TopSpaceMetr RealSpace) st r > 0 & P = Ball (u,r) holds
f1 " P is open
let P be Subset of (TopSpaceMetr RealSpace); :: thesis: ( r > 0 & P = Ball (u,r) implies f1 " P is open )
assume that
r > 0 and
A3: P = Ball (u,r) ; :: thesis: f1 " P is open
reconsider u1 = u as Real ;
Ball (u,r) = { s where s is Real : ( u1 - r < s & s < u1 + r ) } by Th17;
then f " (Ball (u,r)) = { p where p is Element of (TOP-REAL n) : ( u1 - r < p /. i & p /. i < u1 + r ) } by A2, Th15;
hence f1 " P is open by A1, A3, Th14; :: thesis: verum
end;
hence f is continuous by Th16, TOPMETR:def 6; :: thesis: verum