nnholderNorm_le

Mathlib.Topology.MetricSpace.HolderNorm

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

← MathLib Explorer

English

For hf: HolderWith C r f, eHolderNorm r f ≤ C (in ENNReal sense).

Русский

Для hf: HolderWith C r f, eHolderNorm r f ≤ C (в смысле ENNReal).

LaTeX

$$$eHolderNorm(r,f) \le \operatorname{ofNNReal}(C).$$$

Lean4

theorem nnholderNorm_le {C r : ℝ≥0} {f : X → Y} (hf : HolderWith C r f) : nnHolderNorm r f ≤ C :=
  by
  rw [← ENNReal.coe_le_coe, hf.memHolder.coe_nnHolderNorm_eq_eHolderNorm]
  exact hf.eHolderNorm_le

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

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

Разделы

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

Аффилиация

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