English
A finite type admits a truncation-encoded encodable instance, reflecting non-uniqueness of encoding.
Русский
Конечный тип допускает экземпляр кодируемости через усечённое кодирование, учитывающее неуникальность кодирования.
LaTeX
$$$ \\text{Fintype.truncEncodable}(\\alpha) : \\text{Trunc}(\\text{Encodable } \\alpha)$$$
Lean4
/-- A finite type is encodable. Because the encoding is not unique, we wrap it in `Trunc` to
preserve computability. -/
def _root_.Fintype.truncEncodable (α : Type*) [DecidableEq α] [Fintype α] : Trunc (Encodable α) :=
@Quot.recOnSubsingleton _ _ (fun s : Multiset α => (∀ x : α, x ∈ s) → Trunc (Encodable α)) _ Finset.univ.1
(fun l H => Trunc.mk <| encodableOfList l H) Finset.mem_univ
