aecover_restrict_of_ae_imp — Mathlib

English

If s is measurable, and for μ-almost every x in s we have x ∈ φ_n eventually along l, and each φ_n is measurable, then μ.restrict s is covered by φ along l.

Русский

Если s измеримо и для μ-почти всякого x ∈ s имеется, что x принадлежит φ_n не позднее along l, и каждый φ_n измерим, то ограничение μ на s образует покрытие φ вдоль l.

LaTeX

$$$\text{MeasurableSet } s \land (\forallᵐ x \partial μ, x ∈ s \to \forall^\! n \in l, x ∈ φ(n)) \land (\forall n, \text{MeasurableSet } φ(n)) \Rightarrow \mathrm{AECover}(μ\restriction s, l, φ).$$$

Lean4

theorem aecover_restrict_of_ae_imp {s : Set α} {φ : ι → Set α} (hs : MeasurableSet s)
    (ae_eventually_mem : ∀ᵐ x ∂μ, x ∈ s → ∀ᶠ n in l, x ∈ φ n) (measurable : ∀ n, MeasurableSet <| φ n) :
    AECover (μ.restrict s) l φ where
  ae_eventually_mem := by rwa [ae_restrict_iff' hs]
  measurableSet := measurable

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