ae_restrict_biUnion_iff — Mathlib

English

For a countable index family, the a.e. equality μ.restrict (⋃ i ∈ t, s_i) ≡ ∀ i ∈ t, μ.restrict (s_i) almost everywhere.

Русский

Для счётной связки индексов равенство a.e. между ограничением объединения и ограничениями по каждому элементу эквивалентно.

LaTeX

$$$f =ᵐ[μ.restrict (\\bigcup_{i∈t} s_i)] g \\iff \\forall i∈t, f =ᵐ[μ.restrict (s_i)] g$.$$

Lean4

theorem ae_restrict_biUnion_iff (s : ι → Set α) {t : Set ι} (ht : t.Countable) (p : α → Prop) :
    (∀ᵐ x ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ x ∂μ.restrict (s i), p x := by
  simp_rw [Filter.Eventually, ae_restrict_biUnion_eq s ht, mem_iSup]

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