instCountableAB4StarOfAB4StarOfSize

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instCountableAB4StarOfAB4StarOfSize

English

If C has products of size 0 and AB4StarOfSize 0, then CountableAB4Star holds.

Русский

Если в C есть произведения нулевого размера и AB4StarOfSize 0, тогда CountableAB4Star выполняется.

LaTeX

$$$[HasProducts.{0} C] \land [AB4StarOfSize.{0} C] \Rightarrow CountableAB4Star C$$$

Lean4

instance (priority := 100) [HasProducts.{0} C] [AB4StarOfSize.{0} C] : CountableAB4Star C :=
  ⟨inferInstance⟩

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

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

Разделы

Аффилиация

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