instFintype

Mathlib.Topology.Compactification.OnePoint.Basic

URI: https://scilib.ai/kg/mathlib#OnePoint.instFintype

English

If X is finite, then OnePoint X is finite.

Русский

Если X конечно, то OnePoint X конечно.

LaTeX

$$$\\text{Fintype } X \\Rightarrow \\text{Fintype } (\\text{OnePoint } X)$$$

Lean4

instance [Fintype X] : Fintype (OnePoint X) :=
  inferInstanceAs (Fintype (Option X))

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

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

Разделы

Аффилиация

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