instHasSeparator — Mathlib

English

If C has a separator, then the category of homological complexes over C with shape c also has a separator, defined via separatingFamily and Coproducts.

Русский

Если в категории C есть разделитель, то категория гомологическх комплексов над C с формой c также имеет разделитель, задаваемый через separatingFamily и coproducts.

LaTeX

$$$[\text{HasSeparator } C] \Rightarrow \mathrm{HasSeparator}(\mathrm{HomologicalComplex}(C,c))$$$

Lean4

instance [HasSeparator C] : HasSeparator (HomologicalComplex C c) :=
  ⟨_, isSeparator_coproduct_separatingFamily c (isSeparator_separator C)⟩

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