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 }
by A1, A4;
then A6:
(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 A6, 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 ) )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 ) )A7:
r / 2
< (r / 2) + (r / 2)
by XREAL_1:31;
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 A8:
(
b in Ball a,
(r / 2) or
b = p )
by SETWISEO:6;
p' - a = |[((p' `1 ) - (p' `1 )),(0 - (r / 2))]|
by A4, A5, EUCLID:66;
then |.(p' - a).| =
|.(0 - (r / 2)).|
by TOPREAL6:31
.=
|.((r / 2) - 0 ).|
by COMPLEX1:146
.=
r / 2
by ABSVALUE:def 1
;
then
|.(b - a).| <= r / 2
by A8, TOPREAL9:7;
hence
|.(b - a).| < r
by A7, XXREAL_0:2;
:: thesis: verum end; suppose A9:
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 }
by A2, A4;
then A10:
(Ball p',(r / 2)) /\ y>=0-plane in BB . p
by A4;
BB . p c= the
topology of
Niemytzki-plane
by YELLOW_8:def 2;
then reconsider U =
(Ball p',(r / 2)) /\ y>=0-plane as
open Subset of
Niemytzki-plane by A10, 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 ) )A11:
p in Ball a,
(r / 2)
by Th17;
p in y>=0-plane
by A4, A9;
hence
(
p in U &
a in U )
by A11, 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 A12:
|.(b - a).| <= r / 2
by TOPREAL9:7;
r / 2
< (r / 2) + (r / 2)
by XREAL_1:31;
hence
|.(b - a).| < r
by A12, XXREAL_0:2;
:: thesis: verum end;