sorted_gt_listMap — Mathlib

English

Let f be strictly antitone. Then (l.map f).Sorted(>) iff l.Sorted(<).

Русский

Пусть f — строго антимонотонная. Тогда (l.map f).Sorted(>) эквивалентно l.Sorted(<).

LaTeX

$$$$ \forall l:\mathrm{List}(\alpha),\; \mathrm{StrictAnti}(f) \Rightarrow ((\mathrm{List.map}\ f\ l).Sorted(>) \iff l.Sorted(<)). $$$$

Lean4

theorem sorted_gt_listMap (hf : StrictAnti f) : (l.map f).Sorted (· > ·) ↔ l.Sorted (· < ·) :=
  hf.dual_right.sorted_lt_listMap

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