toRight_insert_inl — Mathlib

English

For any finite set u of elements of α ⊕ β and any a ∈ α, inserting inl a into u does not change the right projection of the set: (insert (inl a) u).toRight = u.toRight.

Русский

Для любого конечного множества u элементов типа α ⊕ β и любого a ∈ α вставка inl a в u не меняет правую часть множества: (insert (inl a) u).toRight = u.toRight.

LaTeX

$$$ (\\mathrm{insert}(\\mathrm{inl} a) u).toRight = u.toRight $$$

Lean4

@[simp]
theorem toRight_insert_inl : (insert (inl a) u).toRight = u.toRight := by ext y; simp

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