set f = + (x,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:
dom BB = y>=0-plane
by Lm1, PARTFUN1:def 4;
now let a,
b be
real number ;
( 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 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 13;
c in y>=0-plane
by Lm1;
then reconsider z =
c as
Point of
(TOP-REAL 2) ;
z = |[(z `1),(z `2)]|
by EUCLID:57;
then A9:
z `2 >= 0
by Lm1, Th22;
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
real positive number by A6;
reconsider U =
(Ball (|[x,r1]|,r1)) \/ {|[x,0]|} as
Subset of
Niemytzki-plane by Th31;
take U =
U;
( U in Union BB & c in U & U c= (+ (x,r)) " [.0,b.[ )A11:
x is
Real
by XREAL_0:def 1;
then A12:
|[x,0]| in y>=0-plane
;
r1 is
Real
by XREAL_0:def 1;
then
U in { ((Ball (|[x,q]|,q)) \/ {|[x,0]|}) where q is Element of REAL : q > 0 }
;
then A13:
U in BB . |[x,0]|
by A1, A11;
z = |[x,0]|
by A10, A9, Th64;
hence
(
U in Union BB &
c in U &
U c= (+ (x,r)) " [.0,b.[ )
by A13, A12, A3, A6, Th71, CARD_5:10, SETWISEO:6;
verum end; suppose A14:
(
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
real positive number by A6;
A15:
r1 is
Real
by XREAL_0:def 1;
reconsider U =
Ball (
|[x,r1]|,
r1) as
Subset of
Niemytzki-plane by Th33;
take U =
U;
( U in Union BB & c in U & U c= (+ (x,r)) " [.0,b.[ )A16:
x is
Real
by XREAL_0:def 1;
then A17:
|[x,r1]| in y>=0-plane
by A15;
U c= y>=0-plane
by Th24;
then
U /\ y>=0-plane = U
by XBOOLE_1:28;
then
U in { ((Ball (|[x,r1]|,q)) /\ y>=0-plane) where q is Element of REAL : q > 0 }
by A15;
then
U in BB . |[x,r1]|
by A2, A15, A16;
hence
U in Union BB
by A17, A3, CARD_5:10;
( c in U & U c= (+ (x,r)) " [.0,b.[ )A18:
(+ (x,r)) " ].0,b.[ c= (+ (x,r)) " [.0,b.[
by RELAT_1:178, XXREAL_1:45;
Ball (
|[x,(r * b)]|,
(r * b))
c= (+ (x,r)) " ].0,b.[
by A14, Th70;
hence
(
c in U &
U c= (+ (x,r)) " [.0,b.[ )
by A18, A14, A7, A9, Th72, XBOOLE_1:1;
verum end; end; hence
(+ (x,r)) " [.0,b.[ is
open
by YELLOW_9:31;
(+ (x,r)) " ].a,1.] is open now 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 A19:
(+ (x,r)) . c in ].a,1.]
by FUNCT_1:def 13;
then A20:
(+ (x,r)) . c > a
by XXREAL_1:2;
A21:
(+ (x,r)) . c <= 1
by A19, XXREAL_1:2;
A22:
z = |[(z `1),(z `2)]|
by EUCLID:57;
then A23:
z `2 >= 0
by Lm1, Th22;
per cases
( z `2 > 0 or ( (+ (x,r)) . c = 1 & z `2 = 0 ) or ( a < (+ (x,r)) . c & (+ (x,r)) . c < 1 ) )
by A22, A19, A21, Lm1, Th22, 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
real positive number such that A24:
r1 <= z `2
and A25:
Ball (
z,
r1)
c= (+ (x,r)) " ].a,1.]
by A4, A20, Th73;
reconsider U =
Ball (
z,
r1) as
Subset of
Niemytzki-plane by A22, A24, Th33;
U c= y>=0-plane
by A22, A24, Th24;
then A26:
U /\ y>=0-plane = U
by XBOOLE_1:28;
r1 is
Real
by XREAL_0:def 1;
then
U in { ((Ball (|[(z `1),(z `2)]|,q)) /\ y>=0-plane) where q is Element of REAL : q > 0 }
by A26, A22;
then A27:
U in BB . |[(z `1),(z `2)]|
by A24, 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 A24;
hence
U in Union BB
by A27, A3, CARD_5:10;
( c in U & U c= (+ (x,r)) " ].a,1.] )thus
(
c in U &
U c= (+ (x,r)) " ].a,1.] )
by A25, Th17;
verum end; suppose A28:
(
(+ (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
real positive number such that A29:
(Ball (|[(z `1),r1]|,r1)) \/ {z} c= (+ (x,r)) " {1}
by Th74;
reconsider U =
(Ball (|[(z `1),r1]|,r1)) \/ {z} as
Subset of
Niemytzki-plane by A22, A28, Th31;
r1 is
Real
by XREAL_0:def 1;
then
U in { ((Ball (|[(z `1),q]|,q)) \/ {|[(z `1),0]|}) where q is Element of REAL : q > 0 }
by A22, A28;
then A30:
U in BB . |[(z `1),(z `2)]|
by A1, A28;
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 A30, A3, CARD_5:10;
( c in U & U c= (+ (x,r)) " ].a,1.] )thus
c in U
by SETWISEO:6;
U c= (+ (x,r)) " ].a,1.]
1
in ].a,1.]
by A5, XXREAL_1:2;
then
{1} c= ].a,1.]
by ZFMISC_1:37;
then
(+ (x,r)) " {1} c= (+ (x,r)) " ].a,1.]
by RELAT_1:178;
hence
U c= (+ (x,r)) " ].a,1.]
by A29, XBOOLE_1:1;
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
real positive number such that A31:
r1 <= z `2
and A32:
Ball (
z,
r1)
c= (+ (x,r)) " ].a,1.[
by A4, A23, Th69;
reconsider U =
Ball (
z,
r1) as
Subset of
Niemytzki-plane by A22, A31, Th33;
U c= y>=0-plane
by A22, A31, Th24;
then A33:
U /\ y>=0-plane = U
by XBOOLE_1:28;
r1 is
Real
by XREAL_0:def 1;
then
U in { ((Ball (|[(z `1),(z `2)]|,q)) /\ y>=0-plane) where q is Element of REAL : q > 0 }
by A33, A22;
then A34:
U in BB . |[(z `1),(z `2)]|
by A31, 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 A31;
hence
U in Union BB
by A34, A3, CARD_5:10;
( c in U & U c= (+ (x,r)) " ].a,1.] )
(+ (x,r)) " ].a,1.[ c= (+ (x,r)) " ].a,1.]
by RELAT_1:178, XXREAL_1:41;
hence
(
c in U &
U c= (+ (x,r)) " ].a,1.] )
by A32, Th17, XBOOLE_1:1;
verum end; end; hence
(+ (x,r)) " ].a,1.] is
open
by YELLOW_9:31;
verum end;
hence
+ (x,r) is continuous
by Th79; verum