union_symm_inl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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