let o be Point of (TOP-REAL 2); 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:17;
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):];
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;
( 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
;
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 Lm5, MCART_1:21;
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:39, TOPMETR:17;
consider g being
Real 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:19;
reconsider g =
g as
Element of
REAL by XREAL_0:def 1;
set W2 =
{ |[x,y]| where x, y is Real : ( ((p `2) `2) - g < y & y < ((p `2) `2) + g ) } ;
{ |[x,y]| where x, y is 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 Real : ( ((p `2) `2) - g < y & y < ((p `2) `2) + g ) } as
Subset of
(TOP-REAL 2) ;
take
[:([#] (TOP-REAL 2)),W2:]
;
( 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:53;
A8:
((p `2) `2) - g < ((p `2) `2) - 0
by A5, XREAL_1:15;
((p `2) `2) + 0 < ((p `2) `2) + g
by A5, XREAL_1:6;
then
p `2 in W2
by A7, A8;
hence
p in [:([#] (TOP-REAL 2)),W2:]
by A3, ZFMISC_1:def 2;
( [:([#] (TOP-REAL 2)),W2:] is open & Yo .: [:([#] (TOP-REAL 2)),W2:] c= V )
W2 is
open
by PSCOMP_1:21;
hence
[:([#] (TOP-REAL 2)),W2:] is
open
by BORSUK_1:6;
Yo .: [:([#] (TOP-REAL 2)),W2:] c= V
let b be
object ;
TARSKI:def 3 ( not b in Yo .: [:([#] (TOP-REAL 2)),W2:] or b in V )
assume
b in Yo .: [:([#] (TOP-REAL 2)),W2:]
;
b in V
then consider a being
Point of
[:(TOP-REAL 2),(TOP-REAL 2):] such that A9:
a in [:([#] (TOP-REAL 2)),W2:]
and A10:
Yo . a = b
by FUNCT_2:65;
A11:
a = [(a `1),(a `2)]
by Lm5, MCART_1:21;
A12:
(diffX2_2 o) . a = ((a `2) `2) - (o `2)
by Def2;
a `2 in W2
by A9, A11, ZFMISC_1:87;
then consider x2,
y2 being
Real such that A13:
a `2 = |[x2,y2]|
and A14:
((p `2) `2) - g < y2
and A15:
y2 < ((p `2) `2) + g
;
A16:
(a `2) `2 = y2
by A13, EUCLID:52;
then A17:
(((p `2) `2) - g) - (o `2) < ((a `2) `2) - (o `2)
by A14, XREAL_1:9;
((a `2) `2) - (o `2) < (((p `2) `2) + g) - (o `2)
by A15, A16, XREAL_1:9;
then
((a `2) `2) - (o `2) in ].((((p `2) `2) - (o `2)) - g),((((p `2) `2) - (o `2)) + g).[
by A17, XXREAL_1:4;
hence
b in V
by A6, A10, A12;
verum
end;
hence
diffX2_2 o is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
by JGRAPH_2:10; verum