reconsider Dx = diffX1_X2_1 as Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1 by TOPMETR:17;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st Dx . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dx .: W c= V )
proof
let p be
Point of
[:(TOP-REAL 2),(TOP-REAL 2):];
for V being Subset of R^1 st Dx . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dx .: W c= V )let V be
Subset of
R^1;
( Dx . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dx .: W c= V ) )
assume that A1:
Dx . p in V
and A2:
V is
open
;
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dx .: W c= V )
A3:
p = [(p `1),(p `2)]
by Lm5, MCART_1:21;
A4:
diffX1_X2_1 . p = ((p `1) `1) - ((p `2) `1)
by Def3;
set r =
((p `1) `1) - ((p `2) `1);
reconsider V1 =
V as
open Subset of
REAL by A2, BORSUK_5:39, TOPMETR:17;
consider g being
Real such that A5:
0 < g
and A6:
].((((p `1) `1) - ((p `2) `1)) - g),((((p `1) `1) - ((p `2) `1)) + g).[ c= V1
by A1, A4, RCOMP_1:19;
reconsider g =
g as
Element of
REAL by XREAL_0:def 1;
set W1 =
{ |[x,y]| where x, y is Real : ( ((p `1) `1) - (g / 2) < x & x < ((p `1) `1) + (g / 2) ) } ;
set W2 =
{ |[x,y]| where x, y is Real : ( ((p `2) `1) - (g / 2) < x & x < ((p `2) `1) + (g / 2) ) } ;
{ |[x,y]| where x, y is Real : ( ((p `1) `1) - (g / 2) < x & x < ((p `1) `1) + (g / 2) ) } c= the
carrier of
(TOP-REAL 2)
then reconsider W1 =
{ |[x,y]| where x, y is Real : ( ((p `1) `1) - (g / 2) < x & x < ((p `1) `1) + (g / 2) ) } as
Subset of
(TOP-REAL 2) ;
{ |[x,y]| where x, y is Real : ( ((p `2) `1) - (g / 2) < x & x < ((p `2) `1) + (g / 2) ) } c= the
carrier of
(TOP-REAL 2)
then reconsider W2 =
{ |[x,y]| where x, y is Real : ( ((p `2) `1) - (g / 2) < x & x < ((p `2) `1) + (g / 2) ) } as
Subset of
(TOP-REAL 2) ;
take
[:W1,W2:]
;
( p in [:W1,W2:] & [:W1,W2:] is open & Dx .: [:W1,W2:] c= V )
A7:
p `1 = |[((p `1) `1),((p `1) `2)]|
by EUCLID:53;
A8:
0 / 2
< g / 2
by A5, XREAL_1:74;
then A9:
((p `1) `1) - (g / 2) < ((p `1) `1) - 0
by XREAL_1:15;
((p `1) `1) + 0 < ((p `1) `1) + (g / 2)
by A8, XREAL_1:6;
then A10:
p `1 in W1
by A7, A9;
A11:
p `2 = |[((p `2) `1),((p `2) `2)]|
by EUCLID:53;
A12:
((p `2) `1) - (g / 2) < ((p `2) `1) - 0
by A8, XREAL_1:15;
((p `2) `1) + 0 < ((p `2) `1) + (g / 2)
by A8, XREAL_1:6;
then
p `2 in W2
by A11, A12;
hence
p in [:W1,W2:]
by A3, A10, ZFMISC_1:def 2;
( [:W1,W2:] is open & Dx .: [:W1,W2:] c= V )
A13:
W1 is
open
by PSCOMP_1:19;
W2 is
open
by PSCOMP_1:19;
hence
[:W1,W2:] is
open
by A13, BORSUK_1:6;
Dx .: [:W1,W2:] c= V
let b be
object ;
TARSKI:def 3 ( not b in Dx .: [:W1,W2:] or b in V )
assume
b in Dx .: [:W1,W2:]
;
b in V
then consider a being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] such that A14:
a in [:W1,W2:]
and A15:
Dx . a = b
by FUNCT_2:65;
A16:
a = [(a `1),(a `2)]
by Lm5, MCART_1:21;
A17:
diffX1_X2_1 . a = ((a `1) `1) - ((a `2) `1)
by Def3;
a `1 in W1
by A14, A16, ZFMISC_1:87;
then consider x1,
y1 being
Real such that A18:
a `1 = |[x1,y1]|
and A19:
((p `1) `1) - (g / 2) < x1
and A20:
x1 < ((p `1) `1) + (g / 2)
;
A21:
(a `1) `1 = x1
by A18, EUCLID:52;
A22:
(((p `1) `1) - (g / 2)) + (g / 2) < x1 + (g / 2)
by A19, XREAL_1:6;
A23:
((p `1) `1) - x1 > ((p `1) `1) - (((p `1) `1) + (g / 2))
by A20, XREAL_1:15;
A24:
((p `1) `1) - x1 < (x1 + (g / 2)) - x1
by A22, XREAL_1:9;
((p `1) `1) - x1 > - (g / 2)
by A23;
then A25:
|.(((p `1) `1) - x1).| < g / 2
by A24, SEQ_2:1;
a `2 in W2
by A14, A16, ZFMISC_1:87;
then consider x2,
y2 being
Real such that A26:
a `2 = |[x2,y2]|
and A27:
((p `2) `1) - (g / 2) < x2
and A28:
x2 < ((p `2) `1) + (g / 2)
;
A29:
(a `2) `1 = x2
by A26, EUCLID:52;
A30:
(((p `2) `1) - (g / 2)) + (g / 2) < x2 + (g / 2)
by A27, XREAL_1:6;
A31:
((p `2) `1) - x2 > ((p `2) `1) - (((p `2) `1) + (g / 2))
by A28, XREAL_1:15;
A32:
((p `2) `1) - x2 < (x2 + (g / 2)) - x2
by A30, XREAL_1:9;
((p `2) `1) - x2 > - (g / 2)
by A31;
then
|.(((p `2) `1) - x2).| < g / 2
by A32, SEQ_2:1;
then A33:
|.(((p `1) `1) - x1).| + |.(((p `2) `1) - x2).| < (g / 2) + (g / 2)
by A25, XREAL_1:8;
|.((((p `1) `1) - x1) - (((p `2) `1) - x2)).| <= |.(((p `1) `1) - x1).| + |.(((p `2) `1) - x2).|
by COMPLEX1:57;
then
|.(- ((((p `1) `1) - x1) - (((p `2) `1) - x2))).| <= |.(((p `1) `1) - x1).| + |.(((p `2) `1) - x2).|
by COMPLEX1:52;
then
|.((x1 - x2) - (((p `1) `1) - ((p `2) `1))).| < g
by A33, XXREAL_0:2;
then
((a `1) `1) - ((a `2) `1) in ].((((p `1) `1) - ((p `2) `1)) - g),((((p `1) `1) - ((p `2) `1)) + g).[
by A21, A29, RCOMP_1:1;
hence
b in V
by A6, A15, A17;
verum
end;
hence
diffX1_X2_1 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
by JGRAPH_2:10; verum