sorted_le_listMap — Mathlib

English

Let f be strictly antitone (order-reversing). 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(\le) \iff l.Sorted(\ge)). $$$$

Lean4

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

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