eLpNorm_ne_top

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.MemLp.eLpNorm_ne_top

English

Moreover, eLpNorm f p μ ≠ ∞ for MemLp f.

Русский

Кроме того, eLpNorm f p μ не равно бесконечности.

LaTeX

$$$eLpNorm f\,p\,\mu \neq \infty$ for MemLp f.$$

Lean4

theorem eLpNorm_ne_top [TopologicalSpace ε] {f : α → ε} (hfp : MemLp f p μ) : eLpNorm f p μ ≠ ∞ :=
  ne_of_lt hfp.2

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

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

Разделы

Аффилиация

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