hasCoproductsOfShape_of_small — Mathlib

English

For a type β that is small, if C has coproducts, then HasCoproductsOfShape β C holds.

Русский

Для типа β, являющегося малым, если в C существуют копроизведения, то HasCoproductsOfShape β C holds.

LaTeX

$$$ HasCoproductsOfShape\\beta\\ C $$$

Lean4

theorem hasCoproductsOfShape_of_small (β : Type w₂) [Small.{w₁} β] [HasCoproducts.{w₁} C] : HasCoproductsOfShape β C :=
  hasColimitsOfShape_of_equivalence <| Discrete.equivalence <| Equiv.symm <| equivShrink β

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