intEquivNat — Mathlib

English

There exists an equivalence between the integers ℤ and the natural numbers ℕ, obtained by composing the standard encodings through ℤ ≃ ℕ ⊕ ℕ and then ℕ ⊕ ℕ ≃ ℕ.

Русский

Существует эквивалентность между целыми числами ℤ и натуральными ℕ, получаемая путём композиции стандартных кодировок через ℤ ≃ ℕ ⊕ ℕ и затем ℕ ⊕ ℕ ≃ ℕ.

LaTeX

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

Lean4

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

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