affinity_unitClosedBall — Mathlib

English

For r ≥ 0 and x ∈ E, the map y ↦ x + y scales the unit closed ball to the closed ball with center x and radius r: x +ᵥ r • closedBall(0,1) = closedBall(x,r).

Русский

Для r ≥ 0 и x ∈ E отображение переносит единичный замкнутый шар в замкнутый шар радиуса r вокруг x: x +ᵥ r • closedBall(0,1) = closedBall(x,r).

LaTeX

$$$x +\\!_v (r \\cdot \\overline{B}(0,1)) = \\overline{B}(x,r)$$$

Lean4

/-- Any closed ball `Metric.closedBall x r`, `0 ≤ r` is the image of the unit closed ball under
`fun y ↦ x + r • y`. -/
theorem affinity_unitClosedBall {r : ℝ} (hr : 0 ≤ r) (x : E) : x +ᵥ r • closedBall (0 : E) 1 = closedBall x r := by
  rw [smul_unitClosedBall, Real.norm_of_nonneg hr, vadd_closedBall_zero]

Похожие утверждения