nnnorm_nsmul — Mathlib

English

For any natural n and x in a NormedAddCommMonoid, the nnnorm is homogeneous: ‖n • x‖₊ = n • ‖x‖₊.

Русский

Для любого натурального n и x в нормированном аддитивном коммутативном моное выполняется: ‖n · x‖₊ = n · ‖x‖₊.

LaTeX

$$$$\| n \cdot x \|_{+} = n \cdot \| x \|_{+}.$$$$

Lean4

theorem nnnorm_nsmul [NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E) : ‖n • x‖₊ = n • ‖x‖₊ := by
  simpa [Nat.cast_smul_eq_nsmul] using nnnorm_smul (n : K) x

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