English
There is a natural equivalence between (Fin m → α) × (Fin n → α) and (Fin (m+n) → α).
Русский
Существует естественная эквивалентность между (Fin m → α) × (Fin n → α) и Fin (m+n) → α.
LaTeX
$$$ (\\mathrm{Fin}\,m \\to α) \\times (\\mathrm{Fin}\,n \\to α) \\cong (\\mathrm{Fin}(m+n) \\to α)$$$
Lean4
/-- The natural `Equiv` between `(Fin m → α) × (Fin n → α)` and `Fin (m + n) → α` -/
@[simps]
def appendEquiv {α : Type*} (m n : ℕ) : (Fin m → α) × (Fin n → α) ≃ (Fin (m + n) → α)
where
toFun fg := Fin.append fg.1 fg.2
invFun f := ⟨fun i ↦ f (Fin.castAdd n i), fun i ↦ f (Fin.natAdd m i)⟩
left_inv fg := by simp
right_inv f := by simp [Fin.append_castAdd_natAdd]
