range

Mathlib.Data.Multiset.Range

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

← MathLib Explorer

English

range n is the multiset consisting of all integers 0,1,...,n-1.

Русский

range n — это мультимножество, состоящее из чисел 0,1,...,n-1.

LaTeX

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

Lean4

/-- `range n` is the multiset lifted from the list `range n`,
  that is, the set `{0, 1, ..., n-1}`. -/
def range (n : ℕ) : Multiset ℕ :=
  List.range n

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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