ofFinite — Mathlib

English

Noncomputably obtain a Fintype instance on α from a Finite α; this selects some concrete enumeration.

Русский

Невычислимо получаем структуру конечного типа на α из конечности α; выбирается конкретное перечисление.

LaTeX

$$$\text{There exists a }\mathrm{Fintype}\;\alpha\text{ given a }\mathrm{Finite}\;\alpha.$$$

Lean4

/-- Noncomputably get a `Fintype` instance from a `Finite` instance. This is not an
instance because we want `Fintype` instances to be useful for computations. -/
noncomputable def ofFinite (α : Type*) [Finite α] : Fintype α :=
  (nonempty_fintype α).some

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