eHolderNorm_zero

Mathlib.Topology.MetricSpace.HolderNorm

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

English

The NNHolderNorm of a constant function equals zero: nnHolderNorm r (Function.const X c) = 0.

Русский

NNHolderNorm константной функции равен нулю: nnHolderNorm r (Function.const X c) = 0.

LaTeX

$$$\mathrm{nnHolderNorm}(r,\mathrm{const}_X c) = 0.$$$

Lean4

@[simp]
theorem eHolderNorm_zero [Zero Y] (r : ℝ≥0) : eHolderNorm r (0 : X → Y) = 0 :=
  eHolderNorm_const X r 0

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

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

Разделы

Аффилиация

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