top

Mathlib.CategoryTheory.MorphismProperty.Descent

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

English

If W ≤ Q and P.DescendsAlong Q holds, then P.DescendsAlong W holds.

Русский

Если W ≤ Q и PDescendsAlong Q выполняется, то PDescendsAlong W выполняется.

LaTeX

$$$ [P.DescendsAlong Q] (W \\le Q) \\Rightarrow P.DescendsAlong W$$$

Lean4

instance top : (⊤ : MorphismProperty C).DescendsAlong Q where of_isPullback _ _ _ := trivial

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

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

Разделы

Аффилиация

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