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 12;
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 A8:
h . p in Int V
by TOPS_1:23;
reconsider r =
h . p as
Point of
(Euclid n) by EUCLID:67;
consider r0 being
real number such that A9:
(
r0 > 0 &
Ball (
r,
r0)
c= V )
by A6, A8, GOBOARD6:5;
reconsider r01 =
f . p as
Point of
(Euclid n) by EUCLID:67;
reconsider G1 =
Ball (
r01,
(r0 / 2)) as
Subset of
(TOP-REAL n) by EUCLID:67;
A10:
f . p in G1
by A9, GOBOARD6:1;
A11:
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n)
by EUCLID:def 8;
G1 is
open
by A11, TOPMETR:14, TOPS_3:76;
then consider W1 being
Subset of
T such that A12:
(
p in W1 &
W1 is
open &
f .: W1 c= G1 )
by A10, JGRAPH_2:10;
reconsider r02 =
g . p as
Point of
(Euclid n) by EUCLID:67;
reconsider G2 =
Ball (
r02,
(r0 / 2)) as
Subset of
(TOP-REAL n) by EUCLID:67;
A13:
g . p in G2
by A9, GOBOARD6:1;
G2 is
open
by A11, TOPMETR:14, TOPS_3:76;
then consider W2 being
Subset of
T such that A14:
(
p in W2 &
W2 is
open &
g .: W2 c= G2 )
by A13, JGRAPH_2:10;
take W =
W1 /\ W2;
( p in W & W is open & h .: W c= V )
thus
p in W
by A12, A14, XBOOLE_0:def 4;
( W is open & h .: W c= V )
thus
W is
open
by A12, A14;
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 A15:
(
z in dom h &
z in W &
h . z = x )
by FUNCT_1:def 6;
A16:
z in W1
by A15, XBOOLE_0:def 4;
reconsider pz =
z as
Point of
T by A15;
dom f = the
carrier of
T
by FUNCT_2:def 1;
then A17:
f . pz in f .: W1
by A16, FUNCT_1:def 6;
reconsider bb1 =
f . pz as
Point of
(Euclid n) by EUCLID:67;
dist (
r01,
bb1)
< r0 / 2
by A12, A17, METRIC_1:11;
then A18:
|.((f . p) - (f . pz)).| < r0 / 2
by A6, JGRAPH_1:28;
A19:
z in W2
by A15, XBOOLE_0:def 4;
dom g = the
carrier of
T
by FUNCT_2:def 1;
then A20:
g . pz in g .: W2
by A19, FUNCT_1:def 6;
reconsider bb2 =
g . pz as
Point of
(Euclid n) by EUCLID:67;
dist (
r02,
bb2)
< r0 / 2
by A14, A20, METRIC_1:11;
then A21:
|.((g . p) - (g . pz)).| < r0 / 2
by A6, JGRAPH_1:28;
A22:
(f . pz) - (g . pz) = x
by A7, A15;
reconsider bb0 =
(f . pz) - (g . pz) as
Point of
(Euclid n) by EUCLID:67;
A23:
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:47
.=
(((f . p) - (f . pz)) - (g . p)) + (g . pz)
by A6, TOPREAL9:1
.=
(((f . p) - (f . pz)) + (g . pz)) + (- (g . p))
by EUCLID:26
.=
((f . p) - (f . pz)) + ((g . pz) - (g . p))
by EUCLID:26
;
then A24:
|.(((f . p) - (g . p)) - ((f . pz) - (g . pz))).| <= |.((f . p) - (f . pz)).| + |.((g . pz) - (g . p)).|
by A6, TOPRNS_1:29;
A25:
|.((g . p) - (g . pz)).| =
|.(- ((g . pz) - (g . p))).|
by EUCLID:44
.=
|.((g . pz) - (g . p)).|
by A6, TOPRNS_1:26
;
|.((f . p) - (f . pz)).| + |.((g . p) - (g . pz)).| < (r0 / 2) + (r0 / 2)
by A18, A21, XREAL_1:8;
then
|.(((f . p) - (g . p)) - ((f . pz) - (g . pz))).| < r0
by A24, A25, XXREAL_0:2;
then
|.((h . p) - (h . pz)).| < r0
by A7, A23;
then
dist (
r,
bb0)
< r0
by A6, A15, A22, JGRAPH_1:28;
then
x in Ball (
r,
r0)
by A22, METRIC_1:11;
hence
x in V
by A9;
verum
end;
hence
h is continuous
by JGRAPH_2:10; verum