nsmul

Mathlib.Topology.MetricSpace.HolderNorm

URI: https://scilib.ai/kg/mathlib#MemHolder.nsmul

English

If hf : MemHolder r f, then MemHolder r (n • f) for any natural number n.

Русский

Если hf: MemHolder r f, то MemHolder r (n • f) для любого натурального n.

LaTeX

$$$\operatorname{MemHolder}(r,f) \Rightarrow \operatorname{MemHolder}(r, n\cdot f).$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru