sorted_listMap — Mathlib

English

For any RelEmbedding e: ra ↪r rb and any list l, (l.map e) is rb-sorted iff l is ra-sorted.

Русский

Для любого вложения отношения e: ra ↪r rb и любого списка l, (l.map e) упорядочен по rb тогда и только тогда, когда l упорядочен по ra.

LaTeX

$$$$ (List.map e\ l).Sorted rb \iff l.Sorted ra. $$$$

Lean4

@[simp]
theorem sorted_listMap (e : ra ↪r rb) {l : List α} : (l.map e).Sorted rb ↔ l.Sorted ra := by
  simp [Sorted, pairwise_map, e.map_rel_iff]

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