over_products_of_widePullbacks — Mathlib

English

If C has all finite wide pullbacks, then Over B has all finite products.

Русский

Если в C существуют все конечные широкие pullback, то Over B содержит все конечные произведения.

LaTeX

$$$[HasFiniteWidePullbacks C] \Rightarrow HasFiniteProducts(Over B)$$$

Lean4

/-- Given all wide pullbacks in `C`, construct products in `C/B`. -/
theorem over_products_of_widePullbacks [HasWidePullbacks.{w} C] {B : C} : HasProducts.{w} (Over B) := fun _ =>
  over_product_of_widePullback

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