cmp_map_eq — Mathlib

English

If hf is StrictAntiOn on S, then for x,y ∈ S, cmp(f x)(f y) = cmp y x.

Русский

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

LaTeX

$$$ (hf : StrictAntiOn f s) \rightarrow Set.instMembership.mem s x \rightarrow Set.instMembership.mem s y \rightarrow Eq (cmp (f x) (f y)) (cmp y x) $$$

Lean4

theorem cmp_map_eq (hf : StrictAntiOn f s) (hx : x ∈ s) (hy : y ∈ s) : cmp (f x) (f y) = cmp y x :=
  hf.dual_right.cmp_map_eq hy hx

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