smul_unitBall_of_pos — Mathlib

English

If a ≤ 0 and r > 0, then Ioo(a,b) · sphere(0,r) equals the difference ball(0, br) minus closedBall(0, ar).

Русский

Если a ≤ 0 и r > 0, то Ioo(a,b)·sphere(0,r) = ball(0, br) \ closedBall(0, ar).

LaTeX

$$$\mathrm{Ioo}(a,b) \cdot \mathrm{sphere}(0,r) = \mathrm{ball}(0, br) \setminus \mathrm{closedBall}(0, ar).$$$

Lean4

/-- In a real normed space, the image of the unit ball under scalar multiplication by a positive
constant `r` is the ball of radius `r`. -/
theorem smul_unitBall_of_pos {r : ℝ} (hr : 0 < r) : r • ball (0 : E) 1 = ball (0 : E) r := by
  rw [smul_unitBall hr.ne', Real.norm_of_nonneg hr.le]

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