univ_finite_iff_nonempty_fintype — Mathlib

English

The universal set is finite if and only if α carries a finite type structure (i.e., there exists a nonempty fintype on α).

Русский

Объединение всего множества (универсум) конечна тогда и только тогда, когда у α есть конечная структура типа (существует непустой fintype над α).

LaTeX

$$$ (\\mathrm{univ} : Set α).Finite \\iff \\operatorname{Nonempty}(\\text{Fintype } α) $$$

Lean4

theorem univ_finite_iff_nonempty_fintype : (univ : Set α).Finite ↔ Nonempty (Fintype α) :=
  ⟨fun h => ⟨fintypeOfFiniteUniv h⟩, fun ⟨_i⟩ => finite_univ⟩
    -- `simp`-normal form is `Set.toFinset_singleton`.

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