English
For any finite set u of α ⊕ β, toLeft(u) consists exactly of those elements a ∈ α for which inl(a) ∈ u.
Русский
Для конечного множества u ⊆ α ⊕ β проекция toLeft(u) содержит ровно те элементы a ∈ α, для которых inl(a) принадлежит u.
LaTeX
$$$ a \in \mathrm{toLeft}(u) \iff \mathrm{inl}(a) \in u $$$
Lean4
/-- Given a finset of elements `α ⊕ β`, extract all the elements of the form `α`. This
forms a quasi-inverse to `disjSum`, in that it recovers its left input.
See also `List.partitionMap`.
-/
def toLeft (u : Finset (α ⊕ β)) : Finset α :=
u.filterMap (Sum.elim some fun _ => none) (by clear x; aesop)
