sorted_ge_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(\ge) \iff l.Sorted(\le)). $$$$

Lean4

theorem sorted_ge_listMap (hf : StrictAnti f) : (l.map f).Sorted (· ≥ ·) ↔ l.Sorted (· ≤ ·) :=
  hf.dual_right.sorted_le_listMap

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