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