union_left_iff — Mathlib

English

For aCountable index set, the AEDisjoint of s with a union on the right is equivalent to AEDisjoint with each component.

Русский

Для счётного iUnion справа AEDisjoint μ s (⋃ i t_i) эквивалентно ∀ i, AEDisjoint μ s (t_i).

LaTeX

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

Lean4

@[simp]
theorem union_left_iff : AEDisjoint μ (s ∪ t) u ↔ AEDisjoint μ s u ∧ AEDisjoint μ t u := by
  simp [union_eq_iUnion, and_comm]

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