hasFiniteLimits_of_hasLimitsOfSize

English

If C has all limits of every size, then C has finite limits.

Русский

Если в C существуют пределы всех форм, то в C существуют конечные пределы.

LaTeX

$$$\operatorname{HasFiniteLimits}(C)\quad\text{(follows from having limits of all sizes)}$$$

Lean4

theorem hasFiniteLimits_of_hasLimitsOfSize [HasLimitsOfSize.{v', u'} C] : HasFiniteLimits C where
  out := fun J hJ hJ' =>
    haveI := hasLimitsOfSizeShrink.{0, 0} C
    let F := @FinCategory.equivAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ'
    @hasLimitsOfShape_of_equivalence (@FinCategory.AsType J (@FinCategory.fintypeObj J hJ hJ'))
      (@FinCategory.categoryAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ') _ _ J hJ F _

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