closedBall_smul — Mathlib

English

If c > 0 in NNReal, then (c • p).closedBall x r = p.closedBall x (r / c).

Русский

Если c > 0 в NNReal, то (c • p).closedBall x r = p.closedBall x (r / c).

LaTeX

$$$ (c \\cdot p).closedBall\, x\, r = p.closedBall\, x\, \\frac{r}{c} $$$

Lean4

theorem closedBall_smul (p : Seminorm 𝕜 E) {c : NNReal} (hc : 0 < c) (r : ℝ) (x : E) :
    (c • p).closedBall x r = p.closedBall x (r / c) := by
  ext
  rw [mem_closedBall, mem_closedBall, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    le_div_iff₀ (NNReal.coe_pos.mpr hc)]

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