range_eq_Ico

Mathlib.Order.Interval.Finset.Nat

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

English

For every natural number n, the range n equals the Ico(0,n).

Русский

Для каждого натурального числа n диапазон n равен Ico(0,n).

LaTeX

$$$\forall n \in \mathbb{N},\ \operatorname{range}(n) = \operatorname{Ico}(0,n)$$$

Lean4

theorem _root_.Finset.range_eq_Ico : range = Ico 0 :=
  Ico_zero_eq_range.symm

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

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

Разделы

Аффилиация

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