let o be Point of (TOP-REAL 2); :: thesis: diffX2_1 o is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
reconsider Xo = diffX2_1 o 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 Xo . 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 & Xo .: W c= V )
proof
let p be
Point of
[:(TOP-REAL 2),(TOP-REAL 2):];
:: thesis: for V being Subset of R^1 st Xo . 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 & Xo .: W c= V )let V be
Subset of
R^1 ;
:: thesis: ( Xo . 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 & Xo .: W c= V ) )
assume that A1:
Xo . 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 & Xo .: W c= V )
A3:
Xo . p = ((p `2 ) `1 ) - (o `1 )
by Def1;
set r =
((p `2 ) `1 ) - (o `1 );
reconsider V1 =
V as
open Subset of
REAL by A2, BORSUK_5:62, TOPMETR:24;
consider g being
real number such that A4:
0 < g
and A5:
].((((p `2 ) `1 ) - (o `1 )) - g),((((p `2 ) `1 ) - (o `1 )) + g).[ c= V1
by A1, A3, RCOMP_1:40;
reconsider g =
g as
Element of
REAL by XREAL_0:def 1;
set W2 =
{ |[x,y]| where x, y is Element of REAL : ( ((p `2 ) `1 ) - g < x & x < ((p `2 ) `1 ) + g ) } ;
{ |[x,y]| where x, y is Element of REAL : ( ((p `2 ) `1 ) - g < x & x < ((p `2 ) `1 ) + g ) } c= the
carrier of
(TOP-REAL 2)
then reconsider W2 =
{ |[x,y]| where x, y is Element of REAL : ( ((p `2 ) `1 ) - g < x & x < ((p `2 ) `1 ) + g ) } as
Subset of
(TOP-REAL 2) ;
take
[:([#] (TOP-REAL 2)),W2:]
;
:: thesis: ( p in [:([#] (TOP-REAL 2)),W2:] & [:([#] (TOP-REAL 2)),W2:] is open & Xo .: [:([#] (TOP-REAL 2)),W2:] c= V )
A6:
p `2 = |[((p `2 ) `1 ),((p `2 ) `2 )]|
by EUCLID:57;
A7:
p = [(p `1 ),(p `2 )]
by Lm7, MCART_1:23;
(
((p `2 ) `1 ) - g < ((p `2 ) `1 ) - 0 &
((p `2 ) `1 ) + 0 < ((p `2 ) `1 ) + g )
by A4, XREAL_1:8, XREAL_1:17;
then
p `2 in W2
by A6;
hence
p in [:([#] (TOP-REAL 2)),W2:]
by A7, ZFMISC_1:def 2;
:: thesis: ( [:([#] (TOP-REAL 2)),W2:] is open & Xo .: [:([#] (TOP-REAL 2)),W2:] c= V )
W2 is
open
by PSCOMP_1:66;
hence
[:([#] (TOP-REAL 2)),W2:] is
open
by BORSUK_1:46;
:: thesis: Xo .: [:([#] (TOP-REAL 2)),W2:] c= V
let b be
set ;
:: according to TARSKI:def 3 :: thesis: ( not b in Xo .: [:([#] (TOP-REAL 2)),W2:] or b in V )
assume
b in Xo .: [:([#] (TOP-REAL 2)),W2:]
;
:: thesis: b in V
then consider a being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] such that A8:
a in [:([#] (TOP-REAL 2)),W2:]
and A9:
Xo . a = b
by FUNCT_2:116;
A10:
a = [(a `1 ),(a `2 )]
by Lm7, MCART_1:23;
A11:
(diffX2_1 o) . a = ((a `2 ) `1 ) - (o `1 )
by Def1;
a `2 in W2
by A8, A10, ZFMISC_1:106;
then consider x2,
y2 being
Element of
REAL such that A12:
a `2 = |[x2,y2]|
and A13:
(
((p `2 ) `1 ) - g < x2 &
x2 < ((p `2 ) `1 ) + g )
;
(a `2 ) `1 = x2
by A12, EUCLID:56;
then
(
(((p `2 ) `1 ) - g) - (o `1 ) < ((a `2 ) `1 ) - (o `1 ) &
((a `2 ) `1 ) - (o `1 ) < (((p `2 ) `1 ) + g) - (o `1 ) )
by A13, XREAL_1:11;
then
((a `2 ) `1 ) - (o `1 ) in ].((((p `2 ) `1 ) - (o `1 )) - g),((((p `2 ) `1 ) - (o `1 )) + g).[
by XXREAL_1:4;
hence
b in V
by A5, A9, A11;
:: thesis: verum
end;
hence
diffX2_1 o is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
by JGRAPH_2:20; :: thesis: verum