nnHolderNorm_nsmul — Mathlib

English

If hf is MemHolder r f, then for natural n, nnHolderNorm r (n • f) = n • nnHolderNorm r f.

Русский

Пусть hf: MemHolder r f. Тогда для натурального n: nnHolderNorm r (n • f) = n • nnHolderNorm r f.

LaTeX

$$$nnHolderNorm\, r\; (n \cdot f) = n \cdot nnHolderNorm\, r\; f$$$

Lean4

theorem nnHolderNorm_nsmul [NormedSpace ℝ Y] (n : ℕ) (hf : MemHolder r f) :
    nnHolderNorm r (n • f) = n • nnHolderNorm r f := by simp [← Nat.cast_smul_eq_nsmul (R := ℝ), hf.nnHolderNorm_smul]

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