# Documentation

Mathlib.Logic.Equiv.Nat

# Equivalences involving ℕ#

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

@[simp]
theorem Equiv.boolProdNatEquivNat_apply :
∀ (a : ),

An equivalence between Bool × ℕ and ℕ, by mapping (true, x) to 2 * x + 1 and (false, x) to 2 * x.

Equations
@[simp]
theorem Equiv.natSumNatEquivNat_symm_apply :
∀ (a : ), = bif then Sum.inr () else Sum.inl ()

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

Equations

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

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

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

Equations