of_not_fintype

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#Infinite.of_not_fintype

English

If there is no fintype structure on α, then α is infinite.

Русский

Если для α не существует структуры конечного множества, то α бесконечен.

LaTeX

$$Not exists Fintype(α) ⇒ Infinite(α)$$

Lean4

theorem of_not_fintype (h : Fintype α → False) : Infinite α :=
  isEmpty_fintype.mp ⟨h⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru