instHasExplicitFiniteCoproductsTrue

English

The category CompHaus has explicit finite coproducts; for a finite family {X_i}, the coproduct is the disjoint union with the obvious injections.

Русский

Категория CompHaus имеет явные конечные копроизведения; для конечной семейства объектов {X_i} их копроизведение есть дизъюнктное объединение с естественными внедрениями.

LaTeX

$$$\operatorname{HasExplicitFiniteCoproducts}(\text{const}_{\text{True}})$$$

Lean4

instance : HasExplicitFiniteCoproducts.{w, u} (fun _ ↦ True) where hasProp _ := inferInstance

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