range_snd — Mathlib

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

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