fintypeOfNotInfinite

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#fintypeOfNotInfinite

← MathLib Explorer

English

If α is not infinite, then α is finite.

Русский

Если α не бесконечно, тогда α конечно.

LaTeX

$$$\\neg \\operatorname{Infinite}(\\alpha) \\Rightarrow \\text{Finite}(\\alpha)$$$

Lean4

/-- A non-infinite type is a fintype. -/
noncomputable def fintypeOfNotInfinite {α : Type*} (h : ¬Infinite α) : Fintype α :=
  @Fintype.ofFinite _ (not_infinite_iff_finite.mp h)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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