essInf_antitone_measure

Mathlib.MeasureTheory.Function.EssSup

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

← MathLib Explorer

English

If μ ≪ ν, then essInf f ν ≤ essInf f μ.

Русский

Если μ эквивалентна (важна в отношении) ν, тогда essInf f ν ≤ essInf f μ.

LaTeX

$$essInf f ν ≤ essInf f μ$$

Lean4

theorem essInf_antitone_measure {f : α → β} (hμν : μ ≪ ν) : essInf f ν ≤ essInf f μ :=
  by
  refine liminf_le_liminf_of_le (Measure.ae_le_iff_absolutelyContinuous.mpr hμν) ?_ ?_
  all_goals isBoundedDefault

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

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

Разделы

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

Аффилиация

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