sorted_ge_listMap — Mathlib

English

Let α be linearly ordered, f strictly monotone, l a list; then (l.map f) is sorted by ≥ if and only if l is sorted by ≥.

Русский

Пусть α упорядочено по линейному порядку, f строго монотонна, и l — список; тогда (l.map f) упорядочен по ≥ тогда и только тогда, когда сам список l упорядочен по ≥.

LaTeX

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

Lean4

theorem sorted_ge_listMap (hf : StrictMono f) : (l.map f).Sorted (· ≥ ·) ↔ l.Sorted (· ≥ ·) :=
  (OrderEmbedding.ofStrictMono f hf).sorted_swap_listMap

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