iUnion_right_iff — Mathlib

English

For aCountable index set, the AEDisjoint of a union on the left with t is equivalent to AEDisjoint for each component.

Русский

Для счётного индекса iUnion слева AEDisjoint μ (⋃ i s_i) t эквивалентно ∀ i, AEDisjoint μ (s_i) t.

LaTeX

$$AEDisjoint μ (⋃ i, s i) t ↔ ∀ i, AEDisjoint μ (s i) t$$

Lean4

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

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