preservesLimits_of_evaluation — Mathlib

English

If F: D ⥤ K ⥤ C preserves limits for each evaluation, then it preserves all limits.

Русский

Если F: D ⥤ K ⥤ C сохраняет пределы по каждой оценке, тогда он сохраняет все пределы.

LaTeX

$$$\forall k,\ PreservesLimitsOfSize(J, F, ev_k) \Rightarrow PreservesLimitsOfSize(J, F)$$$

Lean4

/-- `F : D ⥤ K ⥤ C` preserves all limits if it does for each `k : K`. -/
theorem preservesLimits_of_evaluation (F : D ⥤ K ⥤ C)
    (_ : ∀ k : K, PreservesLimitsOfSize.{w', w} (F ⋙ (evaluation K C).obj k)) : PreservesLimitsOfSize.{w', w} F :=
  ⟨fun {L} _ => preservesLimitsOfShape_of_evaluation F L fun _ => PreservesLimitsOfSize.preservesLimitsOfShape⟩

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