instFintypeCarrier

Mathlib.CategoryTheory.FintypeCat

URI: https://scilib.ai/kg/mathlib#FintypeCat.instFintypeCarrier

English

Let X be a finite type. Then X.carrier is finite.

Русский

Пусть X — конечный тип. Тогда носитель X конечен.

LaTeX

$$$|\\mathrm{carrier}(X)| < \\infty$$$

Lean4

instance {X : FintypeCat} : Fintype X :=
  X.2

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

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

Разделы

Аффилиация

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