biUnion_diff_biUnion_eq — Mathlib

English

Disjoint bounded unions correspond to a dependent sum over a disjoint family.

Русский

Разделимые ограниченные объединения соответствуют зависимой сумме над попарно непересекающимся семейством.

LaTeX

$$$$\text{biUnionEqSigmaOfDisjoint } (h: s.PairwiseDisjoint f) : (⋃ i ∈ s, f i) ≃ Σ i : s, f i.$$$$

Lean4

theorem biUnion_diff_biUnion_eq {s t : Set ι} {f : ι → Set α} (h : (s ∪ t).PairwiseDisjoint f) :
    ((⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i) = ⋃ i ∈ s \ t, f i :=
  by
  refine
    (biUnion_diff_biUnion_subset f s t).antisymm
      (iUnion₂_subset fun i hi a ha => (mem_diff _).2 ⟨mem_biUnion hi.1 ha, ?_⟩)
  rw [mem_iUnion₂]; rintro ⟨j, hj, haj⟩
  exact (h (Or.inl hi.1) (Or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩

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