ae_le_essSup

Mathlib.MeasureTheory.Function.EssSup

URI: https://scilib.ai/kg/mathlib#ENNReal.ae_le_essSup

English

For any f, f(y) ≤ essSup f μ holds almost everywhere.

Русский

Для любого f почти всюду выполняется f(y) ≤ essSup f μ.

LaTeX

$$$$ \\forall f: \\alpha \\to \\mathbb{R}_{\\ge 0}^\\infty, \\ f \\le^{\\mathrm{ae}}_{\\mu} \\operatorname{essSup} f \\mu $$$$

Lean4

theorem ae_le_essSup (f : α → ℝ≥0∞) : ∀ᵐ y ∂μ, f y ≤ essSup f μ :=
  eventually_le_limsup f

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

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

Разделы

Аффилиация

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