let f be Function of (TopSpaceMetr M),(TopSpaceMetr M); :: thesis: ( f is isometric implies f is continuous )
assume f is isometric ; :: thesis: f is continuous
then consider g being isometric Function of M,M such that
A1: g = f ;
let W be Point of (TopSpaceMetr M); :: according to BORSUK_1:def 1 :: thesis: for b1 being a_neighborhood of f . W ex b2 being a_neighborhood of W st f .: b2 c= b1
let G be a_neighborhood of f . W; :: thesis: ex b1 being a_neighborhood of W st f .: b1 c= G
reconsider fw = f . W, w = W as Point of M ;
f . W in Int G by CONNSP_2:def 1;
then consider r being Real such that
A2: r > 0 and
A3: Ball (fw,r) c= G by GOBOARD6:4;
reconsider H = Ball (w,r) as a_neighborhood of W by A2, GOBOARD6:91;
take H ; :: thesis: f .: H c= G
thus f .: H c= G :: thesis: verum
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f .: H or a in G )
assume a in f .: H ; :: thesis: a in G
then consider b being object such that
A4: b in dom f and
A5: b in H and
A6: f . b = a by FUNCT_1:def 6;
reconsider b = b as Point of (TopSpaceMetr M) by A4;
reconsider b9 = b as Point of M ;
dist (b9,w) < r by A5, METRIC_1:11;
then dist ((g . b9),fw) < r by A1, VECTMETR:def 3;
then a in Ball (fw,r) by A1, A6, METRIC_1:11;
hence a in G by A3; :: thesis: verum
end;