instHasColimitsOfSize — Mathlib

English

If D has colimits of a given size, then HasColimitsOfSize (Sh(J,D)).

Русский

Если D имеет колимиты заданного размера, то у шейфов J D существуют колимиты соответствующего размера.

LaTeX

$$$(\text{HasColimitsOfSize } {u_1,u_2} D) \Rightarrow (\text{HasColimitsOfSize } {u_1,u_2} (\mathrm{Sh}(J,D))).$$$

Lean4

instance [HasColimitsOfSize.{u₁, u₂} D] : HasColimitsOfSize.{u₁, u₂} (Sheaf J D) :=
  ⟨inferInstance⟩

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