ofWidePullbacks — Mathlib

English

If F preserves limits of shape WithTerminal J, then the functor Over.post F preserves limits of shape J.

Русский

Если F сохраняет пределы формы WithTerminal J, тогда функтор Over.post F сохраняет пределы формы J.

LaTeX

$$$\text{PreservesLimitsOfShape} (WithTerminal\ J)\ F \Rightarrow \text{PreservesLimitsOfShape } J\ (\mathrm{Over.post}\ F)$$$

Lean4

instance ofWidePullbacks {J : Type*} [PreservesLimitsOfShape (WidePullbackShape J) F] :
    PreservesLimitsOfShape (WithTerminal <| Discrete J) F :=
  preservesLimitsOfShape_of_equiv WithTerminal.widePullbackShapeEquiv F

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