toLeft_cons_inl — Mathlib

English

Left projection after adding a new left element: (cons (inl a) u ha).toLeft = cons a (u.toLeft) (proof).

Русский

Левая проекция после добавления нового левого элемента: (cons (inl a) u ha).toLeft = cons a (u.toLeft) (доказательство).

LaTeX

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

Lean4

@[simp]
theorem toLeft_cons_inl (ha) : (cons (inl a) u ha).toLeft = cons a u.toLeft (by simpa) := by ext y; simp

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