antitone — Mathlib

English

If α is a preorder with at most one element, then every map f: α → β is antitone; that is, for all x, y ∈ α, x ≤ y implies f(y) ≤ f(x).

Русский

Если α является предпредметом с не более чем одним элементом, то любая функция f: α → β антитонна: для всех x, y ∈ α, если x ≤ y, то f(y) ≤ f(x).

LaTeX

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

Lean4

protected theorem antitone [Subsingleton α] (f : α → β) : Antitone f := fun _ _ _ ↦
  (congr_arg _ <| Subsingleton.elim _ _).le

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