listNatEquivNat — Mathlib

English

There exists a bijection between the set of lists of natural numbers and the natural numbers, i.e., List ℕ ≃ ℕ.

Русский

Существует биекция между множеством списков натуральных чисел и множеством натуральных чисел: List ℕ ≃ ℕ.

LaTeX

$$$\\text{List }\\mathbb{N} \\simeq \\mathbb{N}.$$$

Lean4

/-- `List ℕ` is equivalent to `ℕ`. -/
def listNatEquivNat : List ℕ ≃ ℕ :=
  Denumerable.eqv _

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