range_succ_eq_Icc_zero

Mathlib.Order.Interval.Finset.Nat

URI: https://scilib.ai/kg/mathlib#Nat.range_succ_eq_Icc_zero

← MathLib Explorer

English

For every natural number n, range(n+1) equals Icc(0,n).

Русский

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

LaTeX

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

Lean4

theorem range_succ_eq_Icc_zero (n : ℕ) : range (n + 1) = Icc 0 n := by
  rw [range_eq_Icc_zero_sub_one _ (Nat.add_one_ne_zero _), Nat.add_sub_cancel_right]

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

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

Разделы

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

Аффилиация

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