ae_le_eLpNormEssSup

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

English

For f: α → ε, almost everywhere, ∥f(y)∥ ≤ eLpNormEssSup f μ.

Русский

Пусть f: α → ε. Почти всюду выполняется неравенство ∥f(y)∥ ≤ eLpNormEssSup f μ.

LaTeX

$$∀ᵐ y ∂μ, ∥f(y)∥ ≤ eLpNormEssSup f μ$$

Lean4

theorem ae_le_eLpNormEssSup {f : α → ε} : ∀ᵐ y ∂μ, ‖f y‖ₑ ≤ eLpNormEssSup f μ :=
  ae_le_essSup

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

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

Разделы

Аффилиация

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