@[simp]
An equivalence between ℕ × ℕ and ℕ, using the mkpair and unpair functions in
data.nat.pairing.
Equations
- equiv.nat_prod_nat_equiv_nat = {to_fun := λ (p : ℕ × ℕ), p.fst.mkpair p.snd, inv_fun := nat.unpair, left_inv := equiv.nat_prod_nat_equiv_nat._proof_1, right_inv := nat.mkpair_unpair}
@[simp]
An equivalence between bool × ℕ and ℕ, by mapping (tt, x) to 2 * x + 1 and (ff, x) to
2 * x.
Equations
An equivalence between ℤ and ℕ, through ℤ ≃ ℕ ⊕ ℕ and ℕ ⊕ ℕ ≃ ℕ.
An equivalence between α × α and α, given that there is an equivalence between α and ℕ.