Theorems · Theorem · functional analysis

affinity_unitClosedBall

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
  0 ≤ r → ∀ (x : E), x +ᵥ r • Metric.closedBall 0 1 = Metric.closedBall x r

Any closed ball Metric.closedBall x r, 0 ≤ r is the image of the unit closed ball under fun y ↦ x + r • y.

Defined in

Mathlib.Analysis.Normed.Module.Ball.Pointwise

Cited by

1 results in Mathlib

Foundations

Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace