Mathlib.Logic.Equiv.Nat

Equiv.boolProdNatEquivNat definition

: Bool × ℕ ≃ ℕ

Full source

/-- An equivalence between `Bool × ℕ` and `ℕ`, by mapping `(true, x)` to `2 * x + 1` and
`(false, x)` to `2 * x`. -/
@[simps]
def boolProdNatEquivNat : BoolBool × ℕBool × ℕ ≃ ℕ where
  toFun := uncurry bit
  invFun := boddDiv2
  left_inv := fun ⟨b, n⟩ => by simp only [bodd_bit, div2_bit, uncurry_apply_pair, boddDiv2_eq]
  right_inv n := by simp only [bit_decomp, boddDiv2_eq, uncurry_apply_pair]

Equivalence between $\mathrm{Bool} \times \mathbb{N}$ and $\mathbb{N}$ via doubling and parity

Informal description

The equivalence between $\mathrm{Bool} \times \mathbb{N}$ and $\mathbb{N}$ is defined by mapping $(true, x)$ to $2x + 1$ and $(false, x)$ to $2x$. This is a bijection with an inverse function that reconstructs the original pair from the natural number.

Equiv.natSumNatEquivNat definition

: ℕ ⊕ ℕ ≃ ℕ

Full source

/-- An equivalence between `ℕ ⊕ ℕ` and `ℕ`, by mapping `(Sum.inl x)` to `2 * x` and `(Sum.inr x)` to
`2 * x + 1`.
-/
@[simps! symm_apply]
def natSumNatEquivNat : ℕℕ ⊕ ℕℕ ⊕ ℕ ≃ ℕ :=
  (boolProdEquivSum ℕ).symm.trans boolProdNatEquivNat

Equivalence between $\mathbb{N} \oplus \mathbb{N}$ and $\mathbb{N}$ via doubling and parity adjustment

Informal description

The equivalence between $\mathbb{N} \oplus \mathbb{N}$ and $\mathbb{N}$ is defined by mapping $\mathrm{Sum.inl}(x)$ to $2x$ and $\mathrm{Sum.inr}(x)$ to $2x + 1$. This bijection pairs each natural number with either an even or odd number, effectively splitting $\mathbb{N}$ into two copies of itself.

Equiv.natSumNatEquivNat_apply theorem

: ⇑natSumNatEquivNat = Sum.elim (2 * ·) (2 * · + 1)

Full source

@[simp]
theorem natSumNatEquivNat_apply : ⇑natSumNatEquivNat = Sum.elim (2 * ·) (2 * · + 1) := by
  ext (x | x) <;> rfl

Application of the Equivalence $\mathbb{N} \oplus \mathbb{N} \simeq \mathbb{N}$ via Doubling and Parity Adjustment

Informal description

The application of the equivalence $\mathbb{N} \oplus \mathbb{N} \simeq \mathbb{N}$ is given by the function $f$ defined as: \[ f(\mathrm{inl}(x)) = 2x \quad \text{and} \quad f(\mathrm{inr}(x)) = 2x + 1 \] where $\mathrm{inl}$ and $\mathrm{inr}$ are the left and right injections into the sum type $\mathbb{N} \oplus \mathbb{N}$.

Equiv.intEquivNat definition

: ℤ ≃ ℕ

Full source

/-- An equivalence between `ℤ` and `ℕ`, through `ℤ ≃ ℕ ⊕ ℕ` and `ℕ ⊕ ℕ ≃ ℕ`.
-/
def intEquivNat : ℤℤ ≃ ℕ :=
  intEquivNatSumNat.trans natSumNatEquivNat

Equivalence between integers and natural numbers

Informal description

An equivalence between the integers $\mathbb{Z}$ and the natural numbers $\mathbb{N}$, constructed by composing the equivalence $\mathbb{Z} \simeq \mathbb{N} \oplus \mathbb{N}$ (which maps non-negative integers to the left summand and negative integers to the right summand) with the equivalence $\mathbb{N} \oplus \mathbb{N} \simeq \mathbb{N}$ (which maps pairs of natural numbers to natural numbers via $2x$ and $2x + 1$).

Equiv.prodEquivOfEquivNat definition

(e : α ≃ ℕ) : α × α ≃ α

Full source

/-- An equivalence between `α × α` and `α`, given that there is an equivalence between `α` and `ℕ`.
-/
def prodEquivOfEquivNat (e : α ≃ ℕ) : α × αα × α ≃ α :=
  calc
    α × α ≃ ℕ × ℕ := prodCongr e e
    _ ≃ ℕcalc
    α × α ≃ ℕ × ℕ := prodCongr e e
    _ ≃ ℕ := pairEquiv
    _ ≃ α := e.symm

Equivalence between $\alpha \times \alpha$ and $\alpha$ via $\mathbb{N}$

Informal description

Given an equivalence $e : \alpha \simeq \mathbb{N}$ between a type $\alpha$ and the natural numbers, there is an equivalence $\alpha \times \alpha \simeq \alpha$ constructed by composing the product equivalence $\alpha \times \alpha \simeq \mathbb{N} \times \mathbb{N}$ induced by $e$, the pairing equivalence $\mathbb{N} \times \mathbb{N} \simeq \mathbb{N}$, and the inverse equivalence $\mathbb{N} \simeq \alpha$ of $e$.