instHasFiniteProducts — Mathlib

English

If D has finite products, then the category of J-sheaves on D has finite products.

Русский

Если у категории D существуют конечные произведения, то у категории шейфов J D существуют конечные произведения.

LaTeX

$$$(\text{HasFiniteProducts } D) \Rightarrow (\text{HasFiniteProducts } (\mathrm{Sh}(J,D))).$$$

Lean4

instance [HasFiniteProducts D] : HasFiniteProducts (Sheaf J D) :=
  ⟨inferInstance⟩

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