natEquivNatSumPUnit — Mathlib

English

The natural numbers are equivalent to a countable sum of a pair of natural numbers.

Русский

Натуральные числа эквивалентны счетному удвоению натуральных чисел.

LaTeX

$$$$ \\mathbb{N} \\simeq \\mathbb{N} \\oplus \\mathbb{N}. $$$$

Lean4

/-- The set of natural numbers is equivalent to `ℕ ⊕ PUnit`. -/
def natEquivNatSumPUnit : ℕ ≃ ℕ ⊕ PUnit
    where
  toFun n := Nat.casesOn n (inr PUnit.unit) inl
  invFun := Sum.elim Nat.succ fun _ => 0
  left_inv n := by cases n <;> rfl
  right_inv := by rintro (_ | _) <;> rfl

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