sorted_lt_listMap — Mathlib

English

Let f be strictly increasing. For any list l, the image list (l.map f) is strictly increasing with respect to < iff l is strictly increasing with respect to <.

Русский

Пусть f строго возрастает. Для любого списка l образованный списком (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_lt_listMap (hf : StrictMono f) : (l.map f).Sorted (· < ·) ↔ l.Sorted (· < ·) :=
  (OrderEmbedding.ofStrictMono f hf).sorted_lt_listMap

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