# The equivalence between `ℕ+` and `ℕ` #

source
def Equiv.pnatEquivNat :
ℕ+ ≃ ℕ

An equivalence between `ℕ+` and `ℕ` given by `PNat.natPred` and `Nat.succPNat`.

Equations

- Equiv.pnatEquivNat = { toFun := PNat.natPred, invFun := Nat.succPNat, left_inv := PNat.succPNat_natPred, right_inv := Nat.natPred_succPNat }

Instances For

source
@[simp]
theorem Equiv.pnatEquivNat_apply :
⇑pnatEquivNat = PNat.natPred
source
@[simp]
theorem Equiv.pnatEquivNat_symm_apply :
⇑pnatEquivNat.symm = Nat.succPNat