nonempty_fintype — Mathlib

English

If α is finite, then α has a fintype structure; hence there exists a finite encoding of α.

Русский

Если α конечно, то на α существует структура конечного типа; следовательно, существует конечное кодирование α.

LaTeX

$$$\text{Nonempty }(\mathrm{Fintype}\ α)$$$

Lean4

/-- See also `nonempty_encodable`, `nonempty_denumerable`. -/
theorem nonempty_fintype (α : Type*) [Finite α] : Nonempty (Fintype α) :=
  by
  rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
  exact ⟨.ofEquiv _ e.symm⟩

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