English
The sort of the range n with respect to the natural order equals the standard list range: sort (≤) (range n) = List.range n.
Русский
Сортировка диапазона n по естественному порядку равна стандартному списку List.range n.
LaTeX
$$$ \\operatorname{sort}_{(\\le)}(\\operatorname{range} n) = \\operatorname{List.range} n $$$
Lean4
@[simp]
theorem sort_range (n : ℕ) : sort (· ≤ ·) (range n) = List.range n :=
Multiset.sort_range n