finite_iff_nonempty_fintype — Mathlib

English

Finite α holds exactly when there exists a Fintype instance for α (finite iff there exists a fintype structure).

Русский

Конечность α эквивалентна существованию структуры конечного типа для α.

LaTeX

$$$\operatorname{Finite}(\alpha) \iff \operatorname{Nonempty}(\text{Fintype }\alpha).$$$

Lean4

theorem finite_iff_nonempty_fintype (α : Type*) : Finite α ↔ Nonempty (Fintype α) :=
  ⟨fun _ => nonempty_fintype α, fun ⟨_⟩ => inferInstance⟩

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