finSumFinEquiv — Mathlib

English

Let m and n be natural numbers. There exists a bijection between Fin(m) ⊕ Fin(n) and Fin(m+n). Concretely, the bijection sends inl i to Fin.castAdd n i and inr j to Fin.natAdd m j, with an explicit inverse given by Fin.addCases.

Русский

Пусть m и n — натуральные числа. Существует биекция между Fin(m) ⊕ Fin(n) и Fin(m+n). Бижекция отправляет inl i в Fin.castAdd n i и inr j в Fin.natAdd m j, а обратная биекция задаётся через Fin.addCases.

LaTeX

$$$ Fin(m) \\oplus Fin(n) \\cong Fin(m+n) $$$

Lean4

/-- Equivalence between `Fin m ⊕ Fin n` and `Fin (m + n)` -/
def finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n)
    where
  toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m)
  invFun i := @Fin.addCases m n (fun _ => Fin m ⊕ Fin n) Sum.inl Sum.inr i
  left_inv x := by rcases x with y | y <;> simp
  right_inv x := by refine Fin.addCases (fun i => ?_) (fun i => ?_) x <;> simp

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