antidiagonalTuple_zero_succ

Mathlib.Data.Fin.Tuple.NatAntidiagonal

URI: https://scilib.ai/kg/mathlib#List.Nat.antidiagonalTuple_zero_succ

English

The 0-tuple with sum n+1 is empty.

Русский

Нулевой кортеж со суммой n+1 пуст.

LaTeX

$$$ antidiagonalTuple\\ 0\\ (n+1) = \\emptyset $$$

Lean4

@[simp]
theorem antidiagonalTuple_zero_succ (n : ℕ) : antidiagonalTuple 0 (n + 1) = [] :=
  rfl

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

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

Разделы

Аффилиация

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