smul_closedBall_subset — Mathlib

English

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

Русский

Если k ≠ 0, тогда k • p.closedBall 0 r = p.closedBall 0 (||k|| r).

LaTeX

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

Lean4

theorem smul_closedBall_subset {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} : k • p.closedBall 0 r ⊆ p.closedBall 0 (‖k‖ * r) :=
  by
  rintro x ⟨y, hy, h⟩
  rw [Seminorm.mem_closedBall_zero, ← h, map_smul_eq_mul]
  rw [Seminorm.mem_closedBall_zero] at hy
  gcongr

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