English
Let α and β be finite types. The image of the universal Finset under the right injection i ↦ inr i equals the universal Finset of β; equivalently, every element of β appears as the right component of some element of α ⊕ β.
Русский
Пусть α и β — конечные множества. Образ всеобщего множества по правому включению i ↦ inr i совпадает с всеобъемлющим множеством β; то есть каждая точка β появляется как правая часть некоторого элемента из α ⊕ β.
LaTeX
$$$$\\operatorname{image}(\\mathrm{Sum.inr})\\,\\operatorname{univ} = \\operatorname{univ}.$$$
Lean4
@[simp]
theorem toRight_univ : (univ : Finset (α ⊕ β)).toRight = univ := by ext; simp
