reflects_limits_subsingleton

Mathlib.CategoryTheory.Limits.Preserves.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.reflects_limits_subsingleton

English

If F reflects limits of shape J, then ReflectsLimit K F holds for any K.

Русский

Если F отражает предел по форме J, то ReflectsLimit K F выполняется для любой K.

LaTeX

$$$ [\\text{ReflectsLimitsOfShape } J F] \\Rightarrow \\text{ReflectsLimit } K F. $$$

Lean4

instance reflects_limits_subsingleton (F : C ⥤ D) : Subsingleton (ReflectsLimitsOfSize.{w', w} F) := by constructor;
  rintro ⟨a⟩ ⟨b⟩; congr!

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru