Computability.Encoding.encode_injective

theorem Computability.Encoding.encode_injective : ∀ {α : Type u} (e : Computability.Encoding α), Function.Injective e.encode

This theorem states that for any type `α` and any computability encoding `e` of that type, the `encode` function of `e` is injective. In other words, if `e.encode x = e.encode y` for any two elements `x` and `y` of the type `α`, then it must be the case that `x = y`. This is a property of the `encode` function in the context of computability theory, ensuring that different elements are encoded to different values, allowing a clear distinction between them.

More concisely: For any type `α` and computability encoding `e` of that type, if `e.encode x = e.encode y`, then `x = y`.