sorted_swap_listMap — Mathlib

English

For a RelEmbedding e, sorting after mapping with e and then swapping the relation is equivalent to sorting with the swapped relations on the original list.

Русский

Для вложения отношения e упорядоченность после отображения и применения перестановки эквивалентна упорядоченности по обмененным отношениям на исходном списке.

LaTeX

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

Lean4

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

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