monotone' — Mathlib

English

If β is a subsingleton, then every map f: α → β is monotone; this holds regardless of the domain α and codomain β as long as β has at most one element.

Русский

Если β является однозначным, тогда любая функция f: α → β монотонна; это справедливо независимо от области определения α и области значений β, если в β не более одного элемента.

LaTeX

$$$ (\\forall x,y : \\beta,\\ x = y) \\Rightarrow (\\forall f : \\alpha \\to \\beta, \\forall x,y : \\alpha,\\ x \\le y \\to f x \\le f y)$$$

Lean4

theorem monotone' [Subsingleton β] (f : α → β) : Monotone f := fun _ _ _ ↦ (Subsingleton.elim _ _).le

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