English
For any nonempty α, the range of the second projection Prod.snd on α × β is the whole β.
Русский
Для любого ненулевого α диапазон проекции snd на α × β совпадает с полным множеством β.
LaTeX
$$$ [\\text{Nonempty }\\alpha] \\Rightarrow \\mathrm{range}(\\mathrm{Prod.snd}) = \\mathrm{univ}. $$$
Lean4
@[simp]
theorem _root_.Prod.range_snd [Nonempty α] : range (Prod.snd : α × β → β) = univ :=
Prod.snd_surjective.range_eq