encode_injective — Mathlib

English

If α is encodable, then encode: α → ℕ is injective; i.e., encode a = encode b implies a = b.

Русский

Если α можно закодировать, то кодировка α → ℕ инъективна; то есть encode a = encode b ⇒ a = b.

LaTeX

$$$\operatorname{encode} : α \to ℕ\; \;\; \text{ is injective: } \forall a,b,\ encode(a)=encode(b) \Rightarrow a=b$$$

Lean4

theorem encode_injective [Encodable α] : Function.Injective (@encode α _)
  | x, y, e => Option.some.inj <| by rw [← encodek, e, encodek]

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