surjective_to_subsingleton — Mathlib

English

From a nonempty domain to a subsingleton codomain, any function is surjective.

Русский

Из ненулевого домена в одноэлементный кодомон любой отображение сюръективно.

LaTeX

$$$ [\mathrm{na} : Nonempty \; \alpha] [\mathrm{Subsingleton} \; \beta] (f : \alpha \to \beta) : \mathrm{Surjective} f $$$

Lean4

theorem surjective_to_subsingleton [na : Nonempty α] [Subsingleton β] (f : α → β) : Surjective f := fun _ ↦
  let ⟨a⟩ := na;
  ⟨a, Subsingleton.elim _ _⟩

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