preservesFiniteLimits — Mathlib

English

If a functor preserves limits of size (0,0), it preserves finite limits.

Русский

Если функтор сохраняет пределы размера (0,0), он сохраняет конечные пределы.

LaTeX

$$PreservesFiniteLimits(F) from PreservesLimitsOfSize(0,0)(F)$$

Lean4

instance (priority := 120) preservesFiniteLimits (F : C ⥤ D) [PreservesLimitsOfSize.{0, 0} F] :
    PreservesFiniteLimits F :=
  PreservesLimitsOfSize.preservesFiniteLimits F

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