toLeft_disjSum_toRight — Mathlib

English

For any finite set u of α ⊕ β, taking its left and right projections and forming their disjoint sum yields the original set: toLeft(u) ⊎ toRight(u) = u.

Русский

Для любого конечного множества u ⊆ α ⊕ β, взяв его левую и правую проекции и сложив их дизъюнктивно, восстанавливаем исходное множество: toLeft(u) ⊎ toRight(u) = u.

LaTeX

$$$ u.toLeft \uplus u.toRight = u $$$

Lean4

theorem toLeft_disjSum_toRight : u.toLeft.disjSum u.toRight = u := by ext (x | x) <;> simp

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