isEmpty_fintype — Mathlib

English

A type α is infinite iff the type of fintype structures on α is empty.

Русский

Тип α бесконечен тогда и только тогда, когда множество структур Fintype α пусто.

LaTeX

$$$\\operatorname{IsEmpty}(\\mathrm{Fintype}(\\alpha)) \\iff \\operatorname{Infinite}(\\alpha)$$$

Lean4

@[simp]
theorem isEmpty_fintype {α : Type*} : IsEmpty (Fintype α) ↔ Infinite α :=
  ⟨fun ⟨h⟩ => ⟨fun h' => (@nonempty_fintype α h').elim h⟩, fun ⟨h⟩ => ⟨fun h' => h h'.finite⟩⟩

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