essInf_eq_sSup — Mathlib

English

Symmetric relation: essInf can also be represented by a supremum form via dual lattice.

Русский

Симметричное представление essInf через сопряженную решетку.

LaTeX

$$$essInf f μ = sSup{ a | μ {x | f x < a} = 0 }$.$$

Lean4

theorem essInf_eq_sSup {m : MeasurableSpace α} (μ : Measure α) (f : α → β) :
    essInf f μ = sSup {a | μ {x | f x < a} = 0} :=
  by
  dsimp [essInf, liminf, limsInf]
  simp only [eventually_map, ae_iff, not_le]

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