Documentation

Mathlib.Logic.Equiv.Nat

Equivalences involving #

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

@[simp]
@[simp]
theorem Equiv.boolProdNatEquivNat_apply :
∀ (a : Bool × ), Equiv.boolProdNatEquivNat a = Function.uncurry Nat.bit a

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

Equations
Instances For
    @[simp]
    theorem Equiv.natSumNatEquivNat_symm_apply :
    ∀ (a : ), Equiv.natSumNatEquivNat.symm a = Bool.rec (Sum.inl a.div2) (Sum.inr a.div2) a.bodd

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

    Equations
    Instances For
      @[simp]
      theorem Equiv.natSumNatEquivNat_apply :
      Equiv.natSumNatEquivNat = Sum.elim (fun (x : ) => 2 * x) fun (x : ) => 2 * x + 1

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

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

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

        Equations
        Instances For