listEncode_injective — Mathlib

English

The encoding of terms in a language into a list of tagged sums is injective.

Русский

Кодирование термов языка в список помеченных сумм инъективно.

LaTeX

$$$$ \\text{The encoding map }\\text{listEncode}: L\\text{Term }\\alpha \\to \\text{List}(\\alpha\\oplus(\\Sigma i, L.Functions i)) \\text{ is injective.}$$$$

Lean4

theorem listEncode_injective : Function.Injective (listEncode : L.Term α → List (α ⊕ (Σ i, L.Functions i))) :=
  Term.encoding.encode_injective

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