English
Let α be linearly ordered, β a preorder, and f: α → β strictly increasing. For every finite list l of elements of α, applying f to each element and then sorting by ≤ yields a list that is sorted if and only if the original list is sorted by ≤.
Русский
Пусть α упорядочено по линейному порядку, β — ограниченно частично упорядоченное, и f: α → β строго возрастает. Для любого конечного списка l над α применение f к каждому элементу и последующая сортировка по ≤ дают список, упорядованный по ≤ тогда и только тогда, когда исходный список l упорядочен по ≤.
LaTeX
$$$$ \forall l:\mathrm{List}(\alpha),\; \mathrm{StrictMono}(f) \Rightarrow \big( (\mathrm{List.map}\ f\ l).Sorted(\le) \iff l.Sorted(\le) \big). $$$$
Lean4
theorem sorted_le_listMap (hf : StrictMono f) : (l.map f).Sorted (· ≤ ·) ↔ l.Sorted (· ≤ ·) :=
(OrderEmbedding.ofStrictMono f hf).sorted_listMap
