hasFiniteProducts — Mathlib

English

If C has finite products and W contains identities and is stable under finite products, then D has finite products.

Русский

Если C имеет конечные произведения, и W содержит тождественные морфизмы и сохраняется под конечными произведениями, то D имеет конечные произведения.

LaTeX

$$$ \\mathrm{HasFiniteProducts}\ D $$$

Lean4

theorem hasFiniteProducts : HasFiniteProducts D :=
  ⟨fun _ => hasProductsOfShape L W _⟩

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