Documentation

Mathlib.Logic.Equiv.Nat

Equivalences involving ℕ #

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

source
def Equiv.boolProdNatEquivNat :
Bool × ℕ ≃ ℕ

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

Equations
Instances For
    source
    @[simp]
    theorem Equiv.boolProdNatEquivNat_apply (a✝ : Bool × ℕ) :
    boolProdNatEquivNat a✝ = Function.uncurry Nat.bit a✝
    source
    @[simp]
    theorem Equiv.boolProdNatEquivNat_symm_apply (n : ℕ) :
    boolProdNatEquivNat.symm n = (n.bodd, n.div2)
    source
    def Equiv.natSumNatEquivNat :
    ℕ ⊕ ℕ ≃ ℕ

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

    Equations
    Instances For
      source
      @[simp]
      theorem Equiv.natSumNatEquivNat_symm_apply (a✝ : ℕ) :
      natSumNatEquivNat.symm a✝ = if a✝.bodd = true then Sum.inr a✝.div2 else Sum.inl a✝.div2
      source
      @[simp]
      theorem Equiv.natSumNatEquivNat_apply :
      ⇑natSumNatEquivNat = Sum.elim (fun (x : ℕ) => 2 * x) fun (x : ℕ) => 2 * x + 1
      source
      def Equiv.intEquivNat :
      ℤ ≃ ℕ

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

      Equations
      Instances For
        source
        def Equiv.prodEquivOfEquivNat {α : Type u_1} (e : α ≃ ℕ) :
        α × α ≃ α

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

        Equations
        Instances For