English
There is an equivalence between Fin n ⊕ ℕ and ℕ. The toFun sends inl a to a and inr b to n + b; the inverse uses a case distinction depending on whether the natural number is less than n.
Русский
Существует эквивелентность между Fin n ⊕ ℕ и ℕ. Преобразование toFun отправляет inl a в a, а inr b в n + b; обратное используeт разложение в зависимости от того, меньше ли число n.
LaTeX
$$$ Fin(n) \\oplus \\mathbb{N} \\cong \\mathbb{N} $$$
Lean4
/-- Equivalence between `Fin n ⊕ ℕ` and `ℕ` that sends `inl (a : Fin n)` to
`(a : ℕ)` and `inr a` to `n + a`. -/
def finSumNatEquiv (n : ℕ) : Fin n ⊕ ℕ ≃ ℕ
where
toFun := Sum.elim Fin.val (n + ·)
invFun i := if hi : i < n then .inl ⟨i, hi⟩ else .inr (i - n)
left_inv
i :=
(i.casesOn (fun _ => dif_pos (Fin.is_lt _))
(fun _ => (dif_neg (Nat.le_add_right _ _).not_gt).trans <| congrArg _ (Nat.add_sub_cancel_left _ _)))
right_inv
i :=
(apply_dite _ _ _ _).trans <|
(i.lt_or_ge n).by_cases (fun hi => dif_pos hi) (fun hi => (dif_neg hi.not_gt).trans <| Nat.add_sub_cancel' hi)
