top

Mathlib.CategoryTheory.MorphismProperty.Descent

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

English

The top property ⊤ descends along any Q: (⊤).CodescendsAlong Q holds for every Q.

Русский

Свойство верхнего уровня descends along любой Q: (⊤).CodescendsAlong Q истинно для любого Q.

LaTeX

$$$\forall {C} [\mathsf{Category} C], {Q : \mathsf{MorphismProperty} C}, (\top) .CodescendsAlong Q.$$$

Lean4

instance top : (⊤ : MorphismProperty C).CodescendsAlong Q where of_isPushout _ _ _ := trivial

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

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

Разделы

Аффилиация

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