preservesLimits_of_createsLimits_and_hasLimits

English

Redundant entry reinforcing preservation when limits exist in target and created by F.

Русский

Повторяющее утверждение: сохранение пределов при существовании пределов в целевой категории и созданных F.

LaTeX

$$$$ \text{PreservesLimitsOfShape } J\; F $$$$

Lean4

/-- `F` preserves limits if it creates limits and `D` has limits. -/
instance (priority := 100) preservesLimits_of_createsLimits_and_hasLimits (F : C ⥤ D) [CreatesLimitsOfSize.{w, w'} F]
    [HasLimitsOfSize.{w, w'} D] : PreservesLimitsOfSize.{w, w'} F where

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