eLpNorm_ne_top

Mathlib.MeasureTheory.Function.LpSpace.Basic

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

English

For every f in Lp(E, p, μ), the extended Lp norm eLpNorm f p μ is finite (not equal to ∞).

Русский

Для каждого f ∈ Lp(E, p, μ) расширенная Lp-норма eLpNorm f p μ конечна (не равна ∞).

LaTeX

$$$eLpNorm(f,p,\mu) \neq \infty$$$

Lean4

@[aesop (rule_sets := [finiteness]) safe apply]
theorem eLpNorm_ne_top (f : Lp E p μ) : eLpNorm f p μ ≠ ∞ :=
  (eLpNorm_lt_top f).ne

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

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

Разделы

Аффилиация

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