antidiagonal_eq_map

Mathlib.Data.Finset.NatAntidiagonal

URI: https://scilib.ai/kg/mathlib#Finset.Nat.antidiagonal_eq_map

English

The antidiagonal n is obtained by mapping i from 0 to n to the pair (i, n−i).

Русский

Антидиагональнaя пара n получается отображением i↦(i, n−i) для i от 0 до n.

LaTeX

$$$\operatorname{antidiagonal}(n) = \operatorname{range}(n+1) \mapsto (i, n-i)$$$

Lean4

theorem antidiagonal_eq_map (n : ℕ) :
    antidiagonal n = (range (n + 1)).map ⟨fun i ↦ (i, n - i), fun _ _ h ↦ (Prod.ext_iff.1 h).1⟩ :=
  rfl

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

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

Разделы

Аффилиация

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