English
There is a natural equivalence between Fin2 n and Fin n given by toFin and ofFin, with inverse relationships.
Русский
Существует естественное эквивалентное соответствие между Fin2 n и Fin n, задаваемое отображениями toFin и ofFin, взаимно обратными.
LaTeX
$$$\mathrm{equivFin}(n) : \mathrm{Fin2}(n) \simeq \mathrm{Fin}(n),\; \text{toFun} = \mathrm{toFin},\; \text{invFun} = \mathrm{ofFin},\; \text{left_inv} = \mathrm{ofFin\_toFin},\; \text{right_inv} = \mathrm{toFin\_ofFin}.$$$
Lean4
/-- `Fin2` is equivalent to the usual encoding of `Fin` as a subtype of `ℕ`. -/
@[simps]
def equivFin (n : Nat) : Fin2 n ≃ Fin n where
toFun := toFin
invFun := ofFin
left_inv := ofFin_toFin
right_inv := toFin_ofFin
