def NatPair.equiv : ℕ × ℕ ≃ ℕ

Equations

• NatPair.equiv = { toFun := NatPair.f, invFun := NatPair.g, left_inv := NatPair.leftInverse_g_f, right_inv := NatPair.rightInverse_g_f }