English
For a sigma-finite measure, any measurable set can be approximated from inside by a measurable set of finite measure.
Русский
Для сигма-ограниченной меры любое измеримое множество можно аппроксимировать изнутри измеримым множеством конечной меры.
LaTeX
$$$[\SigmaFinite(\mu)] \Rightarrow InnerRegularWRT(\mu; (s \mapsto MeasurableSet s \land μ s \neq ∞); (s \mapsto MeasurableSet s)).$$$
Lean4
/-- Given a σ-finite measure, any measurable set can be approximated from inside by a measurable
set of finite measure. -/
theorem of_sigmaFinite [SigmaFinite μ] :
InnerRegularWRT μ (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) (fun s ↦ MeasurableSet s) :=
by
intro s hs r hr
set B : ℕ → Set α := spanningSets μ
have hBU : ⋃ n, s ∩ B n = s := by rw [← inter_iUnion, iUnion_spanningSets, inter_univ]
have : μ s = ⨆ n, μ (s ∩ B n) := by rw [← (monotone_const.inter (monotone_spanningSets μ)).measure_iUnion, hBU]
rw [this] at hr
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
refine ⟨s ∩ B n, inter_subset_left, ⟨hs.inter (measurableSet_spanningSets μ n), ?_⟩, hn⟩
exact ((measure_mono inter_subset_right).trans_lt (measure_spanningSets_lt_top μ n)).ne
