ae_of_forall_measure_lt_top_ae_restrict

English

If μ is σ-finite and for every measurable set s with μ(s) < ∞ we have P almost everywhere on μ.restrict s, then P holds μ-almost everywhere.

Русский

Если μ сигма-конечна и для каждого измеримого s с μ(s)<∞ имеетc P почти всюду на μ.restrict s, то P верно μ-близко ко почти всей мере.

LaTeX

$$$\forall s\, MeasurableSet s\, (μ s < ∞) \implies (P \text{ a.e. on } μ\restriction s) \Rightarrow (P \text{ a.e. on } μ)$$$

Lean4

/-- To prove something for almost all `x` w.r.t. a σ-finite measure, it is sufficient to show that
  this holds almost everywhere in sets where the measure has finite value. -/
theorem ae_of_forall_measure_lt_top_ae_restrict {μ : Measure α} [SigmaFinite μ] (P : α → Prop)
    (h : ∀ s, MeasurableSet s → μ s < ∞ → ∀ᵐ x ∂μ.restrict s, P x) : ∀ᵐ x ∂μ, P x :=
  ae_of_forall_measure_lt_top_ae_restrict' μ P fun s hs h2s _ => h s hs h2s

Похожие утверждения