hasCountableCoproducts_of_hasCoproducts

English

If C has countable coproducts, then C has all coproducts of countable shape J.

Русский

Если в C существуют счётные копроодукты, то у C существуют копроодукты формы счётной формы J.

LaTeX

$$$ [\\operatorname{HasCountableCoproducts} \\mathcal{C}] \\Rightarrow \\operatorname{HasCoproductsOfShape J \\mathcal{C}} $$$

Lean4

instance (priority := 100) hasCountableCoproducts_of_hasCoproducts [HasCoproducts C] : HasCountableCoproducts C where
  out
    _ :=
    have : HasCoproducts.{0} C := has_smallest_coproducts_of_hasCoproducts
    inferInstance

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