range_add_one

Mathlib.Data.Finset.Range

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

English

For any natural n, range(n+1) is obtained by inserting n into range(n).

Русский

Для любого натурального n диапазон(n+1) получается добавлением элемента n в диапазон(n).

LaTeX

$$$$ \operatorname{range}(n+1) = \operatorname{insert}(n, \operatorname{range}(n)). $$$$

Lean4

theorem range_add_one : range (n + 1) = insert n (range n) := by grind

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

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

Разделы

Аффилиация

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