let V be RealUnitarySpace; for v being VECTOR of V
for r being Real st the carrier of V <> {(0. V)} & r > 0 holds
ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )
let v be VECTOR of V; for r being Real st the carrier of V <> {(0. V)} & r > 0 holds
ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )
let r be Real; ( the carrier of V <> {(0. V)} & r > 0 implies ex w being VECTOR of V st
( w <> v & w in Ball (v,r) ) )
assume that
A1:
the carrier of V <> {(0. V)}
and
A2:
r > 0
; ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )
consider r9 being Real such that
A3:
0 < r9
and
A4:
r9 < r
by A2, XREAL_1:5;
reconsider r9 = r9 as Real ;
now ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )per cases
( v = 0. V or v <> 0. V )
;
suppose A5:
v = 0. V
;
ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )
ex
w being
VECTOR of
V st
(
w <> 0. V &
||.w.|| < r )
proof
not the
carrier of
V c= {(0. V)}
by A1;
then
NonZero V <> {}
by XBOOLE_1:37;
then consider u being
object such that A6:
u in NonZero V
by XBOOLE_0:def 1;
A7:
not
u in {(0. V)}
by A6, XBOOLE_0:def 5;
reconsider u =
u as
VECTOR of
V by A6;
A8:
u <> 0. V
by A7, TARSKI:def 1;
then A9:
||.u.|| <> 0
by BHSP_1:26;
set a =
||.u.||;
A10:
||.u.|| >= 0
by BHSP_1:28;
take w =
(r9 / ||.u.||) * u;
( w <> 0. V & ||.w.|| < r )
A11:
||.w.|| =
|.(r9 / ||.u.||).| * ||.u.||
by BHSP_1:27
.=
(r9 / ||.u.||) * ||.u.||
by A3, A10, ABSVALUE:def 1
.=
r9 / (||.u.|| / ||.u.||)
by XCMPLX_1:81
.=
r9
by A9, XCMPLX_1:51
;
r9 / ||.u.|| > 0
by A3, A9, A10, XREAL_1:139;
hence
(
w <> 0. V &
||.w.|| < r )
by A4, A8, A11, RLVECT_1:11;
verum
end; then consider u being
VECTOR of
V such that A12:
u <> 0. V
and A13:
||.u.|| < r
;
||.(v - u).|| =
||.(- u).||
by A5
.=
||.u.||
by BHSP_1:31
;
then
u in { y where y is Point of V : ||.(v - y).|| < r }
by A13;
then
u in Ball (
v,
r)
by BHSP_2:def 5;
hence
ex
w being
VECTOR of
V st
(
w <> v &
w in Ball (
v,
r) )
by A5, A12;
verum
hence
ex w being VECTOR of V st
( w <> v & w in Ball (v,r) )
; verum