instFintype

Mathlib.CategoryTheory.WithTerminal.FinCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.WithInitial.instFintype

English

If the underlying type C is finite, then the type WithInitial(C) is finite as well.

Русский

Если основанный тип C конечен, то и WithInitial(C) конечен.

LaTeX

$$$\#C < \infty \Rightarrow \#(\mathrm{WithInitial}(C)) < \infty$$$

Lean4

instance instFintype [Fintype C] : Fintype (WithInitial C) :=
  .ofEquiv (Option C) <| optionEquiv C

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

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

Разделы

Аффилиация

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