cmp_map_eq — Mathlib

English

If f is strictly monotone on S, then for x,y ∈ S, the comparison of f(x) and f(y) is the same as the comparison of x and y, i.e., cmp(f(x), f(y)) = cmp(x, y).

Русский

Если f строго монотонна на S, то для любых x,y ∈ S сравнение f(x) и f(y) совпадает с сравнением x и y: cmp(f(x), f(y)) = cmp(x, y).

LaTeX

$$$ (hf : StrictMonoOn f s) → \forall x ∈ s, \forall y ∈ s, Eq (cmp (f x) (f y)) (cmp x y) $$$

Lean4

theorem cmp_map_eq (hf : StrictMonoOn f s) (hx : x ∈ s) (hy : y ∈ s) : cmp (f x) (f y) = cmp x y :=
  ((hf.compares hx hy).2 (cmp_compares x y)).cmp_eq

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