range_fst — Mathlib

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

Похожие утверждения