English
There is a natural equivalence between the dependent sum (Σ n, antidiagonalTuple k n) and the function type Fin k → ℕ; forgetting the index yields the embedding to functions, and conversely the inverse maps a function to the pair (sum, function) with the appropriate membership proof.
Русский
Существует естественное эквивалентное соответствие между декартовым суммой (Σ n, antidiagonalTuple k n) и функциями Fin k → ℕ; обратное преобразование строится через сумму и доказательство принадлежности.
LaTeX
$$$ (\Sigma n:\mathbb{N}, \operatorname{antidiagonalTuple}(k,n)) \simeq (\mathrm{Fin}(k) \to \mathbb{N}). $$$
Lean4
/-- `Finset.Nat.antidiagonalTuple k n` is a finset of `k`-tuples summing to `n` -/
def antidiagonalTuple (k n : ℕ) : Finset (Fin k → ℕ) :=
⟨Multiset.Nat.antidiagonalTuple k n, Multiset.Nat.nodup_antidiagonalTuple k n⟩
