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