coe_biUnionEqSigmaOfDisjoint_symm_apply

English

The symmetry of the biUnion-sigma equivalence holds, with the left/right projections corresponding to the σ-structure.

Русский

Симметрия эквивалентности biUnion–sigma сохраняется: проекции соответствуют сигма-структуре.

LaTeX

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

Lean4

@[simp]
theorem coe_biUnionEqSigmaOfDisjoint_symm_apply {α ι : Type*} {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f)
    (x : (i : s) × f i) : ((Set.biUnionEqSigmaOfDisjoint h).symm x : α) = x.2 := by rfl

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