everywherePosSubset_ae_eq — Mathlib

English

For an inner regular measure, the everywhere-positivity of the subset μ.everywherePosSubset s holds.

Русский

При своей внутренней регулярности мера сохраняет свойство everywherePosSubset s как всюду положительное.

LaTeX

$$$$ μ.IsEverywherePos( μ.everywherePosSubset s). $$$$

Lean4

/-- In a space with an inner regular measure, any measurable set coincides almost everywhere with
its everywhere positive subset. -/
theorem everywherePosSubset_ae_eq [OpensMeasurableSpace α] [InnerRegular μ] (hs : MeasurableSet s) :
    μ.everywherePosSubset s =ᵐ[μ] s :=
  by
  simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), measure_empty, true_and,
    (hs.diff hs.everywherePosSubset).measure_eq_iSup_isCompact, ENNReal.iSup_eq_zero]
  intro k hk h'k
  exact measure_eq_zero_of_subset_diff_everywherePosSubset h'k hk

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