sort_range — Mathlib

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

Похожие утверждения