toEncodable — Mathlib

English

A noncomputable choice of an ordering on a finite type is provided by toEncodable.

Русский

Не вычисляемый выбор порядка на конечном типе задаётся через toEncodable.

LaTeX

$$$\\text{toEncodable}(\\alpha) : \\text{Encodable } \\alpha$$$

Lean4

/-- A noncomputable way to arbitrarily choose an ordering on a finite type.
It is not made into a global instance, since it involves an arbitrary choice.
This can be locally made into an instance with `attribute [local instance] Fintype.toEncodable`. -/
noncomputable def _root_.Fintype.toEncodable (α : Type*) [Fintype α] : Encodable α := by
  classical exact (Fintype.truncEncodable α).out

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