instHasLimitsOfSizeDiscretePUnit — Mathlib

English

The discrete category on the unit type PUnit has limits of every size; i.e., for any small category J, the functor category J ⥤ Discrete PUnit has a limit.

Русский

Дискретная категория над единичным типом PUnit имеет пределы любого размера; т.е. для любого малого категориального множества J категория функционалов J ⥤ Discrete PUnit имеет предел.

LaTeX

$$HasLimitsOfSize.{v', v} (Discrete PUnit)$$

Lean4

instance : HasLimitsOfSize.{v', v} (Discrete PUnit) :=
  ⟨fun _ _ => ⟨fun _ => ⟨punitCone, punitConeIsLimit⟩⟩⟩

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