eHolderNorm_eq_top

Mathlib.Topology.MetricSpace.HolderNorm

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

English

eHolderNorm r f equals ∞ if and only if MemHolder r f does not hold.

Русский

eHolderNorm r f равно бесконечности тогда и только тогда, когда MemHolder r f не выполняется.

LaTeX

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

Lean4

@[simp]
theorem eHolderNorm_eq_top : eHolderNorm r f = ∞ ↔ ¬MemHolder r f := by rw [← eHolderNorm_ne_top, not_not]

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

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

Разделы

Аффилиация

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