essSup_liminf_le — Mathlib

English

Let f: ι → α → ℝ≥0∞ with countable ι. Then

Русский

Пусть f: ι → α → ℝ≥0∞ и ι счётно; тогда

LaTeX

$$$$ \operatorname{ess\,sup}_{\mu} \bigl( \operatorname{atTop}.\operatorname{liminf}_{n} f(n, x) \bigr) \le \operatorname{atTop}.\operatorname{liminf}_{n} \operatorname{ess\,sup}_{x} f(n, x) .$$$

Lean4

theorem essSup_liminf_le {ι} [Countable ι] [Preorder ι] (f : ι → α → ℝ≥0∞) :
    essSup (fun x => atTop.liminf fun n => f n x) μ ≤ atTop.liminf fun n => essSup (fun x => f n x) μ :=
  by
  simp_rw [essSup]
  exact ENNReal.limsup_liminf_le_liminf_limsup fun a b => f b a

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