essSup_mono_measure — Mathlib

English

If μ is absolutely continuous with respect to ν, then essInf f ν ≥ essInf f μ.

Русский

Если μ абсолютно непрерывна по отношению к ν, то essInf f ν ≥ essInf f μ.

LaTeX

$$$essInf f ν ≥ essInf f μ$$$

Lean4

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

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