let p be Point of Niemytzki-plane ; :: thesis: for r being real positive number ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )
let r be real positive number ; :: thesis: ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )
consider BB being Neighborhood_System of Niemytzki-plane such that
A1:
for x being Element of REAL holds BB . |[x,0 ]| = { ((Ball |[x,q]|,q) \/ {|[x,0 ]|}) where q is Element of REAL : q > 0 }
and
A2:
for x, y being Element of REAL st y > 0 holds
BB . |[x,y]| = { ((Ball |[x,y]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 }
by Def3;
A3:
the carrier of Niemytzki-plane = y>=0-plane
by Def3;
p in the carrier of Niemytzki-plane
;
then reconsider p' = p as Point of (TOP-REAL 2) by A3;
A4:
p = |[(p' `1 ),(p' `2 )]|
by EUCLID:57;
per cases
( p' `2 = 0 or p' `2 > 0 )
by A3, A4, Th22;
suppose A5:
p' `2 = 0
;
:: thesis: ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )then
(
BB . p = { ((Ball |[(p' `1 ),q]|,q) \/ {|[(p' `1 ),0 ]|}) where q is Element of REAL : q > 0 } &
r / 2 is
Real )
by A1, A4;
then
(
(Ball |[(p' `1 ),(r / 2)]|,(r / 2)) \/ {|[(p' `1 ),0 ]|} in BB . p &
BB . p c= the
topology of
Niemytzki-plane )
by YELLOW_8:def 2;
then reconsider U =
(Ball |[(p' `1 ),(r / 2)]|,(r / 2)) \/ {p} as
open Subset of
Niemytzki-plane by A4, A5, PRE_TOPC:def 5;
take a =
|[(p' `1 ),(r / 2)]|;
:: thesis: ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )take
U
;
:: thesis: ( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )
(
p' - a = |[((p' `1 ) - (p' `1 )),(0 - (r / 2))]| &
0 - (r / 2) is
Real )
by A4, A5, EUCLID:66;
then A6:
|.(p' - a).| =
|.(0 - (r / 2)).|
by TOPREAL6:31
.=
|.((r / 2) - 0 ).|
by COMPLEX1:146
.=
r / 2
by ABSVALUE:def 1
;
thus
p in U
by SETWISEO:6;
:: thesis: ( a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )
a in Ball a,
(r / 2)
by Th17;
hence
a in U
by XBOOLE_0:def 3;
:: thesis: for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < rlet b be
Point of
(TOP-REAL 2);
:: thesis: ( b in U implies |.(b - a).| < r )assume
b in U
;
:: thesis: |.(b - a).| < rthen
(
b in Ball a,
(r / 2) or
b = p )
by SETWISEO:6;
then
(
|.(b - a).| <= r / 2 &
r / 2
< (r / 2) + (r / 2) )
by A6, TOPREAL9:7, XREAL_1:31;
hence
|.(b - a).| < r
by XXREAL_0:2;
:: thesis: verum end; suppose A7:
p' `2 > 0
;
:: thesis: ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )then
(
BB . p = { ((Ball |[(p' `1 ),(p' `2 )]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 } &
r / 2 is
Real )
by A2, A4;
then
(
(Ball p',(r / 2)) /\ y>=0-plane in BB . p &
BB . p c= the
topology of
Niemytzki-plane )
by A4, YELLOW_8:def 2;
then reconsider U =
(Ball p',(r / 2)) /\ y>=0-plane as
open Subset of
Niemytzki-plane by PRE_TOPC:def 5;
take a =
p';
:: thesis: ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )take
U
;
:: thesis: ( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )
(
p in Ball a,
(r / 2) &
p in y>=0-plane )
by A4, A7, Th17;
hence
(
p in U &
a in U )
by XBOOLE_0:def 4;
:: thesis: for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < rlet b be
Point of
(TOP-REAL 2);
:: thesis: ( b in U implies |.(b - a).| < r )assume
b in U
;
:: thesis: |.(b - a).| < rthen
b in Ball a,
(r / 2)
by XBOOLE_0:def 4;
then
(
|.(b - a).| <= r / 2 &
r / 2
< (r / 2) + (r / 2) )
by TOPREAL9:7, XREAL_1:31;
hence
|.(b - a).| < r
by XXREAL_0:2;
:: thesis: verum end;