iUnion_left_iff — Mathlib

English

If a family s indexed by ι is pairwise disjoint, then the family of AEDisjoint μ on s is pairwise.

Русский

Если семейство s_i попарно непересекаются, то семейство AEDisjoint μ на s тоже попарно.

LaTeX

$$Set.PairwiseDisjoint aedisjoint$$

Lean4

@[simp]
theorem iUnion_left_iff {ι : Sort*} [Countable ι] {s : ι → Set α} :
    AEDisjoint μ (⋃ i, s i) t ↔ ∀ i, AEDisjoint μ (s i) t := by
  simp only [AEDisjoint, iUnion_inter, measure_iUnion_null_iff]

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