comp_preservesLimit — Mathlib

English

If t is a limit cone for a diagram K and F.mapCone t is also a limit cone, then F preserves the limit for K; i.e., there is a canonical witness to preservation.

Русский

Если t — предел-конус диаграммы K и F.mapCone t также предел-конус, тогда F сохраняет предел для K; то есть существует канонический свидетель сохранения.

LaTeX

$$$$\text{IsLimit}(t) \land \text{IsLimit}(F.mapCone(t)) \Rightarrow \mathrm{PreservesLimit}(K,F).$$$$

Lean4

instance comp_preservesLimit [PreservesLimit K F] [PreservesLimit (K ⋙ F) G] : PreservesLimit K (F ⋙ G) where
  preserves hc := ⟨isLimitOfPreserves G (isLimitOfPreserves F hc)⟩

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