antitone' — Mathlib

English

If β is a subsingleton, then every map f: α → β is antitone; i.e., ∀ x,y ∈ α, x ≤ y implies f(y) ≤ f(x).

Русский

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

LaTeX

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

Lean4

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

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