hasLimitsOfSize — Mathlib

English

Let J be a type indexing shape, with J having a category structure. If A and B have all limits of size w, w' and R preserves limits of size w, w', then the comma category has limits of size w, w'.

Русский

Пусть J индексирует форму пределов, и J имеет структуру категории. Если A и B имеют пределы размера w, w' и R сохраняет пределы размера w, w', то запятая-категория имеет пределы размера w, w'.

LaTeX

$$$\\operatorname{HasLimitsOfSize}(J,A) \\land \\operatorname{HasLimitsOfSize}(J,B) \\land \\operatorname{PreservesLimitsOfSize}(J,R) \\Rightarrow \\operatorname{HasLimitsOfSize}(J, \\mathrm{Comma}(L,R))$$$

Lean4

instance hasLimitsOfSize [HasLimitsOfSize.{w, w'} A] [HasLimitsOfSize.{w, w'} B] [PreservesLimitsOfSize.{w, w'} R] :
    HasLimitsOfSize.{w, w'} (Comma L R) :=
  ⟨fun _ _ => inferInstance⟩

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