let N, M be non empty MetrSpace; :: thesis: for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let f be Function of (TopSpaceMetr N),(TopSpaceMetr M); :: thesis: ( f is continuous implies for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) )
assume A1: f is continuous ; :: thesis: for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let r be Real; :: thesis: for u being Element of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let u be Element of N; :: thesis: for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let u1 be Element of M; :: thesis: ( r > 0 & u1 = f . u implies ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) )
reconsider P = Ball (u1,r) as Subset of (TopSpaceMetr M) by TOPMETR:12;
A2: ( the carrier of N = the carrier of (TopSpaceMetr N) & dom f = the carrier of (TopSpaceMetr N) ) by FUNCT_2:def 1, TOPMETR:12;
assume ( r > 0 & u1 = f . u ) ; :: thesis: ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
then f . u in P by GOBOARD6:1;
then A3: u in f " P by A2, FUNCT_1:def 7;
f " P is open by A1, Th2;
then consider s1 being Real such that
A4: s1 > 0 and
A5: Ball (u,s1) c= f " P by A3, TOPMETR:15;
reconsider s1 = s1 as Real ;
for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s1 holds
dist (u1,w1) < r
proof
let w be Element of N; :: thesis: for w1 being Element of M st w1 = f . w & dist (u,w) < s1 holds
dist (u1,w1) < r
let w1 be Element of M; :: thesis: ( w1 = f . w & dist (u,w) < s1 implies dist (u1,w1) < r )
assume that
A6: w1 = f . w and
A7: dist (u,w) < s1 ; :: thesis: dist (u1,w1) < r
w in Ball (u,s1) by A7, METRIC_1:11;
then f . w in P by A5, FUNCT_1:def 7;
hence dist (u1,w1) < r by A6, METRIC_1:11; :: thesis: verum
end;
hence ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) by A4; :: thesis: verum