let a be Real; for X being non empty compact Subset of (TOP-REAL 2)
for p being Point of (Euclid 2) st p = 0. (TOP-REAL 2) & a > 0 holds
X c= Ball (p,((((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a))
let X be non empty compact Subset of (TOP-REAL 2); for p being Point of (Euclid 2) st p = 0. (TOP-REAL 2) & a > 0 holds
X c= Ball (p,((((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a))
let p be Point of (Euclid 2); ( p = 0. (TOP-REAL 2) & a > 0 implies X c= Ball (p,((((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a)) )
assume that
A1:
p = 0. (TOP-REAL 2)
and
A2:
a > 0
; X c= Ball (p,((((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a))
set A = X;
set n = N-bound X;
set s = S-bound X;
set e = E-bound X;
set w = W-bound X;
set r = (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a;
A3:
(((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + 0 < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a
by A2, XREAL_1:8;
let x be object ; TARSKI:def 3 ( not x in X or x in Ball (p,((((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a)) )
assume A4:
x in X
; x in Ball (p,((((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a))
then reconsider b = x as Point of (Euclid 2) by TOPREAL3:8;
reconsider P = p, B = b as Point of (TOP-REAL 2) by TOPREAL3:8;
A5:
P `1 = 0
by A1, Th22;
A6:
B `1 <= E-bound X
by A4, PSCOMP_1:24;
A7:
B `2 <= N-bound X
by A4, PSCOMP_1:24;
A8:
S-bound X <= B `2
by A4, PSCOMP_1:24;
A9:
P `2 = 0
by A1, Th22;
A10: dist (p,b) =
(Pitag_dist 2) . (p,b)
by METRIC_1:def 1
.=
sqrt ((((P `1) - (B `1)) ^2) + (((P `2) - (B `2)) ^2))
by TOPREAL3:7
.=
sqrt (((B `1) ^2) + ((B `2) ^2))
by A5, A9
;
A11:
0 <= (B `2) ^2
by XREAL_1:63;
0 <= (B `1) ^2
by XREAL_1:63;
then
sqrt (((B `1) ^2) + ((B `2) ^2)) <= (sqrt ((B `1) ^2)) + (sqrt ((B `2) ^2))
by A11, SQUARE_1:59;
then
sqrt (((B `1) ^2) + ((B `2) ^2)) <= |.(B `1).| + (sqrt ((B `2) ^2))
by COMPLEX1:72;
then A12:
sqrt (((B `1) ^2) + ((B `2) ^2)) <= |.(B `1).| + |.(B `2).|
by COMPLEX1:72;
A13:
0 <= |.(N-bound X).|
by COMPLEX1:46;
A14:
0 <= |.(E-bound X).|
by COMPLEX1:46;
A15:
0 <= |.(W-bound X).|
by COMPLEX1:46;
A16:
0 <= |.(S-bound X).|
by COMPLEX1:46;
A17:
W-bound X <= B `1
by A4, PSCOMP_1:24;
now ( ( B `1 >= 0 & B `2 >= 0 & dist (p,b) < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a ) or ( B `1 < 0 & B `2 >= 0 & dist (p,b) < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a ) or ( B `1 >= 0 & B `2 < 0 & dist (p,b) < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a ) or ( B `1 < 0 & B `2 < 0 & dist (p,b) < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a ) )per cases
( ( B `1 >= 0 & B `2 >= 0 ) or ( B `1 < 0 & B `2 >= 0 ) or ( B `1 >= 0 & B `2 < 0 ) or ( B `1 < 0 & B `2 < 0 ) )
;
case A18:
(
B `1 >= 0 &
B `2 >= 0 )
;
dist (p,b) < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a
(|.(E-bound X).| + |.(N-bound X).|) + 0 <= (|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|
by A15, XREAL_1:7;
then
|.(E-bound X).| + |.(N-bound X).| <= ((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|
by A16, XREAL_1:7;
then A19:
|.(E-bound X).| + |.(N-bound X).| < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a
by A3, XXREAL_0:2;
A20:
|.(B `2).| <= |.(N-bound X).|
by A7, A18, Th1;
|.(B `1).| <= |.(E-bound X).|
by A6, A18, Th1;
then
|.(B `1).| + |.(B `2).| <= |.(E-bound X).| + |.(N-bound X).|
by A20, XREAL_1:7;
then
dist (
p,
b)
<= |.(E-bound X).| + |.(N-bound X).|
by A10, A12, XXREAL_0:2;
hence
dist (
p,
b)
< (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a
by A19, XXREAL_0:2;
verum end; case A21:
(
B `1 < 0 &
B `2 >= 0 )
;
dist (p,b) < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a
0 + (|.(N-bound X).| + |.(W-bound X).|) <= |.(E-bound X).| + (|.(N-bound X).| + |.(W-bound X).|)
by A14, XREAL_1:7;
then
|.(W-bound X).| + |.(N-bound X).| <= ((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|
by A16, XREAL_1:7;
then A22:
|.(W-bound X).| + |.(N-bound X).| < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a
by A3, XXREAL_0:2;
A23:
|.(B `2).| <= |.(N-bound X).|
by A7, A21, Th1;
|.(B `1).| <= |.(W-bound X).|
by A17, A21, Th2;
then
|.(B `1).| + |.(B `2).| <= |.(W-bound X).| + |.(N-bound X).|
by A23, XREAL_1:7;
then
dist (
p,
b)
<= |.(W-bound X).| + |.(N-bound X).|
by A10, A12, XXREAL_0:2;
hence
dist (
p,
b)
< (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a
by A22, XXREAL_0:2;
verum end; case A24:
(
B `1 >= 0 &
B `2 < 0 )
;
dist (p,b) < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + aA25:
((|.(E-bound X).| + |.(N-bound X).|) + |.(S-bound X).|) + 0 <= ((|.(E-bound X).| + |.(N-bound X).|) + |.(S-bound X).|) + |.(W-bound X).|
by A15, XREAL_1:7;
(|.(E-bound X).| + |.(S-bound X).|) + 0 <= (|.(E-bound X).| + |.(S-bound X).|) + |.(N-bound X).|
by A13, XREAL_1:7;
then
|.(E-bound X).| + |.(S-bound X).| <= ((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|
by A25, XXREAL_0:2;
then A26:
|.(E-bound X).| + |.(S-bound X).| < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a
by A3, XXREAL_0:2;
A27:
|.(B `2).| <= |.(S-bound X).|
by A8, A24, Th2;
|.(B `1).| <= |.(E-bound X).|
by A6, A24, Th1;
then
|.(B `1).| + |.(B `2).| <= |.(E-bound X).| + |.(S-bound X).|
by A27, XREAL_1:7;
then
dist (
p,
b)
<= |.(E-bound X).| + |.(S-bound X).|
by A10, A12, XXREAL_0:2;
hence
dist (
p,
b)
< (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a
by A26, XXREAL_0:2;
verum end; case A28:
(
B `1 < 0 &
B `2 < 0 )
;
dist (p,b) < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + athen A29:
|.(B `2).| <= |.(S-bound X).|
by A8, Th2;
|.(B `1).| <= |.(W-bound X).|
by A17, A28, Th2;
then
|.(B `1).| + |.(B `2).| <= |.(W-bound X).| + |.(S-bound X).|
by A29, XREAL_1:7;
then A30:
dist (
p,
b)
<= |.(W-bound X).| + |.(S-bound X).|
by A10, A12, XXREAL_0:2;
0 + (|.(W-bound X).| + |.(S-bound X).|) <= (|.(E-bound X).| + |.(N-bound X).|) + (|.(W-bound X).| + |.(S-bound X).|)
by A14, A13, XREAL_1:7;
then
|.(W-bound X).| + |.(S-bound X).| < (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a
by A2, XREAL_1:8;
hence
dist (
p,
b)
< (((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a
by A30, XXREAL_0:2;
verum end; end; end;
hence
x in Ball (p,((((|.(E-bound X).| + |.(N-bound X).|) + |.(W-bound X).|) + |.(S-bound X).|) + a))
by METRIC_1:11; verum