essSup_eq_sInf — Mathlib

English

In a dual form, essInf equals sInf of the set of thresholds defined by a relation with f.

Русский

В двойственной форме essInf равен sInf порогов, заданных в отношении к f.

LaTeX

$$$\text{essInf } f μ = sInf{ a | μ{ x | f x < a } = 0 }$.$$

Lean4

theorem essSup_eq_sInf {m : MeasurableSpace α} (μ : Measure α) (f : α → β) :
    essSup f μ = sInf {a | μ {x | a < f x} = 0} :=
  by
  dsimp [essSup, limsup, limsSup]
  simp only [eventually_map, ae_iff, not_le]

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