hasFiniteLimits_of_hasTerminal_and_pullbacks

English

A category with terminal objects and pullbacks has finite limits.

Русский

Категория с терминальными объектами и вытянутыми обратными границами имеет конечные пределы.

LaTeX

$$$HasTerminal(C) \land HasPullbacks(C) \Rightarrow HasFiniteLimits(C)$$$

Lean4

theorem hasFiniteLimits_of_hasTerminal_and_pullbacks [HasTerminal C] [HasPullbacks C] : HasFiniteLimits C :=
  @hasFiniteLimits_of_hasEqualizers_and_finite_products C _
    (@hasFiniteProducts_of_has_binary_and_terminal C _ (hasBinaryProducts_of_hasTerminal_and_pullbacks C) inferInstance)
    (@hasEqualizers_of_hasPullbacks_and_binary_products C _ (hasBinaryProducts_of_hasTerminal_and_pullbacks C)
      inferInstance)

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