let h be Function of T,(TOP-REAL n); :: thesis: ( h = f <--> g implies h is continuous )

assume A5: h = f <--> g ; :: thesis: h is continuous

A6: for r being Point of T holds h . r = (f . r) - (g . r)

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 )

assume A5: h = f <--> g ; :: thesis: h is continuous

A6: for r being Point of T holds h . r = (f . r) - (g . r)

proof

for p being Point of T
let r be Point of T; :: thesis: h . r = (f . r) - (g . r)

dom h = the carrier of T by FUNCT_2:def 1;

hence h . r = (f . r) - (g . r) by A5, VALUED_2:def 46; :: thesis: verum

end;dom h = the carrier of T by FUNCT_2:def 1;

hence h . r = (f . r) - (g . r) by A5, VALUED_2:def 46; :: thesis: verum

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

hence
h is continuous
by JGRAPH_2:10; :: thesis: verum
let p be Point of T; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( p in W & W is open & h .: W c= V )

thus p in W by A11, A13, XBOOLE_0:def 4; :: thesis: ( W is open & h .: W c= V )

thus W is open by A11, A13; :: thesis: h .: W c= V

let x be Element of (TOP-REAL n); :: according to LATTICE7:def 1 :: thesis: ( not x in h .: W or x in V )

assume x in h .: W ; :: thesis: 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; :: thesis: verum

end;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); :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( p in W & W is open & h .: W c= V )

thus p in W by A11, A13, XBOOLE_0:def 4; :: thesis: ( W is open & h .: W c= V )

thus W is open by A11, A13; :: thesis: h .: W c= V

let x be Element of (TOP-REAL n); :: according to LATTICE7:def 1 :: thesis: ( not x in h .: W or x in V )

assume x in h .: W ; :: thesis: 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; :: thesis: verum