toLeft_disjSum

Mathlib.Data.Finset.Sum

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

English

Let s be a finite set of α and t a finite set of β. The left projection of their disjoint sum equals s: (s ⊎ t)^{toLeft} = s.

Русский

Пусть s — конечное множество над α, а t — конечное над β. Левая часть дизъюнктной суммы равна s: (s ⊎ t)^{toLeft} = s.

LaTeX

$$(s \uplus t)^{\mathrm{toLeft}} = s$$

Lean4

@[simp]
theorem toLeft_disjSum : (s.disjSum t).toLeft = s := by ext x; simp

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

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

Разделы

Аффилиация

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