English
If s has finite measure (μ s ≠ ∞) and is measurable, then μ.everywherePosSubset s equals s almost everywhere.
Русский
Если μ s не бесконечно и s измеримо, то everywherePosSubset s совпадает с s почти surely.
LaTeX
$$$$ μ.everywherePosSubset s =^a_μ s. $$$$
Lean4
/-- In a space with an inner regular measure for finite measure sets, any measurable set of finite
measure coincides almost everywhere with its everywhere positive subset. -/
theorem everywherePosSubset_ae_eq_of_measure_ne_top [OpensMeasurableSpace α] [InnerRegularCompactLTTop μ]
(hs : MeasurableSet s) (h's : μ s ≠ ∞) : μ.everywherePosSubset s =ᵐ[μ] s :=
by
have A : μ (s \ μ.everywherePosSubset s) ≠ ∞ := ((measure_mono diff_subset).trans_lt h's.lt_top).ne
simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), measure_empty, true_and,
(hs.diff hs.everywherePosSubset).measure_eq_iSup_isCompact_of_ne_top A, ENNReal.iSup_eq_zero]
intro k hk h'k
exact measure_eq_zero_of_subset_diff_everywherePosSubset h'k hk
