mathlib documentation

logic.equiv.nat

Equivalences involving `ℕ` #

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

@[simp]

def equiv.nat_prod_nat_equiv_nat :

ℕ × ℕ ≃ ℕ

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

Equations

equiv.nat_prod_nat_equiv_nat = {to_fun := λ (p : ℕ × ℕ), nat.mkpair p.fst p.snd, inv_fun := nat.unpair, left_inv := equiv.nat_prod_nat_equiv_nat._proof_1, right_inv := nat.mkpair_unpair}

@[simp]

def equiv.bool_prod_nat_equiv_nat :

bool × ℕ ≃ ℕ

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

Equations

equiv.bool_prod_nat_equiv_nat = {to_fun := λ (_x : bool × ℕ), equiv.bool_prod_nat_equiv_nat._match_1 _x, inv_fun := nat.bodd_div2, left_inv := equiv.bool_prod_nat_equiv_nat._proof_1, right_inv := equiv.bool_prod_nat_equiv_nat._proof_2}
equiv.bool_prod_nat_equiv_nat._match_1 (b, n) = nat.bit b n

@[simp]

def equiv.nat_sum_nat_equiv_nat :

ℕ ⊕ ℕ ≃ ℕ

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

Equations

equiv.nat_sum_nat_equiv_nat = (equiv.bool_prod_equiv_sum ℕ).symm.trans equiv.bool_prod_nat_equiv_nat

def equiv.int_equiv_nat :

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

Equations

equiv.int_equiv_nat = equiv.int_equiv_nat_sum_nat.trans equiv.nat_sum_nat_equiv_nat

def equiv.prod_equiv_of_equiv_nat {α : Type u_1} (e : α ≃ ℕ) :

α × α ≃ α

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

Equations

e.prod_equiv_of_equiv_nat = ((e.prod_congr e).trans equiv.nat_prod_nat_equiv_nat).trans e.symm

def equiv.pnat_equiv_nat :

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

Equations

equiv.pnat_equiv_nat = {to_fun := λ (n : ℕ+), n.val.pred, inv_fun := nat.succ_pnat, left_inv := equiv.pnat_equiv_nat._proof_1, right_inv := equiv.pnat_equiv_nat._proof_2}