encode' — Mathlib

English

The encode' map is an embedding of α into ℕ, i.e., an injective encoding function for Encodable α.

Русский

Кодировка encode' является вложением α в ℕ, то есть инъективное кодирование.

LaTeX

$$$ \text{encode'}(\alpha) : \alpha \hookrightarrow \mathbb{N} $$$

Lean4

/-- The `encode` function, viewed as an embedding. -/
def encode' (α) [Encodable α] : α ↪ ℕ :=
  ⟨Encodable.encode, Encodable.encode_injective⟩

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