essSup_eq_ciSup — Mathlib

English

In the supremum form, essSup f μ equals iSup of f(a) under boundedness assumptions.

Русский

В форме верхнего предела essSup равен iSup f(a) при ограниченности.

LaTeX

$$$(hf) : BddAbove (Set.range f) \Rightarrow essSup f μ = iSup (\lambda a, f a)$.$$

Lean4

theorem essSup_eq_ciSup (hμ : ∀ a, μ { a } ≠ 0) (hf : BddAbove (Set.range f)) : essSup f μ = ⨆ a, f a := by
  rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_ciSup hf]

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