coe_unionEqSigmaOfDisjoint_symm_apply

English

Under the same pairwise disjointness hypothesis, the inverse bijection from the union to the sigma-type satisfies that the β-component extracted by the inverse equals the original element: the second projection recovers the β-component.

Русский

При тех же предпосылках разобщённости обратное биекции отображает элемент объединения обратно в пару (индекс, элемент), и второй компонент этой пары совпадает с исходным элементом β.

LaTeX

$$$((\\operatorname{unionEqSigmaOfDisjoint} h).symm x : \\beta) = x.2$$$

Lean4

@[simp]
theorem coe_unionEqSigmaOfDisjoint_symm_apply {α β : Type*} {t : α → Set β} (h : Pairwise (Disjoint on t))
    (x : (i : α) × t i) : ((Set.unionEqSigmaOfDisjoint h).symm x : β) = x.2 := by rfl

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