English
Let l be a list, x an element, and hl₁, hl₂ relate x to each a ∈ l via r and f via s. Then mapping f over (l.orderedInsert r x) equals (l.map f).orderedInsert s (f x).
Русский
Пусть l — список, x — элемент, и hl₁, hl₂ связывают x с каждым a ∈ l через r, а f через s. Тогда отображение f над (l.orderedInsert r x) равно (l.map f).orderedInsert s (f x).
LaTeX
$$$$ \forall f:\alpha\to\beta,\forall l:\mathrm{List}(\alpha),\forall x:\alpha,\forall hl_1,hl_2,\; (\mathrm{List.orderedInsert}\ r\ x\ l).\mathrm{map}\ f = (\mathrm{List.map}\ f\ l).\mathrm{orderedInsert}\ s\ (f\ x). $$$$
Lean4
theorem map_orderedInsert (f : α → β) (l : List α) (x : α) (hl₁ : ∀ a ∈ l, a ≼ x ↔ f a ≼ f x)
(hl₂ : ∀ a ∈ l, x ≼ a ↔ f x ≼ f a) : (l.orderedInsert r x).map f = (l.map f).orderedInsert s (f x) := by
induction l with
| nil => simp
| cons x xs ih =>
rw [List.forall_mem_cons] at hl₁ hl₂
simp only [List.map, List.orderedInsert, ← hl₂.1]
split_ifs
· rw [List.map, List.map]
· rw [List.map, ih (fun _ ha => hl₁.2 _ ha) (fun _ ha => hl₂.2 _ ha)]
