English
In a space with inner regular measure for finite sets, the everywhere-positive subset of a finite-measure measurable set is itself everywhere positive.
Русский
В пространстве с внутренней регулярностью меры для конечных множеств, everywhere-positive подмножество конечномерного измеримого множества является самим everywhere positive.
LaTeX
$$$$ \\text{If } μ(s) < ∞ \\text{ and } s \\text{ is measurable, then } μ.IsEverywherePos( μ.everywherePosSubset s). $$$$
Lean4
/-- In a space with an inner regular measure for finite measure sets, the everywhere positive subset
of a measurable set of finite measure 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_of_measure_ne_top [OpensMeasurableSpace α] [InnerRegularCompactLTTop μ]
(hs : MeasurableSet s) (h's : μ 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_of_measure_ne_top hs h's)
rw [← B.measure_eq] at A
exact A.trans_le (measure_mono hu)
