Projection_is_Surjection
Provedprojectionsproofwikisurjections
Let S and T be non-empty sets. Then the first and second projections on S × T are both surjections.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Projection_is_Surjection {α β : Type _} [Nonempty α] [Nonempty β] : Function.Surjective (Prod.fst : α × β → α) ∧ Function.Surjective (Prod.snd : α × β → β) := by sorrySource