length

Mathlib.Data.List.Intervals

URI: https://scilib.ai/kg/mathlib#List.Ico.length

English

The length of the list Ico n m equals m − n.

Русский

Длина списка Ico n m равна m − n.

LaTeX

$$$\operatorname{length}(\operatorname{Ico}(n,m)) = m - n$$$

Lean4

@[simp]
theorem length (n m : ℕ) : length (Ico n m) = m - n :=
  by
  dsimp [Ico]
  simp [length_range']

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

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

Разделы

Аффилиация

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