surjOn_of_subsingleton — Mathlib

English

If α is a subsingleton, then any map f: α → α is surjective on any subset s ⊆ α onto s.

Русский

Если α — подмножество, тогда любая функция f: α→α сюръективна на любом подмножестве s ⊆ α на s.

LaTeX

$$$ [\text{Subsingleton } \alpha] (f: \alpha \to \alpha) (s: Set \alpha) : \mathrm{SurjOn} f s s $$$

Lean4

theorem surjOn_of_subsingleton [Subsingleton α] (f : α → α) (s : Set α) : SurjOn f s s :=
  surjOn_of_subsingleton' _ id

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