English
An encodable type α is equivalent to the range of its encoding function.
Русский
Кодируемый тип α эквивалентен диапазону кодирования его функции.
LaTeX
$$$ \alpha \cong \mathrm{Set.range}(\mathrm{encode} : \alpha \to \mathbb{N}) $$$
Lean4
/-- An encodable type is equivalent to the range of its encoding function. -/
def equivRangeEncode (α : Type*) [Encodable α] : α ≃ Set.range (@encode α _)
where
toFun := fun a : α => ⟨encode a, Set.mem_range_self _⟩
invFun n := Option.get _ (show isSome (decode₂ α n.1) by obtain ⟨x, hx⟩ := n.2; rw [← hx, encodek₂]; exact rfl)
left_inv a := by dsimp; rw [← Option.some_inj, Option.some_get, encodek₂]
right_inv := fun ⟨n, x, hx⟩ => by
apply Subtype.eq
dsimp
conv =>
rhs
rw [← hx]
rw [encode_injective.eq_iff, ← Option.some_inj, Option.some_get, ← hx, encodek₂]
