smul_unitClosedBall_of_nonneg — Mathlib

English

If r ≥ 0, then r • closedBall(0,1) = closedBall(0,r).

Русский

Если радиус неотрицателен, то r • B̄(0,1) = B̄(0,r).

LaTeX

$$$r \\ge 0 \\implies r \\cdot \\overline{B}(0,1) = \\overline{B}(0,r)$$$

Lean4

/-- In a real normed space, the image of the unit closed ball under multiplication by a nonnegative
number `r` is the closed ball of radius `r` with center at the origin. -/
theorem smul_unitClosedBall_of_nonneg {r : ℝ} (hr : 0 ≤ r) : r • closedBall (0 : E) 1 = closedBall (0 : E) r := by
  rw [smul_unitClosedBall, Real.norm_of_nonneg hr]

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