piAntidiag_univ_fin_eq_antidiagonalTuple

English

There is a canonical representation of piAntidiag on univ as a nat-diagonal tuple, linking function spaces to sequences summing to n.

Русский

Существует каноническое представление piAntidiag на univ в виде нат-диагонального кортежа, связывающего пространства функций с последовательностями, сумма которых равна n.

LaTeX

$$$\\pi\\mathrm{Antidiag}(\\mathrm{univ}, n) = \\mathrm{Nat}.\\mathrm{antidiagonalTuple}(k, n)$$$

Lean4

theorem piAntidiag_univ_fin_eq_antidiagonalTuple (n k : ℕ) : piAntidiag univ n = Nat.antidiagonalTuple k n := by ext;
  simp [Nat.mem_antidiagonalTuple]

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