numDerangements_add_two

Mathlib.Combinatorics.Derangements.Finite

URI: https://scilib.ai/kg/mathlib#numDerangements_add_two

English

The recurrence D(n+2) = (n+1)(D(n) + D(n+1)) holds for all n.

Русский

Рекуррентное соотношение D(n+2) = (n+1)(D(n) + D(n+1)) верно для всех n.

LaTeX

$$$\\mathrm{numDerangements}(n+2) = (n+1)\\big(\\mathrm{numDerangements}(n) + \\mathrm{numDerangements}(n+1)\\big).$$$

Lean4

theorem numDerangements_add_two (n : ℕ) :
    numDerangements (n + 2) = (n + 1) * (numDerangements n + numDerangements (n + 1)) :=
  rfl

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

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

Разделы

Аффилиация

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