sorted_le_range

Mathlib.Data.List.Sort

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

English

For any natural n, the list range n is sorted with respect to ≤.

Русский

Для любого натурального n список range n упорядочен по ≤.

LaTeX

$$$$ \forall n: \mathbb{N},\ List.Sorted(\le)(\operatorname{range} n). $$$$

Lean4

theorem sorted_le_range (n : ℕ) : Sorted (· ≤ ·) (range n) :=
  (sorted_lt_range n).le_of_lt

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

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

Разделы

Аффилиация

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