Equivalences involving ℕ
#
This file defines some additional constructive equivalences using encodable
and the pairing
function on ℕ
.
@[simp]
theorem
Equiv.boolProdNatEquivNat_apply :
∀ (a : Bool × ℕ), ↑Equiv.boolProdNatEquivNat a = Function.uncurry Nat.bit a
@[simp]
theorem
Equiv.boolProdNatEquivNat_symm_apply :
∀ (a : ℕ), ↑(Equiv.symm Equiv.boolProdNatEquivNat) a = Nat.boddDiv2 a
An equivalence between Bool × ℕ
and ℕ
, by mapping (true, x)
to 2 * x + 1
and
(false, x)
to 2 * x
.
Equations
- Equiv.boolProdNatEquivNat = { toFun := Function.uncurry Nat.bit, invFun := Nat.boddDiv2, left_inv := Equiv.boolProdNatEquivNat.proof_1, right_inv := Equiv.boolProdNatEquivNat.proof_2 }
@[simp]
theorem
Equiv.natSumNatEquivNat_symm_apply :
∀ (a : ℕ), ↑(Equiv.symm Equiv.natSumNatEquivNat) a = bif Nat.bodd a then Sum.inr (Nat.div2 a) else Sum.inl (Nat.div2 a)
An equivalence between ℕ ⊕ ℕ
and ℕ
, by mapping (Sum.inl x)
to 2 * x
and (Sum.inr x)
to
2 * x + 1
.
@[simp]
An equivalence between ℤ
and ℕ
, through ℤ ≃ ℕ ⊕ ℕ
and ℕ ⊕ ℕ ≃ ℕ
.
An equivalence between α × α
and α
, given that there is an equivalence between α
and ℕ
.