English
If l and l' are sorted with respect to r, then their merge is also sorted with respect to r.
Русский
Если списки l и l' отсортированы относительно r, то их слияние тоже отсортировано относительно r.
LaTeX
$$$ Sorted_r(l) \\land Sorted_r(l') \\Rightarrow Sorted_r(\\text{merge}(l,l')) $$$
Lean4
theorem merge {l l' : List α} (h : Sorted r l) (h' : Sorted r l') : Sorted r (merge l l' (r · ·)) := by
simpa using
sorted_merge (le := (r · ·))
(fun a b c h₁ h₂ => by simpa using _root_.trans (by simpa using h₁) (by simpa using h₂))
(fun a b => by simpa using IsTotal.total a b) l l' (by simpa using h) (by simpa using h')
