set X = Niemytzki-plane ;
consider B being Neighborhood_System of Niemytzki-plane such that
A1:
for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 }
and
A2:
for x, y being Real st y > 0 holds
B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 }
by Def3;
reconsider uB = Union B as prebasis of Niemytzki-plane by YELLOW_9:27;
A3:
the carrier of Niemytzki-plane = y>=0-plane
by Def3;
now for x being Point of Niemytzki-plane
for V being Subset of Niemytzki-plane st x in V & V in uB holds
ex f being continuous Function of Niemytzki-plane,I[01] st
( f . x = 0 & f .: (V `) c= {1} )let x be
Point of
Niemytzki-plane;
for V being Subset of Niemytzki-plane st x in V & V in uB holds
ex f being continuous Function of Niemytzki-plane,I[01] st
( b4 . f = 0 & b4 .: (b3 `) c= {1} )let V be
Subset of
Niemytzki-plane;
( x in V & V in uB implies ex f being continuous Function of Niemytzki-plane,I[01] st
( b3 . f = 0 & b3 .: (b2 `) c= {1} ) )assume that A4:
x in V
and A5:
V in uB
;
ex f being continuous Function of Niemytzki-plane,I[01] st
( b3 . f = 0 & b3 .: (b2 `) c= {1} )
V is
open
by A5, TOPS_2:def 1;
then consider V9 being
Subset of
Niemytzki-plane such that A6:
V9 in B . x
and A7:
V9 c= V
by A4, YELLOW_8:def 1;
x in y>=0-plane
by A3;
then reconsider x9 =
x as
Point of
(TOP-REAL 2) ;
A8:
x = |[(x9 `1),(x9 `2)]|
by EUCLID:53;
per cases
( x9 `2 = 0 or x9 `2 > 0 )
by A3, A8, Th18;
suppose A9:
x9 `2 = 0
;
ex f being continuous Function of Niemytzki-plane,I[01] st
( b3 . f = 0 & b3 .: (b2 `) c= {1} )then
B . x = { ((Ball (|[(x9 `1),r]|,r)) \/ {|[(x9 `1),0]|}) where r is Real : r > 0 }
by A1, A8;
then consider r being
Real such that A10:
V9 = (Ball (|[(x9 `1),r]|,r)) \/ {|[(x9 `1),0]|}
and A11:
r > 0
by A6;
consider f being
continuous Function of
Niemytzki-plane,
I[01] such that A12:
f . |[(x9 `1),0]| = 0
and A13:
for
a,
b being
Real holds
( (
|[a,b]| in V9 ` implies
f . |[a,b]| = 1 ) & (
|[a,b]| in V9 \ {|[(x9 `1),0]|} implies
f . |[a,b]| = (|.(|[(x9 `1),0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) )
by A10, A11, Th76;
take f =
f;
( f . x = 0 & f .: (V `) c= {1} )thus
f . x = 0
by A9, A12, EUCLID:53;
f .: (V `) c= {1}thus
f .: (V `) c= {1}
verum end; suppose A17:
x9 `2 > 0
;
ex f being continuous Function of Niemytzki-plane,I[01] st
( b3 . f = 0 & b3 .: (b2 `) c= {1} )then
B . x = { ((Ball (|[(x9 `1),(x9 `2)]|,r)) /\ y>=0-plane) where r is Real : r > 0 }
by A2, A8;
then consider r being
Real such that A18:
V9 = (Ball (|[(x9 `1),(x9 `2)]|,r)) /\ y>=0-plane
and A19:
r > 0
by A6;
consider f being
continuous Function of
Niemytzki-plane,
I[01] such that A20:
f . |[(x9 `1),(x9 `2)]| = 0
and A21:
for
a,
b being
Real holds
( (
|[a,b]| in V9 ` implies
f . |[a,b]| = 1 ) & (
|[a,b]| in V9 implies
f . |[a,b]| = |.(|[(x9 `1),(x9 `2)]| - |[a,b]|).| / r ) )
by A17, A18, A19, Th81;
take f =
f;
( f . x = 0 & f .: (V `) c= {1} )thus
f . x = 0
by A20, EUCLID:53;
f .: (V `) c= {1}thus
f .: (V `) c= {1}
verum end; end; end;
hence
Niemytzki-plane is Tychonoff
by Th52, Th82; verum