English
If each restricted measure μ|s_n is inner regular with respect to p and measurable sets, and the s_n cover the space in a monotone way, then μ is inner regular.
Русский
Если по частям каждое ограничение меры μ|s_n имеет внутреннюю регулярность по p и измеримым множествам, и эти s_n образуют покрытие пространства монотоном образом, то и μ имеет внутреннюю регулярность.
LaTeX
$$$(\forall n, InnerRegularWRT(μ|s_n)\ p\ MeasurableSet) \Rightarrow (univ ⊆ ⋃ n\; s_n) \to (Monotone\ s) \Rightarrow InnerRegularWRT(μ; p; MeasurableSet).$$$
Lean4
/-- If the restrictions of a measure to a monotone sequence of sets covering the space are
inner regular for some property `p` and all measurable sets, then the measure itself is
inner regular. -/
theorem of_restrict {μ : Measure α} {s : ℕ → Set α} (h : ∀ n, InnerRegularWRT (μ.restrict (s n)) p MeasurableSet)
(hs : univ ⊆ ⋃ n, s n) (hmono : Monotone s) : InnerRegularWRT μ p MeasurableSet :=
by
intro F hF r hr
have hBU : ⋃ n, F ∩ s n = F := by rw [← inter_iUnion, univ_subset_iff.mp hs, inter_univ]
have : μ F = ⨆ n, μ (F ∩ s n) := by rw [← (monotone_const.inter hmono).measure_iUnion, hBU]
rw [this] at hr
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
rw [← restrict_apply hF] at hn
rcases h n hF _ hn with ⟨K, KF, hKp, hK⟩
exact ⟨K, KF, hKp, hK.trans_le (restrict_apply_le _ _)⟩
