toLeft_cons_inr — Mathlib

English

Left projection after adding a new right element does not change: (cons (inr b) u hb).toLeft = u.toLeft.

Русский

Левая проекция после добавления нового правого элемента не меняется: (cons (inr b) u hb).toLeft = u.toLeft.

LaTeX

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

Lean4

@[simp]
theorem toLeft_cons_inr (hb) : (cons (inr b) u hb).toLeft = u.toLeft := by ext y; simp

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