English
There is a canonical equivalence between the dependent sum (Σ n, antidiagonalTuple k n) and the function type Fin k → ℕ; the toFun forgets n and keeps the tuple, the invFun sends a function to the pair (sum, tuple) together with a proof of membership.
Русский
Существует каноническое эквивалентное отображение между зависимой суммой (Σ n, antidiagonalTuple k n) и функциями Fin k → ℕ; отображение туда забывает n и сохраняет кортеж, обратно функция отправляет одностороннюю пару в соответствующий элемент.
LaTeX
$$$ (\Sigma n:\mathbb{N}, \operatorname{antidiagonalTuple}(k,n)) \simeq (\mathrm{Fin}(k) \to \mathbb{N}). $$$
Lean4
/-- The disjoint union of antidiagonal tuples `Σ n, antidiagonalTuple k n` is equivalent to the
`k`-tuple `Fin k → ℕ`. This is such an equivalence, obtained by mapping `(n, x)` to `x`.
This is the tuple version of `Finset.sigmaAntidiagonalEquivProd`. -/
@[simps]
def sigmaAntidiagonalTupleEquivTuple (k : ℕ) : (Σ n, antidiagonalTuple k n) ≃ (Fin k → ℕ)
where
toFun x := x.2
invFun x := ⟨∑ i, x i, x, mem_antidiagonalTuple.mpr rfl⟩
left_inv := fun ⟨_, _, h⟩ => Sigma.subtype_ext (mem_antidiagonalTuple.mp h) rfl
