toLeft_insert_inr

Mathlib.Data.Finset.Sum

URI: https://scilib.ai/kg/mathlib#Finset.toLeft_insert_inr

English

Left projection of inserting a right element leaves the left projection unchanged: toLeft(insert(inr b) u) = toLeft u.

Русский

Левая проекция при вставке справа не меняется: toLeft(insert(inr b) u) = toLeft u.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru