Commit 2025-10-31 09:48 00fcea5e

feat: biUnion_inter_of_pairwise_disjoint (#31063) A basic order/set lemma: given a family f of pairwise disjoint sets, one has ⋃ i ∈ (s ∩ t), f i = (⋃ i ∈ s, f i) ∩ (⋃ i ∈ t, f i). Prompted by #30109