decode₂_inj — Mathlib

English

If a1 and a2 both appear in the decoding of the same n, then a1 = a2.

Русский

Если два элемента появляются в расшифровке одного и того же n, то они равны.

LaTeX

$$$ \forall n:\mathbb{N},\forall a_1,a_2:\alpha,\ a_1 \in \mathrm{decode}_2(\alpha,n) \land a_2 \in \mathrm{decode}_2(\alpha,n) \Rightarrow a_1 = a_2$$$

Lean4

theorem decode₂_inj [Encodable α] {n : ℕ} {a₁ a₂ : α} (h₁ : a₁ ∈ decode₂ α n) (h₂ : a₂ ∈ decode₂ α n) : a₁ = a₂ :=
  encode_injective <| (mem_decode₂.1 h₁).trans (mem_decode₂.1 h₂).symm

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