English
If the domain α is a preorder with at most one element (a subsingleton), then every map f: α → β into a preorder β is monotone; in particular, for all x, y ∈ α we have x ≤ y imply f(x) ≤ f(y).
Русский
Если область определения α является предпорядком с не более чем одним элементом (однозначный тип), то любая функция f: α → β в предпорядке β монотонна; то есть для всех x, y ∈ α выполняется x ≤ y ⇒ f(x) ≤ f(y).
LaTeX
$$$ (\\forall x,y : \\alpha,\\ x = y) \\Rightarrow (\\forall f : \\alpha \\to \\beta, \\forall x,y : \\alpha,\\ x \\le y \\to f x \\le f y)$$$
Lean4
protected theorem monotone [Subsingleton α] (f : α → β) : Monotone f := fun _ _ _ ↦
(congr_arg _ <| Subsingleton.elim _ _).le
