encode_injective — Mathlib

English

For any encoding e, the encode function is injective; distinct inputs map to distinct encodings.

Русский

Для любого кодирования e функция кодирования инъективна: разные входы дают разные коды.

LaTeX

$$$ \forall x,y:\ e.encode(x)=e.encode(y) \Rightarrow x=y $$$

Lean4

theorem encode_injective {α : Type u} (e : Encoding α) : Function.Injective e.encode :=
  by
  refine fun _ _ h => Option.some_injective _ ?_
  rw [← e.decode_encode, ← e.decode_encode, h]

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