listEncode_sigma_injective — Mathlib

English

The encoding of bounded formulas, when applied to the second component, is injective with respect to the formula component.

Русский

Кодирование ограниченных формул по второй составляющей инъективно по самой формуле.

LaTeX

$$$\\text{listEncode}_{\\sigma}: (n, φ) \\mapsto φ.listEncode$ is injective in φ.$$

Lean4

theorem listEncode_sigma_injective : Function.Injective fun φ : Σ n, L.BoundedFormula α n => φ.2.listEncode :=
  BoundedFormula.encoding.encode_injective

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