let V be RealUnitarySpace; :: thesis: for v being VECTOR of V
for r being Real st the carrier of V = {(0. V)} & r > 0 holds
Ball (v,r) = {(0. V)}
let v be VECTOR of V; :: thesis: for r being Real st the carrier of V = {(0. V)} & r > 0 holds
Ball (v,r) = {(0. V)}
let r be Real; :: thesis: ( the carrier of V = {(0. V)} & r > 0 implies Ball (v,r) = {(0. V)} )
assume that
A1: the carrier of V = {(0. V)} and
A2: r > 0 ; :: thesis: Ball (v,r) = {(0. V)}
for w being VECTOR of V st w in {(0. V)} holds
w in Ball (v,r)
proof
let w be VECTOR of V; :: thesis: ( w in {(0. V)} implies w in Ball (v,r) )
assume A3: w in {(0. V)} ; :: thesis: w in Ball (v,r)
v = 0. V by A1, TARSKI:def 1;
then ||.(v - w).|| = ||.((0. V) - (0. V)).|| by A3, TARSKI:def 1
.= ||.(0. V).||
.= 0 by BHSP_1:26 ;
then w in { y where y is Point of V : ||.(v - y).|| < r } by A2;
hence w in Ball (v,r) by BHSP_2:def 5; :: thesis: verum
end;
then {(0. V)} c= Ball (v,r) ;
hence Ball (v,r) = {(0. V)} by A1; :: thesis: verum