over_product_of_widePullback — Mathlib

English

Same as above: a limit for a discrete diagram in Over B exists given a wide pullback limit in C.

Русский

То же самое: предел дискретной диаграммы в Over B существует при наличии широкого предела pullback в C.

LaTeX

$$$\forall F: \mathrm{Discrete}(J) \to \mathrm{Over}(B),\ HasLimit F$$$

Lean4

/-- Given a wide pullback in `C`, construct a product in `C/B`. -/
theorem over_product_of_widePullback [HasLimitsOfShape (WidePullbackShape J) C] {B : C} :
    HasLimitsOfShape (Discrete J) (Over B) :=
  { has_limit := fun F => has_over_limit_discrete_of_widePullback_limit F }

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