eHolderNorm_nsmul

Mathlib.Topology.MetricSpace.HolderNorm

URI: https://scilib.ai/kg/mathlib#eHolderNorm_nsmul

← MathLib Explorer

English

For a natural number n, eHolderNorm r (n • f) = n • eHolderNorm r f.

Русский

Для натурального числа n: eHolderNorm r (n • f) = n • eHolderNorm r f.

LaTeX

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

Lean4

theorem eHolderNorm_nsmul [NormedSpace ℝ Y] (n : ℕ) : eHolderNorm r (n • f) = n • eHolderNorm r f := by
  simp [← Nat.cast_smul_eq_nsmul (R := ℝ), eHolderNorm_smul]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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