English
If every singleton has positive measure, then the essential supremum of any function f: α→β equals the supremum of its pointwise values, i.e. essSup f μ = ⨆ i, f i.
Русский
Если для каждой точки a множество {a} имеет ненулевую меру, то эс-суп функции f:α→β по мере μ равен наибольшему по смыслу значениям функции: essSup f μ = ⨆ i, f i.
LaTeX
$$$\operatorname{essSup} f\ μ = \big\lubar_{i} f i\big\rubar$$$
Lean4
theorem essSup_eq_iSup (hμ : ∀ a, μ { a } ≠ 0) (f : α → β) : essSup f μ = ⨆ i, f i := by
rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_iSup]