let h be Function of T,(TOP-REAL n); ( h = f <--> g implies h is continuous )
assume A5:
h = f <--> g
; h is continuous
A6:
n in NAT
by ORDINAL1:def 13;
A7:
for r being Point of T holds h . r = (f . r) - (g . r)
for p being Point of T
for V being Subset of (TOP-REAL n) st h . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & h .: W c= V )
proof
let p be
Point of
T;
for V being Subset of (TOP-REAL n) st h . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & h .: W c= V )let V be
Subset of
(TOP-REAL n);
( h . p in V & V is open implies ex W being Subset of T st
( p in W & W is open & h .: W c= V ) )
assume
(
h . p in V &
V is
open )
;
ex W being Subset of T st
( p in W & W is open & h .: W c= V )
then A9:
h . p in Int V
by TOPS_1:55;
reconsider r =
h . p as
Point of
(Euclid n) by EUCLID:71;
consider r0 being
real number such that A10:
(
r0 > 0 &
Ball r,
r0 c= V )
by A6, A9, GOBOARD6:8;
reconsider r01 =
f . p as
Point of
(Euclid n) by EUCLID:71;
reconsider G1 =
Ball r01,
(r0 / 2) as
Subset of
(TOP-REAL n) by EUCLID:71;
A11:
f . p in G1
by A10, GOBOARD6:4;
A12:
TopStruct(# the
carrier of
(TOP-REAL n),the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n)
by EUCLID:def 8;
reconsider g1 =
G1 as
Subset of
(TopSpaceMetr (Euclid n)) ;
G1 is
open
by A12, TOPMETR:21, TOPS_3:76;
then consider W1 being
Subset of
T such that A13:
(
p in W1 &
W1 is
open &
f .: W1 c= G1 )
by A11, JGRAPH_2:20;
reconsider r02 =
g . p as
Point of
(Euclid n) by EUCLID:71;
reconsider G2 =
Ball r02,
(r0 / 2) as
Subset of
(TOP-REAL n) by EUCLID:71;
A14:
g . p in G2
by A10, GOBOARD6:4;
reconsider g2 =
G2 as
Subset of
(TopSpaceMetr (Euclid n)) ;
G2 is
open
by A12, TOPMETR:21, TOPS_3:76;
then consider W2 being
Subset of
T such that A15:
(
p in W2 &
W2 is
open &
g .: W2 c= G2 )
by A14, JGRAPH_2:20;
take W =
W1 /\ W2;
( p in W & W is open & h .: W c= V )
thus
p in W
by A13, A15, XBOOLE_0:def 4;
( W is open & h .: W c= V )
thus
W is
open
by A13, A15;
h .: W c= V
let x be
Element of
(TOP-REAL n);
LATTICE7:def 1 ( not x in h .: W or x in V )
assume
x in h .: W
;
x in V
then consider z being
set such that A16:
(
z in dom h &
z in W &
h . z = x )
by FUNCT_1:def 12;
A17:
z in W1
by A16, XBOOLE_0:def 4;
reconsider pz =
z as
Point of
T by A16;
dom f = the
carrier of
T
by FUNCT_2:def 1;
then A18:
f . pz in f .: W1
by A17, FUNCT_1:def 12;
reconsider bb1 =
f . pz as
Point of
(Euclid n) by EUCLID:71;
dist r01,
bb1 < r0 / 2
by A13, A18, METRIC_1:12;
then A19:
|.((f . p) - (f . pz)).| < r0 / 2
by A6, JGRAPH_1:45;
A20:
z in W2
by A16, XBOOLE_0:def 4;
dom g = the
carrier of
T
by FUNCT_2:def 1;
then A21:
g . pz in g .: W2
by A20, FUNCT_1:def 12;
reconsider bb2 =
g . pz as
Point of
(Euclid n) by EUCLID:71;
dist r02,
bb2 < r0 / 2
by A15, A21, METRIC_1:12;
then A22:
|.((g . p) - (g . pz)).| < r0 / 2
by A6, JGRAPH_1:45;
A23:
(f . pz) - (g . pz) = x
by A7, A16;
reconsider bb0 =
(f . pz) - (g . pz) as
Point of
(Euclid n) by EUCLID:71;
A24:
h . pz = (f . pz) - (g . pz)
by A7;
((f . p) - (g . p)) - ((f . pz) - (g . pz)) =
(((f . p) - (g . p)) - (f . pz)) + (g . pz)
by EUCLID:51
.=
(((f . p) - (f . pz)) - (g . p)) + (g . pz)
by A6, TOPREAL9:1
.=
(((f . p) - (f . pz)) + (g . pz)) + (- (g . p))
by EUCLID:30
.=
((f . p) - (f . pz)) + ((g . pz) - (g . p))
by EUCLID:30
;
then A25:
|.(((f . p) - (g . p)) - ((f . pz) - (g . pz))).| <= |.((f . p) - (f . pz)).| + |.((g . pz) - (g . p)).|
by A6, TOPRNS_1:30;
A26:
|.((g . p) - (g . pz)).| =
|.(- ((g . pz) - (g . p))).|
by EUCLID:48
.=
|.((g . pz) - (g . p)).|
by A6, TOPRNS_1:27
;
|.((f . p) - (f . pz)).| + |.((g . p) - (g . pz)).| < (r0 / 2) + (r0 / 2)
by A19, A22, XREAL_1:10;
then
|.(((f . p) - (g . p)) - ((f . pz) - (g . pz))).| < r0
by A25, A26, XXREAL_0:2;
then
|.((h . p) - (h . pz)).| < r0
by A7, A24;
then
dist r,
bb0 < r0
by A6, A16, A23, JGRAPH_1:45;
then
x in Ball r,
r0
by A23, METRIC_1:12;
hence
x in V
by A10;
verum
end;
hence
h is continuous
by JGRAPH_2:20; verum