set f = + (x,r);
consider BB being Neighborhood_System of Niemytzki-plane such that
A1:
for x being Real holds BB . |[x,0]| = { ((Ball (|[x,q]|,q)) \/ {|[x,0]|}) where q is Real : q > 0 }
and
A2:
for x, y being Real st y > 0 holds
BB . |[x,y]| = { ((Ball (|[x,y]|,q)) /\ y>=0-plane) where q is Real : q > 0 }
by Def3;
A3:
dom BB = y>=0-plane
by Lm1, PARTFUN1:def 2;
now for a, b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( (+ (x,r)) " [.0,b.[ is open & (+ (x,r)) " ].a,1.] is open )let a,
b be
Real;
( 0 <= a & a < 1 & 0 < b & b <= 1 implies ( (+ (x,r)) " [.0,b.[ is open & (+ (x,r)) " ].a,1.] is open ) )assume that A4:
0 <= a
and A5:
a < 1
and A6:
0 < b
and A7:
b <= 1
;
( (+ (x,r)) " [.0,b.[ is open & (+ (x,r)) " ].a,1.] is open )now for c being Element of Niemytzki-plane st c in (+ (x,r)) " [.0,b.[ holds
ex U being Subset of Niemytzki-plane st
( U in Union BB & c in U & U c= (+ (x,r)) " [.0,b.[ )let c be
Element of
Niemytzki-plane;
( c in (+ (x,r)) " [.0,b.[ implies ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " [.0,b.[ ) )assume
c in (+ (x,r)) " [.0,b.[
;
ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " [.0,b.[ )then A8:
(+ (x,r)) . c in [.0,b.[
by FUNCT_1:def 7;
c in y>=0-plane
by Lm1;
then reconsider z =
c as
Point of
(TOP-REAL 2) ;
z = |[(z `1),(z `2)]|
by EUCLID:53;
then A9:
z `2 >= 0
by Lm1, Th18;
per cases
( (+ (x,r)) . c = 0 or ( 0 < (+ (x,r)) . c & (+ (x,r)) . c < b ) )
by A8, XXREAL_1:3;
suppose A10:
(+ (x,r)) . c = 0
;
ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " [.0,b.[ )reconsider r1 =
r * b as
positive Real by A6;
reconsider U =
(Ball (|[x,r1]|,r1)) \/ {|[x,0]|} as
Subset of
Niemytzki-plane by Th27;
take U =
U;
( U in Union BB & c in U & U c= (+ (x,r)) " [.0,b.[ )A11:
|[x,0]| in y>=0-plane
;
U in { ((Ball (|[x,q]|,q)) \/ {|[x,0]|}) where q is Real : q > 0 }
;
then A12:
U in BB . |[x,0]|
by A1;
z = |[x,0]|
by A10, A9, Th60;
hence
(
U in Union BB &
c in U &
U c= (+ (x,r)) " [.0,b.[ )
by A12, A11, A3, A6, Th67, CARD_5:2, ZFMISC_1:136;
verum end; suppose A13:
(
0 < (+ (x,r)) . c &
(+ (x,r)) . c < b )
;
ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " [.0,b.[ )reconsider r1 =
r * b as
positive Real by A6;
reconsider U =
Ball (
|[x,r1]|,
r1) as
Subset of
Niemytzki-plane by Th29;
take U =
U;
( U in Union BB & c in U & U c= (+ (x,r)) " [.0,b.[ )A14:
|[x,r1]| in y>=0-plane
;
U c= y>=0-plane
by Th20;
then
U /\ y>=0-plane = U
by XBOOLE_1:28;
then
U in { ((Ball (|[x,r1]|,q)) /\ y>=0-plane) where q is Real : q > 0 }
;
then
U in BB . |[x,r1]|
by A2;
hence
U in Union BB
by A14, A3, CARD_5:2;
( c in U & U c= (+ (x,r)) " [.0,b.[ )A15:
(+ (x,r)) " ].0,b.[ c= (+ (x,r)) " [.0,b.[
by RELAT_1:143, XXREAL_1:45;
Ball (
|[x,(r * b)]|,
(r * b))
c= (+ (x,r)) " ].0,b.[
by A13, Th66;
hence
(
c in U &
U c= (+ (x,r)) " [.0,b.[ )
by A15, A13, A7, A9, Th68;
verum end; end; end; hence
(+ (x,r)) " [.0,b.[ is
open
by YELLOW_9:31;
(+ (x,r)) " ].a,1.] is open now for c being Element of Niemytzki-plane st c in (+ (x,r)) " ].a,1.] holds
ex U being Subset of Niemytzki-plane st
( U in Union BB & c in U & U c= (+ (x,r)) " ].a,1.] )let c be
Element of
Niemytzki-plane;
( c in (+ (x,r)) " ].a,1.] implies ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " ].a,1.] ) )
c in y>=0-plane
by Lm1;
then reconsider z =
c as
Point of
(TOP-REAL 2) ;
assume
c in (+ (x,r)) " ].a,1.]
;
ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " ].a,1.] )then A16:
(+ (x,r)) . c in ].a,1.]
by FUNCT_1:def 7;
then A17:
(+ (x,r)) . c > a
by XXREAL_1:2;
A18:
(+ (x,r)) . c <= 1
by A16, XXREAL_1:2;
A19:
z = |[(z `1),(z `2)]|
by EUCLID:53;
then A20:
z `2 >= 0
by Lm1, Th18;
per cases
( z `2 > 0 or ( (+ (x,r)) . c = 1 & z `2 = 0 ) or ( a < (+ (x,r)) . c & (+ (x,r)) . c < 1 ) )
by A19, A16, A18, Lm1, Th18, XXREAL_0:1, XXREAL_1:2;
suppose
z `2 > 0
;
ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " ].a,1.] )then consider r1 being
positive Real such that A21:
r1 <= z `2
and A22:
Ball (
z,
r1)
c= (+ (x,r)) " ].a,1.]
by A4, A17, Th69;
reconsider U =
Ball (
z,
r1) as
Subset of
Niemytzki-plane by A19, A21, Th29;
U c= y>=0-plane
by A19, A21, Th20;
then A23:
U /\ y>=0-plane = U
by XBOOLE_1:28;
U in { ((Ball (|[(z `1),(z `2)]|,q)) /\ y>=0-plane) where q is Real : q > 0 }
by A23, A19;
then A24:
U in BB . |[(z `1),(z `2)]|
by A21, A2;
take U =
U;
( U in Union BB & c in U & U c= (+ (x,r)) " ].a,1.] )
|[(z `1),(z `2)]| in y>=0-plane
by A21;
hence
U in Union BB
by A24, A3, CARD_5:2;
( c in U & U c= (+ (x,r)) " ].a,1.] )thus
(
c in U &
U c= (+ (x,r)) " ].a,1.] )
by A22, Th13;
verum end; suppose A25:
(
(+ (x,r)) . c = 1 &
z `2 = 0 )
;
ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " ].a,1.] )then consider r1 being
positive Real such that A26:
(Ball (|[(z `1),r1]|,r1)) \/ {z} c= (+ (x,r)) " {1}
by Th70;
reconsider U =
(Ball (|[(z `1),r1]|,r1)) \/ {z} as
Subset of
Niemytzki-plane by A19, A25, Th27;
U in { ((Ball (|[(z `1),q]|,q)) \/ {|[(z `1),0]|}) where q is Real : q > 0 }
by A19, A25;
then A27:
U in BB . |[(z `1),(z `2)]|
by A1, A25;
take U =
U;
( U in Union BB & c in U & U c= (+ (x,r)) " ].a,1.] )
|[(z `1),(z `2)]| in y>=0-plane
by A25;
hence
U in Union BB
by A27, A3, CARD_5:2;
( c in U & U c= (+ (x,r)) " ].a,1.] )thus
c in U
by ZFMISC_1:136;
U c= (+ (x,r)) " ].a,1.]
1
in ].a,1.]
by A5, XXREAL_1:2;
then
{1} c= ].a,1.]
by ZFMISC_1:31;
then
(+ (x,r)) " {1} c= (+ (x,r)) " ].a,1.]
by RELAT_1:143;
hence
U c= (+ (x,r)) " ].a,1.]
by A26;
verum end; suppose
(
a < (+ (x,r)) . c &
(+ (x,r)) . c < 1 )
;
ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " ].a,1.] )then
(+ (x,r)) . c in ].a,1.[
by XXREAL_1:4;
then consider r1 being
positive Real such that A28:
r1 <= z `2
and A29:
Ball (
z,
r1)
c= (+ (x,r)) " ].a,1.[
by A4, A20, Th65;
reconsider U =
Ball (
z,
r1) as
Subset of
Niemytzki-plane by A19, A28, Th29;
U c= y>=0-plane
by A19, A28, Th20;
then A30:
U /\ y>=0-plane = U
by XBOOLE_1:28;
U in { ((Ball (|[(z `1),(z `2)]|,q)) /\ y>=0-plane) where q is Real : q > 0 }
by A30, A19;
then A31:
U in BB . |[(z `1),(z `2)]|
by A28, A2;
take U =
U;
( U in Union BB & c in U & U c= (+ (x,r)) " ].a,1.] )
|[(z `1),(z `2)]| in y>=0-plane
by A28;
hence
U in Union BB
by A31, A3, CARD_5:2;
( c in U & U c= (+ (x,r)) " ].a,1.] )
(+ (x,r)) " ].a,1.[ c= (+ (x,r)) " ].a,1.]
by RELAT_1:143, XXREAL_1:41;
hence
(
c in U &
U c= (+ (x,r)) " ].a,1.] )
by A29, Th13;
verum end; end; end; hence
(+ (x,r)) " ].a,1.] is
open
by YELLOW_9:31;
verum end;
hence
+ (x,r) is continuous
by Th75; verum