strictMono — Mathlib

English

If α is a subsingleton, then any function f: α → β is strictly monotone; that is, if x < y then f(x) < f(y).

Русский

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

LaTeX

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

Lean4

protected theorem strictMono [Subsingleton α] (f : α → β) : StrictMono f := fun _ _ h ↦
  (h.ne <| Subsingleton.elim _ _).elim

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