range_succ

Mathlib.Data.Finset.Range

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

English

The same statement holds for the successor: range(succ n) = insert n (range n).

Русский

То же самое верно и для следующего: range(succ n) = insert n (range n).

LaTeX

$$$$ \operatorname{range}(\mathrm{succ}(n)) = \operatorname{insert}(n, \operatorname{range}(n)). $$$$

Lean4

@[deprecated range_add_one (since := "2025-09-08")]
theorem range_succ : range (succ n) = insert n (range n) :=
  range_add_one

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

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

Разделы

Аффилиация

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