toRight_insert_inr — Mathlib

English

For any finite set u of α ⊕ β and any b ∈ β, inserting inr b into u yields toRight equal to inserting b into the right projection: (insert (inr b) u).toRight = insert b u.toRight.

Русский

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

LaTeX

$$$ (\\mathrm{insert}(\\mathrm{inr} b) u).toRight = \\mathrm{insert} b \\, u.toRight $$$

Lean4

@[simp]
theorem toRight_insert_inr : (insert (inr b) u).toRight = insert b u.toRight := by ext y; simp

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