let n be Element of NAT ; :: thesis: for f being Function of (TOP-REAL n),R^1 st f = n NormF holds
f is continuous
let f be Function of (TOP-REAL n),R^1 ; :: thesis: ( f = n NormF implies f is continuous )
assume A1:
f = n NormF
; :: thesis: f is continuous
for p being Point of (TOP-REAL n)
for V being Subset of R^1 st f . p in V & V is open holds
ex W being Subset of (TOP-REAL n) st
( p in W & W is open & f .: W c= V )
proof
let p be
Point of
(TOP-REAL n);
:: thesis: for V being Subset of R^1 st f . p in V & V is open holds
ex W being Subset of (TOP-REAL n) st
( p in W & W is open & f .: W c= V )let V be
Subset of
R^1 ;
:: thesis: ( f . p in V & V is open implies ex W being Subset of (TOP-REAL n) st
( p in W & W is open & f .: W c= V ) )
assume A2:
(
f . p in V &
V is
open )
;
:: thesis: ex W being Subset of (TOP-REAL n) st
( p in W & W is open & f .: W c= V )
reconsider v =
p as
Point of
(Euclid n) by EUCLID:71;
reconsider u =
f . p as
Point of
RealSpace by METRIC_1:def 14, TOPMETR:24;
reconsider u' =
f . p as
Real by TOPMETR:24;
A3:
f . p = |.p.|
by A1, Def1;
consider r being
real number such that A4:
(
r > 0 &
Ball u,
r c= V )
by A2, TOPMETR:22, TOPMETR:def 7;
reconsider r =
r as
Real by XREAL_0:def 1;
A5:
Ball v,
r = { q where q is Point of (TOP-REAL n) : |.(p - q).| < r }
by JGRAPH_2:10;
defpred S1[
Point of
(TOP-REAL n)]
means |.(p - $1).| < r;
TopStruct(# the
carrier of
(TOP-REAL n),the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider W1 =
Ball v,
r as
Subset of
(TOP-REAL n) ;
A6:
v in W1
by A4, GOBOARD6:4;
A7:
W1 is
open
by GOBOARD6:6;
f .: W1 c= Ball u,
r
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in f .: W1 or y in Ball u,r )
assume
y in f .: W1
;
:: thesis: y in Ball u,r
then consider x being
set such that A8:
(
x in dom f &
x in W1 &
y = f . x )
by FUNCT_1:def 12;
reconsider q =
x as
Point of
(TOP-REAL n) by A8;
consider q1 being
Point of
(TOP-REAL n) such that A9:
(
q = q1 &
|.(p - q1).| < r )
by A5, A8;
A10:
f . x = |.q.|
by A1, Def1;
A11:
Ball u,
r = ].(u' - r),(u' + r).[
by A4, FRECHET:7;
abs (|.p.| - |.q.|) <= |.(p - q).|
by JORDAN2C:11;
then
abs (u' - |.q.|) < r
by A3, A9, XXREAL_0:2;
then A12:
(
- r < u' - |.q.| &
u' - |.q.| < r )
by SEQ_2:9;
then A13:
u' - (u' - |.q.|) > u' - r
by XREAL_1:17;
u' > |.q.| + (- r)
by A12, XREAL_1:22;
then
u' - (- r) > (|.q.| + (- r)) - (- r)
by XREAL_1:11;
hence
y in Ball u,
r
by A8, A10, A11, A13, XXREAL_1:4;
:: thesis: verum
end;
hence
ex
W being
Subset of
(TOP-REAL n) st
(
p in W &
W is
open &
f .: W c= V )
by A4, A6, A7, XBOOLE_1:1;
:: thesis: verum
end;
hence
f is continuous
by JGRAPH_2:20; :: thesis: verum