sorted_lt_range

Mathlib.Data.List.Sort

URI: https://scilib.ai/kg/mathlib#List.sorted_lt_range

English

For every natural number n, the list range(n) is strictly increasing with respect to <.

Русский

Для каждого натурального числа n последовательность range(n) строго возрастает по отношению к <.

LaTeX

$$$\\mathrm{Sorted}(<)(\\mathrm{range}(n))$$$

Lean4

theorem sorted_lt_range (n : ℕ) : Sorted (· < ·) (range n) :=
  by
  rw [Sorted, pairwise_iff_get]
  simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru