biUnionEqSigmaOfDisjoint — Mathlib

English

If s is pairwise disjoint with respect to f, then the equality of bounded unions with the sigma-type decomposition holds.

Русский

Если s попарно непересекается по f, тогда тождество между ограниченным объединением и разложением по сигма-типу выполняется.

LaTeX

$$$$\forall h : s.PAIRWISE_DISJOINT f, \; (⋃ i ∈ s, f i) \equiv \Sigma i : s, f i.$$$$

Lean4

/-- Equivalence between a disjoint bounded union and a dependent sum. -/
noncomputable def biUnionEqSigmaOfDisjoint {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f) :
    (⋃ i ∈ s, f i) ≃ Σ i : s, f i :=
  (Equiv.setCongr (biUnion_eq_iUnion _ _)).trans <|
    unionEqSigmaOfDisjoint fun ⟨_i, hi⟩ ⟨_j, hj⟩ ne => h hi hj fun eq => ne <| Subtype.eq eq

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