essSup_eq_iSup — Mathlib

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]

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