English
For any finite set u of α ⊕ β, toRight(u) consists exactly of those elements b ∈ β for which inr(b) ∈ u.
Русский
Для конечного множества u ⊆ α ⊕ β проекция toRight(u) содержит ровно те элементы b ∈ β, для которых inr(b) принадлежит u.
LaTeX
$$$ b \in \mathrm{toRight}(u) \iff \mathrm{inr}(b) \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 right input.
See also `List.partitionMap`.
-/
def toRight (u : Finset (α ⊕ β)) : Finset β :=
u.filterMap (Sum.elim (fun _ => none) some) (by clear x; aesop)
