ae_restrict_iUnion_iff — Mathlib

English

Let s_i be a countable family. Then (∀ᵐ x ∂μ.restrict (⋃ i, s_i), p x) iff ∀ i, ∀ᵐ x ∂μ.restrict (s_i), p x.

Русский

Пусть s_i образуют счётное семейство. Тогда условие a.e. на iUnion эквивалентно для каждого i отдельно.

LaTeX

$$$(\\forallᵐ x ∂μ.restrict (\\bigcup_i s_i), p x) \\iff \\forall i, \\forallᵐ x ∂μ.restrict (s_i), p x$.$$

Lean4

theorem ae_restrict_iUnion_iff [Countable ι] (s : ι → Set α) (p : α → Prop) :
    (∀ᵐ x ∂μ.restrict (⋃ i, s i), p x) ↔ ∀ i, ∀ᵐ x ∂μ.restrict (s i), p x := by simp

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