range

Mathlib.Data.Finset.Range

URI: https://scilib.ai/kg/mathlib#Finset.range

English

The finite set range(n) consists exactly of the natural numbers 0,1,2, ..., n−1.

Русский

Конечное множество range(n) состоит ровно из натуральных чисел 0,1,2,..., n−1.

LaTeX

$$$$ \operatorname{range}(n) = \{0,1,\dots, n-1\}. $$$$

Lean4

/-- `range n` is the set of natural numbers less than `n`. -/
def range (n : ℕ) : Finset ℕ :=
  ⟨_, nodup_range n⟩

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

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

Разделы

Аффилиация

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