data.equiv.nat

# Equivalences involving ℕ#

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

@[simp]

An equivalence between ℕ × ℕ and ℕ, using the mkpair and unpair functions in data.nat.pairing.

Equations
@[simp]

An equivalence between bool × ℕ and ℕ, by mapping (tt, x) to 2 * x + 1 and (ff, x) to 2 * x.

Equations
@[simp]

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.prod_equiv_of_equiv_nat {α : Type (max u_1 u_2)} (e : α ) :
α × α α

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

Equations

An equivalence between ℕ+ and ℕ, by mapping x in ℕ+ to x - 1 in ℕ.

Equations