sorted_gt_listMap — Mathlib

English

If f is strictly increasing, then (l.map f) is sorted by > iff l is sorted by >.

Русский

Если f строго возрастает, то (l.map f) упорядочен по > тогда и только тогда, когда l упорядочен по >.

LaTeX

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

Lean4

theorem sorted_gt_listMap (hf : StrictMono f) : (l.map f).Sorted (· > ·) ↔ l.Sorted (· > ·) :=
  (OrderEmbedding.ofStrictMono f hf).sorted_gt_listMap

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