English
For σ-finite μ and ν, if for every measurable set s with μ(s) < ∞ and ν(s) < ∞ we have P almost everywhere on μ.restrict s, then P holds almost everywhere on μ.
Русский
Для σ-конечных μ и ν, если для каждого измеримого множества s с μ(s)<∞ и ν(s)<∞ верно P почти всюду на μ ограниченном s, то P верно почти всюду на μ.
LaTeX
$$$\forall s\, (MeasurableSet\ s)\ (μ s < ∞)\ (ν s < ∞) \Rightarrow (P \text{ a.e. on } μ\restriction s) \implies (P \text{ a.e. on } μ)$$$
Lean4
/-- Similar to `ae_of_forall_measure_lt_top_ae_restrict`, but where you additionally get the
hypothesis that another σ-finite measure has finite values on `s`. -/
theorem ae_of_forall_measure_lt_top_ae_restrict' {μ : Measure α} (ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
(P : α → Prop) (h : ∀ s, MeasurableSet s → μ s < ∞ → ν s < ∞ → ∀ᵐ x ∂μ.restrict s, P x) : ∀ᵐ x ∂μ, P x :=
by
have : ∀ n, ∀ᵐ x ∂μ, x ∈ spanningSets (μ + ν) n → P x :=
by
intro n
have :=
h (spanningSets (μ + ν) n) (measurableSet_spanningSets _ _)
((self_le_add_right _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
((self_le_add_left _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
exact (ae_restrict_iff' (measurableSet_spanningSets _ _)).mp this
filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)
