English
If μ s ≠ ∞ and μ InnerRegularCompactLTTop, then μ.IsEverywherePos(μ.everywherePosSubset s).
Русский
Если μ s ≠ ∞ и μ удовлетворяет внутренней регулярности на компакт-ограничениях, то μ.everywherePosSubset s является everywherePos.
LaTeX
$$$$ μ.IsEverywherePos( μ.everywherePosSubset s). $$$$
Lean4
/-- In a space with an inner regular measure, the everywhere positive subset of a measurable set
is itself everywhere positive. This is not obvious as `μ.everywherePosSubset s` is defined as
the points whose neighborhoods intersect `s` along positive measure subsets, but this does not
say they also intersect `μ.everywherePosSubset s` along positive measure subsets. -/
theorem isEverywherePos_everywherePosSubset [OpensMeasurableSpace α] [InnerRegular μ] (hs : MeasurableSet s) :
μ.IsEverywherePos (μ.everywherePosSubset s) := by
intro x hx n hn
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 hn with ⟨u, u_mem, hu⟩
have A : 0 < μ (u ∩ s) :=
by
have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem
exact hx.2 _ this
have B : (u ∩ μ.everywherePosSubset s : Set α) =ᵐ[μ] (u ∩ s : Set α) :=
ae_eq_set_inter (ae_eq_refl _) (everywherePosSubset_ae_eq hs)
rw [← B.measure_eq] at A
exact A.trans_le (measure_mono hu)
