English
For disjoint families, the difference of unions equals the union over the difference of index sets.
Русский
Для попарно непересекающихся семейств равенство разности объединений утверждает: ⋃ i∈s f i \ ⋃ i∈t f i = ⋃ i∈s\t f i.
LaTeX
$$$$\big(\bigcup_{i\in s} f_i\big) \setminus \big(\bigcup_{i\in t} f_i\big) = \big\bigcup_{i\in s\setminus t} f_i. $$$$
Lean4
/-- Bind operation for `Set.PairwiseDisjoint`. If you want to only consider finsets of indices, you
can use `Set.PairwiseDisjoint.biUnion_finset`. -/
theorem biUnion {s : Set ι'} {g : ι' → Set ι} {f : ι → α} (hs : s.PairwiseDisjoint fun i' : ι' => ⨆ i ∈ g i', f i)
(hg : ∀ i ∈ s, (g i).PairwiseDisjoint f) : (⋃ i ∈ s, g i).PairwiseDisjoint f :=
by
rintro a ha b hb hab
simp_rw [Set.mem_iUnion] at ha hb
obtain ⟨c, hc, ha⟩ := ha
obtain ⟨d, hd, hb⟩ := hb
obtain hcd | hcd := eq_or_ne (g c) (g d)
· exact hg d hd (hcd ▸ ha) hb hab
·
exact
(hs hc hd <| ne_of_apply_ne _ hcd).mono (le_iSup₂ (f := fun i _ => f i) a ha)
(le_iSup₂ (f := fun i _ => f i) b hb)
