English
For all a,b,s, range' a b s is sorted with respect to ≤.
Русский
Для любых a,b,s диапазон range' a b s упорядочен по ≤.
LaTeX
$$$$ \forall a,b,s:\mathbb{N},\ List.Sorted(\le)(List.range' a b s). $$$$
Lean4
theorem filterMap {α β : Type*} {p : α → Option β} {l : List α} {r : α → α → Prop} {r' : β → β → Prop} (hl : l.Sorted r)
(hp : ∀ (a b : α) (c d : β), p a = some c → p b = some d → r a b → r' c d) : (l.filterMap p).Sorted r' := by
induction l with
| nil => simp
| cons a l ih =>
rw [List.filterMap_cons]
cases ha : p a with
| none => exact ih (List.sorted_cons.mp hl).right
| some b =>
rw [List.sorted_cons]
refine ⟨fun x hx ↦ ?_, ih (List.sorted_cons.mp hl).right⟩
obtain ⟨u, hu, hu'⟩ := List.mem_filterMap.mp hx
exact hp a u b x ha hu' <| (List.sorted_cons.mp hl).left u hu
