mathlib3 documentation

logic.equiv.nat

Equivalences involving ℕ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
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
source
@[simp]
theorem equiv.bool_prod_nat_equiv_nat_apply (ᾰ : bool × ℕ) :
⇑equiv.bool_prod_nat_equiv_nat ᾰ = function.uncurry nat.bit ᾰ
source
@[simp]
theorem equiv.bool_prod_nat_equiv_nat_symm_apply (ᾰ : ℕ) :
⇑(equiv.bool_prod_nat_equiv_nat.symm) ᾰ = ᾰ.bodd_div2
source
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
source
@[simp]
theorem equiv.nat_sum_nat_equiv_nat_symm_apply (ᾰ : ℕ) :
⇑(equiv.nat_sum_nat_equiv_nat.symm) ᾰ = cond ᾰ.bodd (sum.inr ᾰ.div2) (sum.inl ᾰ.div2)
source
@[simp]
theorem equiv.nat_sum_nat_equiv_nat_apply  :
⇑equiv.nat_sum_nat_equiv_nat = sum.elim bit0 bit1
source
def equiv.int_equiv_nat  :
ℤ ≃ ℕ

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

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

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

Equations