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)]