coe_snd_biUnionEqSigmaOfDisjoint — Mathlib

English

The second projection of the biUnionEqSigmaOfDisjoint is the identity map on the union, when restricted appropriately.

Русский

Второй проекцией biUnionEqSigmaOfDisjoint является тождественное отображение на объединении, при соответствующем ограничении.

LaTeX

$$$$ ((Set.biUnionEqSigmaOfDisjoint h).snd : \alpha) = x $$$$

Lean4

@[simp]
theorem coe_snd_biUnionEqSigmaOfDisjoint {α ι : Type*} {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f)
    (x : ⋃ i ∈ s, f i) : ((Set.biUnionEqSigmaOfDisjoint h x).snd : α) = x := by simp [biUnionEqSigmaOfDisjoint]

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