English
Under a compatibility condition hl, mapping f after insertionSort equals insertionSort of the mapped list with a corresponding relation, i.e., (l.insertionSort r).map f = (l.map f).insertionSort s.
Русский
При условии совместимости hl отображение после insertionSort равно insertionSort применительно к отображённому списку с соответствующим отношением.
LaTeX
$$$$ \forall f:\alpha\to\beta,\forall l:\mathrm{List}(\alpha),\forall hl:\forall a\in l,\forall b\in l, a\preceq b \iff f a \preceq f b,\; \big( (l.insertionSort r) .map f \big) = \big( l.map f \big).insertionSort s. $$$$
Lean4
theorem map_insertionSort (f : α → β) (l : List α) (hl : ∀ a ∈ l, ∀ b ∈ l, a ≼ b ↔ f a ≼ f b) :
(l.insertionSort r).map f = (l.map f).insertionSort s := by
induction l with
| nil => simp
| cons x xs ih =>
simp_rw [List.forall_mem_cons, forall_and] at hl
simp_rw [List.map, List.insertionSort]
rw [List.map_orderedInsert _ s, ih hl.2.2]
· simpa only [mem_insertionSort] using hl.2.1
· simpa only [mem_insertionSort] using hl.1.2
