biUnion_Iic_aecover — Mathlib

English

If hφ is an ae-cover along atTop, then the family defined by n ↦ ⋃ k∈Iic n φ(k) is also an ae-cover along atTop.

Русский

Если $hφ$ является ae-покрытием вдоль atTop, тогда семейство $n \mapsto \bigcup_{k \\in IIC(n)} φ(k)$ тоже является ae-покрытием вдоль atTop.

LaTeX

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

Lean4

theorem biUnion_Iic_aecover [Preorder ι] {φ : ι → Set α} (hφ : AECover μ atTop φ) :
    AECover μ atTop fun n : ι => ⋃ (k) (_h : k ∈ Iic n), φ k :=
  hφ.superset (fun _ ↦ subset_biUnion_of_mem right_mem_Iic) fun _ ↦ .biUnion (to_countable _) fun _ _ ↦ (hφ.2 _)

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