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