Module docstring
{"# The equivalence between ℕ+ and ℕ
"}
Equiv.pnatEquivNat
definition
: ℕ+ ≃ ℕ
Full source
/-- An equivalence between `ℕ+` and `ℕ` given by `PNat.natPred` and `Nat.succPNat`. -/
@[simps -fullyApplied]
def _root_.Equiv.pnatEquivNat : ℕ+ℕ+ ≃ ℕ where
toFun := PNat.natPred
invFun := Nat.succPNat
left_inv := PNat.succPNat_natPred
right_inv := Nat.natPred_succPNatInformal description
The equivalence between the type of positive natural numbers $\mathbb{N}^+$ and the type of natural numbers $\mathbb{N}$ is given by the functions:
- The forward map sends a positive natural number $n$ to its predecessor $n - 1$ (as a natural number)
- The inverse map sends a natural number $n$ to its successor $n + 1$ (as a positive natural number)
This forms a bijection where composing the two maps in either direction yields the identity function.