English
There exists a surjective function f: α → β if and only if there exists a nonempty function α → β and a nonempty embedding β ↪ α.
Русский
Существует сюръективная функция f: α → β тогда и только тогда, когда существует непустая функция α → β и непустое вложение β ↪ α.
LaTeX
$$$\big(\exists f:\, \alpha \to \beta,\text{Surjective}(f)\big) \iff \big(\exists h:\, \alpha \to \beta,\operatorname{Nonempty}(\alpha \to \beta)\wedge \operatorname{Nonempty}(\beta \hookrightarrow \alpha)\big)$$$
Lean4
theorem exists_surjective_iff {α β : Sort*} : (∃ f : α → β, Surjective f) ↔ Nonempty (α → β) ∧ Nonempty (β ↪ α) :=
⟨fun ⟨f, h⟩ ↦ ⟨⟨f⟩, ⟨⟨_, injective_surjInv h⟩⟩⟩, fun ⟨h, ⟨e⟩⟩ ↦
(nonempty_fun.mp h).elim (fun _ ↦ ⟨isEmptyElim, (isEmptyElim <| e ·)⟩) fun _ ↦ ⟨_, invFun_surjective e.inj'⟩⟩
