reconsider n = n as Element of NAT by ORDINAL1:def 12;
set g = incl (f,n);
per cases
( n = 0 or n > 0 )
;
suppose A2:
n > 0
;
incl (f,n) is continuous
for
p being
Point of
T for
V being
Subset of
(TOP-REAL n) st
(incl (f,n)) . p in V &
V is
open holds
ex
W being
Subset of
T st
(
p in W &
W is
open &
(incl (f,n)) .: W c= V )
proof
let p be
Point of
T;
for V being Subset of (TOP-REAL n) st (incl (f,n)) . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & (incl (f,n)) .: W c= V )let V be
Subset of
(TOP-REAL n);
( (incl (f,n)) . p in V & V is open implies ex W being Subset of T st
( p in W & W is open & (incl (f,n)) .: W c= V ) )
assume that A3:
(incl (f,n)) . p in V
and A4:
V is
open
;
ex W being Subset of T st
( p in W & W is open & (incl (f,n)) .: W c= V )
A5:
(incl (f,n)) . p in Int V
by A3, A4, TOPS_1:23;
reconsider s =
(incl (f,n)) . p as
Point of
(Euclid n) by EUCLID:67;
consider r being
Real such that A6:
r > 0
and A7:
Ball (
s,
r)
c= V
by A5, GOBOARD6:5;
reconsider G =
n |-> (f . p) as
FinSequence of
REAL ;
1
<= n
by A2, NAT_1:14;
then A8:
n in Seg n
;
reconsider F =
(incl (f,n)) . p as
FinSequence of
REAL by EUCLID:24;
A9:
F = n |-> (f . p)
by Def4;
A10:
dom (n |-> (f . p)) = Seg n
;
A11:
((incl (f,n)) . p) /. n =
G /. n
by Def4
.=
G . n
by A8, A10, PARTFUN1:def 6
.=
f . p
by A8, FINSEQ_2:57
;
set R =
r / (sqrt n);
set RR =
R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[;
f . p in R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[
by A2, A11, A6, TOPREAL6:15;
then consider W being
Subset of
T such that A12:
(
p in W &
W is
open )
and A13:
f .: W c= R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[
by JGRAPH_2:10;
take
W
;
( p in W & W is open & (incl (f,n)) .: W c= V )
thus
(
p in W &
W is
open )
by A12;
(incl (f,n)) .: W c= V
let y be
Element of
(TOP-REAL n);
LATTICE7:def 1 ( not y in (incl (f,n)) .: W or y in V )
assume
y in (incl (f,n)) .: W
;
y in V
then consider x being
Element of
T such that A14:
x in W
and A15:
(incl (f,n)) . x = y
by FUNCT_2:65;
reconsider y1 =
y as
Point of
(Euclid n) by EUCLID:67;
reconsider y2 =
y1,
s2 =
s as
Element of
REAL n ;
A16:
y2 = n |-> (f . x)
by A15, Def4;
A17:
(Pitag_dist n) . (
y1,
s) =
|.(y2 - s2).|
by EUCLID:def 6
.=
(sqrt n) * |.((f . x) - (f . p)).|
by A16, A9, Th11
;
f . x in f .: W
by A14, FUNCT_2:35;
then
|.((f . x) - (f . p)).| < r / (sqrt n)
by A13, A11, RCOMP_1:1;
then
dist (
y1,
s)
< r
by A2, A17, XREAL_1:79;
then
y in Ball (
s,
r)
by METRIC_1:11;
hence
y in V
by A7;
verum
end; hence
incl (
f,
n) is
continuous
by JGRAPH_2:10;
verum