limitsOfShape_le

Mathlib.CategoryTheory.MorphismProperty.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.limitsOfShape_le

English

If W is stable under base change, then W.limitsOfShape J ≤ W for all J.

Русский

Если W устойчива к базовым изменениям, то W.limitsOfShape J ≤ W для всех J.

LaTeX

$$[W.IsStableUnderBaseChange] ⇒ [W.limitsOfShape J] ≤ W$$

Lean4

theorem limitsOfShape_le [W.IsStableUnderLimitsOfShape J] : W.limitsOfShape J ≤ W := by
  rwa [← isStableUnderLimitsOfShape_iff_limitsOfShape_le]

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

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

Разделы

Аффилиация

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