eLpNormEssSup_eq_iSup

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.eLpNormEssSup_eq_iSup

English

Similarly, eLpNorm f p ν ≤ eLpNorm f p (μ+ν).

Русский

Аналогично, eLpNorm f p ν ≤ eLpNorm f p (μ+ν).

LaTeX

$$eLpNorm f p ν ≤ eLpNorm f p (μ+ν).$$

Lean4

theorem eLpNormEssSup_eq_iSup (hμ : ∀ a, μ { a } ≠ 0) (f : α → ε) : eLpNormEssSup f μ = ⨆ a, ‖f a‖ₑ :=
  essSup_eq_iSup hμ _

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

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

Разделы

Аффилиация

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