eHolderNorm_le

Mathlib.Topology.MetricSpace.HolderNorm

URI: https://scilib.ai/kg/mathlib#HolderWith.eHolderNorm_le

English

If X is empty, then eHolderNorm r f = 0 (variant statement).

Русский

Если X пусто, то eHolderNorm r f = 0 (вариант формулировки).

LaTeX

$$$\text{IsEmpty}(X) \Rightarrow eHolderNorm(r,f) = 0$$$

Lean4

theorem eHolderNorm_le {C : ℝ≥0} (hf : HolderWith C r f) : eHolderNorm r f ≤ C :=
  iInf₂_le C hf

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

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

Разделы

Аффилиация

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