finSigmaFinEquiv_one — Mathlib

English

When the outer index range is Fin 1, the sigma equivalence reduces to projecting to the inner Fin (n i) component.

Русский

При внешнем диапазоне Fin 1 эквивалентность сигмы сводится к проекции на внутреннюю компоненту Fin (n i).

LaTeX

$$$\\mathrm{finSigmaFinEquiv\\_one} : \\mathrm{Fin}\\!\\!1 \\times \\mathrm{Fin}(n\\,i) \\to \\mathrm{Fin}(n\\,i), \\quad (i,j) \\mapsto j$$$

Lean4

/-- `finSigmaFinEquiv` on `Fin 1 × f` is just `f` -/
theorem finSigmaFinEquiv_one {n : Fin 1 → ℕ} (ij : (i : Fin 1) × Fin (n i)) : (finSigmaFinEquiv ij : ℕ) = ij.2 :=
  by
  rw [finSigmaFinEquiv_apply, add_eq_right]
  apply @Finset.sum_of_isEmpty _ _ _ _ (by simpa using Fin.isEmpty')

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