let T be non empty TopSpace; for M being non empty MetrSpace
for f being Function of (TopSpaceMetr M),T holds
( f is continuous iff for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V )
let M be non empty MetrSpace; for f being Function of (TopSpaceMetr M),T holds
( f is continuous iff for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V )
let f be Function of (TopSpaceMetr M),T; ( f is continuous iff for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V )
hereby ( ( for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V ) implies f is continuous )
assume A1:
f is
continuous
;
for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= Vlet p be
Point of
M;
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= Vlet V be
open Subset of
T;
( f . p in V implies ex s being positive Real st f .: (Ball (p,s)) c= V )assume
f . p in V
;
ex s being positive Real st f .: (Ball (p,s)) c= Vthen consider W being
Subset of
(TopSpaceMetr M) such that A2:
p in W
and A3:
W is
open
and A4:
f .: W c= V
by A1, JGRAPH_2:10;
Int W = W
by A3, TOPS_1:23;
then consider s being
Real such that A5:
s > 0
and A6:
Ball (
p,
s)
c= W
by A2, GOBOARD6:4;
reconsider s =
s as
positive Real by A5;
take s =
s;
f .: (Ball (p,s)) c= V
f .: (Ball (p,s)) c= f .: W
by A6, RELAT_1:123;
hence
f .: (Ball (p,s)) c= V
by A4;
verum
end;
assume A7:
for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: (Ball (p,s)) c= V
; f is continuous
for p being Point of (TopSpaceMetr M)
for V being Subset of T st f . p in V & V is open holds
ex W being Subset of (TopSpaceMetr M) st
( p in W & W is open & f .: W c= V )
hence
f is continuous
by JGRAPH_2:10; verum