has_smallest_products_of_hasProducts

Mathlib.CategoryTheory.Limits.Shapes.Products

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.has_smallest_products_of_hasProducts

English

If a category has products, then it has the smallest level of products, i.e., HasProducts 0 C.

Русский

Если в категории есть произведения, то существует минимальный уровень произведений: HasProducts 0 C.

LaTeX

$$$\\text{HasProducts}^{0} C$ given $\\text{HasProducts} C$.$$

Lean4

theorem has_smallest_products_of_hasProducts [HasProducts.{w} C] : HasProducts.{0} C :=
  hasProducts_shrink

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

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

Разделы

Аффилиация

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