essInf_eq_ciInf

Mathlib.MeasureTheory.Function.EssSup

URI: https://scilib.ai/kg/mathlib#essInf_eq_ciInf

← MathLib Explorer

English

Analogous equality for essInf with ciInf over the domain.

Русский

Аналогичное равенство для essInf и ciInf.

LaTeX

$$$[finite α] \Rightarrow essInf f μ = iInf f a$.$$

Lean4

theorem essInf_eq_ciInf (hμ : ∀ a, μ { a } ≠ 0) (hf : BddBelow (Set.range f)) : essInf f μ = ⨅ a, f a := by
  rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_ciInf hf]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru