toRight_cons_inl — Mathlib

English

Left projection after adding a left element via cons(inl a) remains truthfully adjusted on the right: (cons (inl a) u ha).toRight = u.toRight.

Русский

Левая проекция после добавления элемента слева через cons(inl a) сохраняет правую проекцию: (cons (inl a) u ha).toRight = u.toRight.

LaTeX

$$(\mathrm{cons} (\mathrm{inl} a) \, u \, ha)^{\mathrm{toRight}} = u^{\mathrm{toRight}}$$

Lean4

@[simp]
theorem toRight_cons_inl (ha) : (cons (inl a) u ha).toRight = u.toRight := by ext y; simp

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