eqv — Mathlib

English

A denumerable type α is canonically equivalent to ℕ, i.e., there exists an equivalence α ≃ ℕ.

Русский

У денумерируемого типа α существует естественная эквивалентность α ≃ ℕ.

LaTeX

$$$ \operatorname{eqv}(\alpha) : α \simeq \mathbb{N} $$$

Lean4

/-- A denumerable type is equivalent to `ℕ`. -/
def eqv (α) [Denumerable α] : α ≃ ℕ :=
  ⟨encode, ofNat α, ofNat_encode, encode_ofNat⟩
    -- See Note [lower instance priority]

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