Equivalences involving ℕ

This file defines some additional constructive equivalences using encodable and the pairing function on ℕ.

ink

@[simp]

theorem Equiv.boolProdNatEquivNat_apply : ∀ (a : Bool × ℕ), ↑Equiv.boolProdNatEquivNat a = Function.uncurry Nat.bit a

ink

@[simp]

theorem Equiv.boolProdNatEquivNat_symm_apply : ∀ (a : ℕ), ↑(Equiv.symm Equiv.boolProdNatEquivNat) a = Nat.boddDiv2 a

ink

def Equiv.boolProdNatEquivNat : Bool × ℕ ≃ ℕ

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 }

ink

@[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)

ink

def Equiv.natSumNatEquivNat : ℕ ⊕ ℕ ≃ ℕ

An equivalence between ℕ ⊕ ℕ and ℕ, by mapping (Sum.inl x) to 2 * x and (Sum.inr x) to 2 * x + 1.

Equations

• Equiv.natSumNatEquivNat = Equiv.trans (Equiv.symm (Equiv.boolProdEquivSum ℕ)) Equiv.boolProdNatEquivNat

ink

@[simp]

theorem Equiv.natSumNatEquivNat_apply : ↑Equiv.natSumNatEquivNat = Sum.elim bit0 bit1

ink

def Equiv.intEquivNat : ℤ ≃ ℕ

An equivalence between ℤ and ℕ, through ℤ ≃ ℕ ⊕ ℕ and ℕ ⊕ ℕ ≃ ℕ.

Equations

• Equiv.intEquivNat = Equiv.trans Equiv.intEquivNatSumNat Equiv.natSumNatEquivNat

ink

def Equiv.prodEquivOfEquivNat {α : Type u_1} (e : α ≃ ℕ) : α × α ≃ α

An equivalence between α × α and α, given that there is an equivalence between α and ℕ.

Equations

• Equiv.prodEquivOfEquivNat e = Trans.trans (Trans.trans (Equiv.prodCongr e e) Nat.pairEquiv) (Equiv.symm e)