union_symm_inr — Mathlib

English

The right-injected element under the union equivalence matches the corresponding right member.

Русский

Правый элемент, вложенный через объединение, сопоставляется правому члену пары.

LaTeX

$$$ (h : \\\\mathrm{Disjoint} s t) (y : t) : \\\\mathrm{Equiv.Finset.union} s t h (\\\\mathrm{Sum.inr} y) = \\\\langle y, \\\\mathrm{Finset.mem_union}\\\\.mpr \\\\left| \\\\mathrm{Or.inr} y.2\\\\right.\\\\rangle$$$

Lean4

@[simp]
theorem union_symm_inr (h : Disjoint s t) (y : t) :
    Equiv.Finset.union s t h (Sum.inr y) = ⟨y, Finset.mem_union.mpr <| Or.inr y.2⟩ :=
  rfl

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