orderHom_eq_id — Mathlib

English

If α is a preorder with a single element (subsingleton), then every order-preserving map g: α → α is the identity map.

Русский

Если множество α состоит из одного элемента и упорядочено, тогда любой монотонный отображение g: α → α является тождественным отображением.

LaTeX

$$$[\\text{Subsingleton } \\alpha]\\ (g:\\alpha \\too \\alpha)\\Rightarrow g = \\mathrm{OrderHom.id}_\\alpha$.$$

Lean4

theorem orderHom_eq_id [Subsingleton α] (g : α →o α) : g = OrderHom.id :=
  Subsingleton.elim _ _

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