ae_restrict_biUnion_eq — Mathlib

English

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

Русский

Пусть s_i — семейство множеств, t — счётное множество индексов. Тогда условие почти всюду на biUnion эквивалентно для каждого i в t отдельно.

LaTeX

$$$\\bigl(\\forallᵐ x \\partial μ.restrict (\\bigcup_{i \\in t} s_i), p(x)\\bigr) \\iff \\forall i \\in t, \\forallᵐ x \\partial μ.restrict (s_i), p(x).$$$

Lean4

theorem ae_restrict_biUnion_eq (s : ι → Set α) {t : Set ι} (ht : t.Countable) :
    ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i)) :=
  by
  haveI := ht.to_subtype
  rw [biUnion_eq_iUnion, ae_restrict_iUnion_eq, ← iSup_subtype'']

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