English
Bind operation for Set.PairwiseDisjoint over Finsets: a union over a finite family of Finsets preserves pairwise disjointness under f.
Русский
Объединение множества в рамках Set.PairwiseDisjoint сохраняет попарную непересекаемость относительно f.
LaTeX
$$Set.PairwiseDisjoint.biUnion_finset$$
Lean4
/-- Bind operation for `Set.PairwiseDisjoint`. In a complete lattice, you can use
`Set.PairwiseDisjoint.biUnion`. -/
theorem biUnion_finset {s : Set ι'} {g : ι' → Finset ι} {f : ι → α}
(hs : s.PairwiseDisjoint fun i' : ι' => (g i').sup f) (hg : ∀ i ∈ s, (g i : Set ι).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 (by rwa [hcd] at ha) hb hab
· exact (hs hc hd (ne_of_apply_ne _ hcd)).mono (Finset.le_sup ha) (Finset.le_sup hb)
