Equivalences involving ℕ
#
This file defines some additional constructive equivalences using Encodable
and the pairing
function on ℕ
.
@[simp]
theorem
Equiv.boolProdNatEquivNat_symm_apply :
∀ (a : ℕ), ↑Equiv.boolProdNatEquivNat.symm a = Nat.boddDiv2 a
@[simp]
theorem
Equiv.boolProdNatEquivNat_apply :
∀ (a : Bool × ℕ), ↑Equiv.boolProdNatEquivNat a = Function.uncurry Nat.bit a
An equivalence between ℤ
and ℕ
, through ℤ ≃ ℕ ⊕ ℕ
and ℕ ⊕ ℕ ≃ ℕ
.