English
Under translation by a fixed vector x, a ball around y of radius r becomes a ball around x+y of radius r: x +ᵥ p.ball y r = p.ball (x +ᵥ y) r.
Русский
Применение переноса на вектор x переводит шар вокруг y на шар вокруг x+y той же радиусности: x +ᵥ p.ball y r = p.ball (x +ᵥ y) r.
LaTeX
$$$x +\!\!\, p.ball y r = p.ball (x + y) r$$$
Lean4
/-- The image of a ball under addition with a singleton is another ball. -/
theorem vadd_ball (p : Seminorm 𝕜 E) : x +ᵥ p.ball y r = p.ball (x +ᵥ y) r :=
letI := AddGroupSeminorm.toSeminormedAddCommGroup p.toAddGroupSeminorm
Metric.vadd_ball x y r