intEquivNatSumNat — Mathlib

English

The integers are equivalent to a disjoint union of two copies of natural numbers.

Русский

Целые числа эквивалентны дизъюнктному объединению двух копий натуральных чисел.

LaTeX

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

Lean4

/-- The type of integer numbers is equivalent to `ℕ ⊕ ℕ`. -/
def intEquivNatSumNat : ℤ ≃ ℕ ⊕ ℕ where
  toFun z := Int.casesOn z inl inr
  invFun := Sum.elim Int.ofNat Int.negSucc
  left_inv := by rintro (m | n) <;> rfl
  right_inv := by rintro (m | n) <;> rfl

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