hasConicalTerminal — Mathlib

English

If a category has conical products, it also has a conical terminal.

Русский

Если категория имеет конусные произведения, она также имеет конусный предел на терминах.

LaTeX

$$$[HasConicalProducts\, V\, C] \Rightarrow [HasConicalTerminal\, V\, C].$$$

Lean4

instance hasConicalTerminal [HasConicalProducts.{w} V C] : HasConicalTerminal V C :=
  HasConicalLimitsOfShape.of_equiv V C emptyEquivalence.functor

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