sorted_lt_listMap — Mathlib

English

For an OrderEmbedding e: α ↪o β and any list l, the map (l.map e) is sorted by < iff l is sorted by <.

Русский

Для отображения порядка e: α ↪o β и любого списка l отображение (l.map e) по < упорядочено тогда и только тогда, когда сам список l упорядочен по <.

LaTeX

$$$$ (l.map e).Sorted (\lt) \iff l.Sorted (\lt). $$$$

Lean4

@[simp]
theorem sorted_lt_listMap (e : α ↪o β) {l : List α} : (l.map e).Sorted (· < ·) ↔ l.Sorted (· < ·) :=
  e.ltEmbedding.sorted_listMap

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