The equivalence between ℕ+ and ℕ

@[simp]

theorem Equiv.pnatEquivNat_apply : ⇑Equiv.pnatEquivNat = PNat.natPred

@[simp]

theorem Equiv.pnatEquivNat_symm_apply : ⇑Equiv.pnatEquivNat.symm = Nat.succPNat

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 }