coe_snd_unionEqSigmaOfDisjoint — Mathlib

English

Again, under pairwise disjointness, the inverse bijection satisfies that projecting to the β-component yields the original element of the union, i.e., the second coordinate matches.

Русский

Снова при условии попарной дизъюнктности обратная биекция переносит элемент из объединения в пару так, что второй компонент равен этому элементу.

LaTeX

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

Lean4

@[simp]
theorem coe_snd_unionEqSigmaOfDisjoint {α β : Type*} {t : α → Set β} (h : Pairwise (Disjoint on t))
    (x : ⋃ (i : α), t i) : ((Set.unionEqSigmaOfDisjoint h x).snd : β) = x :=
  by
  conv => right; rw [← unionEqSigmaOfDisjoint h |>.symm_apply_apply x]
  rfl

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