smul_ball_zero — Mathlib

English

If k ≠ 0, k • p.ball 0 r = p.ball 0 (||k|| r).

Русский

Если k ≠ 0, то k • p.ball 0 r = p.ball 0 (||k|| r).

LaTeX

$$$k \neq 0 \Rightarrow k \cdot p.ball(0,r) = p.ball(0,\|k\| r)$$$

Lean4

theorem smul_ball_zero {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} (hk : k ≠ 0) : k • p.ball 0 r = p.ball 0 (‖k‖ * r) :=
  by
  ext
  rw [mem_smul_set_iff_inv_smul_mem₀ hk, p.mem_ball_zero, p.mem_ball_zero, map_smul_eq_mul, norm_inv, ← div_eq_inv_mul,
    div_lt_iff₀ (norm_pos_iff.2 hk), mul_comm]

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