English
There is a natural bijection between the dependent sum (i : Fin m) × Fin (n i) and the finite type Fin (∑ i : Fin m, n i).
Русский
Существует естественная биекция между зависимым суммой (i : Fin m) × Fin (n i) и конечным множеством Fin (∑ i : Fin m, n i).
LaTeX
$$$(i:\\mathrm{Fin} m) \\times \\mathrm{Fin}(n\\,i) \\cong \\mathrm{Fin}\\left(\\sum_{i:\\mathrm{Fin} m} n\\,i\\right)$$$
Lean4
/-- Equivalence between the Sigma type `(i : Fin m) × Fin (n i)` and `Fin (∑ i : Fin m, n i)`. -/
def finSigmaFinEquiv {m : ℕ} {n : Fin m → ℕ} : (i : Fin m) × Fin (n i) ≃ Fin (∑ i : Fin m, n i) :=
match m with
| 0 => @Equiv.equivOfIsEmpty _ _ _ (by simpa using Fin.isEmpty')
| Nat.succ m =>
calc
_ ≃ _ := (@finSumFinEquiv m 1).sigmaCongrLeft.symm
_ ≃ _ := (Equiv.sumSigmaDistrib _)
_ ≃ _ := (finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma _))
_ ≃ _ := finSumFinEquiv
_ ≃ _ := finCongr (Fin.sum_univ_castSucc n).symm
