finite_colimitType — Mathlib

English

The colimit type of a diagram from a finite category to Type* with finite objects is finite.

Русский

Тип колимита для диаграммы из конечной категории в Type*, состоящей из конечных объектов, конечен.

LaTeX

$$$\\text{Finite}(K.\\ ColimitType)$$$

Lean4

/-- The colimit type of a functor from a finite category to Types that only
involves finite objects is finite. -/
instance finite_colimitType {J : Type} [SmallCategory J] [FinCategory J] (K : J ⥤ Type*) [∀ j, Finite (K.obj j)] :
    Finite K.ColimitType :=
  Quot.finite _

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