reconsider Dy = diffX1_X2_2 as Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1 by TOPMETR:24;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st Dy . 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 & Dy .: W c= V )
proof
let p be
Point of
[:(TOP-REAL 2),(TOP-REAL 2):];
:: thesis: for V being Subset of R^1 st Dy . 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 & Dy .: W c= V )let V be
Subset of
R^1 ;
:: thesis: ( Dy . 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 & Dy .: W c= V ) )
assume that A1:
Dy . p in V
and A2:
V is
open
;
:: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dy .: W c= V )
A3:
p = [(p `1 ),(p `2 )]
by Lm7, MCART_1:23;
A4:
diffX1_X2_2 . p = ((p `1 ) `2 ) - ((p `2 ) `2 )
by Def4;
set r =
((p `1 ) `2 ) - ((p `2 ) `2 );
reconsider V1 =
V as
open Subset of
REAL by A2, BORSUK_5:62, TOPMETR:24;
consider g being
real number such that A5:
0 < g
and A6:
].((((p `1 ) `2 ) - ((p `2 ) `2 )) - g),((((p `1 ) `2 ) - ((p `2 ) `2 )) + g).[ c= V1
by A1, A4, RCOMP_1:40;
reconsider g =
g as
Element of
REAL by XREAL_0:def 1;
set W1 =
{ |[x,y]| where x, y is Element of REAL : ( ((p `1 ) `2 ) - (g / 2) < y & y < ((p `1 ) `2 ) + (g / 2) ) } ;
set W2 =
{ |[x,y]| where x, y is Element of REAL : ( ((p `2 ) `2 ) - (g / 2) < y & y < ((p `2 ) `2 ) + (g / 2) ) } ;
{ |[x,y]| where x, y is Element of REAL : ( ((p `1 ) `2 ) - (g / 2) < y & y < ((p `1 ) `2 ) + (g / 2) ) } c= the
carrier of
(TOP-REAL 2)
then reconsider W1 =
{ |[x,y]| where x, y is Element of REAL : ( ((p `1 ) `2 ) - (g / 2) < y & y < ((p `1 ) `2 ) + (g / 2) ) } as
Subset of
(TOP-REAL 2) ;
{ |[x,y]| where x, y is Element of REAL : ( ((p `2 ) `2 ) - (g / 2) < y & y < ((p `2 ) `2 ) + (g / 2) ) } c= the
carrier of
(TOP-REAL 2)
then reconsider W2 =
{ |[x,y]| where x, y is Element of REAL : ( ((p `2 ) `2 ) - (g / 2) < y & y < ((p `2 ) `2 ) + (g / 2) ) } as
Subset of
(TOP-REAL 2) ;
take
[:W1,W2:]
;
:: thesis: ( p in [:W1,W2:] & [:W1,W2:] is open & Dy .: [:W1,W2:] c= V )
A7:
p `1 = |[((p `1 ) `1 ),((p `1 ) `2 )]|
by EUCLID:57;
A8:
0 / 2
< g / 2
by A5, XREAL_1:76;
then
(
((p `1 ) `2 ) - (g / 2) < ((p `1 ) `2 ) - 0 &
((p `1 ) `2 ) + 0 < ((p `1 ) `2 ) + (g / 2) )
by XREAL_1:8, XREAL_1:17;
then A9:
p `1 in W1
by A7;
A10:
p `2 = |[((p `2 ) `1 ),((p `2 ) `2 )]|
by EUCLID:57;
(
((p `2 ) `2 ) - (g / 2) < ((p `2 ) `2 ) - 0 &
((p `2 ) `2 ) + 0 < ((p `2 ) `2 ) + (g / 2) )
by A8, XREAL_1:8, XREAL_1:17;
then
p `2 in W2
by A10;
hence
p in [:W1,W2:]
by A3, A9, ZFMISC_1:def 2;
:: thesis: ( [:W1,W2:] is open & Dy .: [:W1,W2:] c= V )
(
W1 is
open &
W2 is
open )
by PSCOMP_1:68;
hence
[:W1,W2:] is
open
by BORSUK_1:46;
:: thesis: Dy .: [:W1,W2:] c= V
let b be
set ;
:: according to TARSKI:def 3 :: thesis: ( not b in Dy .: [:W1,W2:] or b in V )
assume
b in Dy .: [:W1,W2:]
;
:: thesis: b in V
then consider a being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] such that A11:
a in [:W1,W2:]
and A12:
Dy . a = b
by FUNCT_2:116;
A13:
a = [(a `1 ),(a `2 )]
by Lm7, MCART_1:23;
A14:
diffX1_X2_2 . a = ((a `1 ) `2 ) - ((a `2 ) `2 )
by Def4;
a `1 in W1
by A11, A13, ZFMISC_1:106;
then consider x1,
y1 being
Element of
REAL such that A15:
a `1 = |[x1,y1]|
and A16:
((p `1 ) `2 ) - (g / 2) < y1
and A17:
y1 < ((p `1 ) `2 ) + (g / 2)
;
A18:
(a `1 ) `2 = y1
by A15, EUCLID:56;
(
(((p `1 ) `2 ) - (g / 2)) + (g / 2) < y1 + (g / 2) &
((p `1 ) `2 ) - y1 > ((p `1 ) `2 ) - (((p `1 ) `2 ) + (g / 2)) )
by A16, A17, XREAL_1:8, XREAL_1:17;
then
(
((p `1 ) `2 ) - y1 < (y1 + (g / 2)) - y1 &
((p `1 ) `2 ) - y1 > - (g / 2) )
by XREAL_1:11;
then A19:
abs (((p `1 ) `2 ) - y1) < g / 2
by SEQ_2:9;
a `2 in W2
by A11, A13, ZFMISC_1:106;
then consider x2,
y2 being
Element of
REAL such that A20:
a `2 = |[x2,y2]|
and A21:
((p `2 ) `2 ) - (g / 2) < y2
and A22:
y2 < ((p `2 ) `2 ) + (g / 2)
;
A23:
(a `2 ) `2 = y2
by A20, EUCLID:56;
(
(((p `2 ) `2 ) - (g / 2)) + (g / 2) < y2 + (g / 2) &
((p `2 ) `2 ) - y2 > ((p `2 ) `2 ) - (((p `2 ) `2 ) + (g / 2)) )
by A21, A22, XREAL_1:8, XREAL_1:17;
then
(
((p `2 ) `2 ) - y2 < (y2 + (g / 2)) - y2 &
((p `2 ) `2 ) - y2 > - (g / 2) )
by XREAL_1:11;
then
abs (((p `2 ) `2 ) - y2) < g / 2
by SEQ_2:9;
then A24:
(abs (((p `1 ) `2 ) - y1)) + (abs (((p `2 ) `2 ) - y2)) < (g / 2) + (g / 2)
by A19, XREAL_1:10;
abs ((((p `1 ) `2 ) - y1) - (((p `2 ) `2 ) - y2)) <= (abs (((p `1 ) `2 ) - y1)) + (abs (((p `2 ) `2 ) - y2))
by COMPLEX1:143;
then
abs (- ((((p `1 ) `2 ) - y1) - (((p `2 ) `2 ) - y2))) <= (abs (((p `1 ) `2 ) - y1)) + (abs (((p `2 ) `2 ) - y2))
by COMPLEX1:138;
then
abs ((y1 - y2) - (((p `1 ) `2 ) - ((p `2 ) `2 ))) < g
by A24, XXREAL_0:2;
then
((a `1 ) `2 ) - ((a `2 ) `2 ) in ].((((p `1 ) `2 ) - ((p `2 ) `2 )) - g),((((p `1 ) `2 ) - ((p `2 ) `2 )) + g).[
by A18, A23, RCOMP_1:8;
hence
b in V
by A6, A12, A14;
:: thesis: verum
end;
hence
diffX1_X2_2 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
by JGRAPH_2:20; :: thesis: verum