Documentation

Mathlib.Data.PNat.Equiv

The equivalence between ℕ+ and ℕ #

source
def Equiv.pnatEquivNat :
ℕ+ ≃ ℕ

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

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