preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape

English

A reiteration: preserves limits if creates and D has them.

Русский

Повторное утверждение: сохраняет пределы, если создает и D имеет их.

LaTeX

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

Lean4

/-- `F` preserves the limit of shape `J` if it creates these limits and `D` has them. -/
instance (priority := 100) preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape (F : C ⥤ D)
    [CreatesLimitsOfShape J F] [HasLimitsOfShape J D] : PreservesLimitsOfShape J F where
  -- see Note [lower instance priority]

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