eHolderNorm_ne_top

Mathlib.Topology.MetricSpace.HolderNorm

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

English

For any r and f, eHolderNorm r f ≠ ∞ if and only if MemHolder r f.

Русский

Для любых r и f, eHolderNorm r f не равно бесконечности ↔ MemHolder r f.

LaTeX

$$$eHolderNorm(r,f) \neq \infty \iff \operatorname{MemHolder}(r,f).$$$

Lean4

theorem eHolderNorm_ne_top : eHolderNorm r f ≠ ∞ ↔ MemHolder r f := by rw [← eHolderNorm_lt_top, lt_top_iff_ne_top]

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

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

Разделы

Аффилиация

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