compares — Mathlib

English

If f is strictly monotone on α, then for all a,b ∈ α and any ordering o, o.Compares (f a) (f b) ↔ o.Compares a b.

Русский

Если f строго монотонна на всем α, то для любых a,b ∈ α и любого порядка o верно: o.Compares(f(a))(f(b)) ⇔ o.Compares(a)(b).

LaTeX

$$$ (hf : StrictMono f) \rightarrow \forall a b : α, \forall o : Ordering, o.Compares (f a) (f b) \leftrightarrow o.Compares a b $$$

Lean4

protected theorem compares (hf : StrictMono f) {a b : α} {o : Ordering} : o.Compares (f a) (f b) ↔ o.Compares a b :=
  (hf.strictMonoOn Set.univ).compares trivial trivial

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