biInter_Ici_aecover — Mathlib

English

If hφ is an ae-cover along atTop, then the family n ↦ ⋂ k∈Ici n φ(k) is also an ae-cover along atTop.

Русский

Если $hφ$ является ae-покрытием вдоль atTop, то пересечение $⋂_{k∈Ici n} φ(k)$ образует ae-покрытие вдоль atTop.

LaTeX

$$$\\forall hφ : MeasureTheory.AECover μ atTop φ,\\ MeasureTheory.AECover μ atTop (\\lambda n, ⋂ (k) (_h : k \\in Ici n), φ k)$$$

Lean4

theorem biInter_Ici_aecover [Preorder ι] {φ : ι → Set α} (hφ : AECover μ atTop φ) :
    AECover μ atTop fun n : ι => ⋂ (k) (_h : k ∈ Ici n), φ k
    where
  ae_eventually_mem :=
    hφ.ae_eventually_mem.mono fun x h ↦ by simpa only [mem_iInter, mem_Ici, eventually_forall_ge_atTop]
  measurableSet _ := .biInter (to_countable _) fun n _ => hφ.measurableSet n

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