toRight_cons_inr — Mathlib

English

Right projection after adding a right element via cons(inr b) updates the right projection and adds b to its right: (cons (inr b) u hb).toRight = cons b u.toRight.

Русский

Правая проекция после добавления элемента справа через cons(inr b) изменяет правую проекцию и добавляет b к ней: (cons (inr b) u hb).toRight = cons b u.toRight.

LaTeX

$$(\mathrm{cons} (\mathrm{inr} b) \, u \, hb)^{\mathrm{toRight}} = \mathrm{cons}(b, u^{\mathrm{toRight}})$$

Lean4

@[simp]
theorem toRight_cons_inr (hb) : (cons (inr b) u hb).toRight = cons b u.toRight (by simpa) := by ext y; simp

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