ball_smul — Mathlib

English

If c > 0 in NNReal, then the ball for the scaled seminorm c • p is the same as the ball for p with radius scaled by 1/c: (c • p).ball x r = p.ball x (r / c).

Русский

Если c > 0 в NNReal, шар под нормой, масштабированной на c, равен шару для p радиусом r/c.

LaTeX

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

Lean4

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

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