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