boolProdNatEquivNat — Mathlib

English

There is a natural-number encoding of pairs (b, n) where b ∈ Bool and n ∈ ℕ, mapping (true, n) to 2n+1 and (false, n) to 2n.

Русский

Существует биекция между Bool × ℕ и ℕ, задаваемая отображением (true, n) ↦ 2n+1 и (false, n) ↦ 2n.

LaTeX

$$$(\\mathrm{true},n) \\mapsto 2n+1$, $(\\mathrm{false},n) \\mapsto 2n$; equivalence between $\\text{Bool} \\times \\mathbb{N}$ and $\\mathbb{N}$.$$

Lean4

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

Похожие утверждения