of_le

Mathlib.CategoryTheory.MorphismProperty.Descent

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

English

If W ≤ Q then P.DescendsAlong W follows from P.DescendsAlong Q.

Русский

Если W ≤ Q, то из P.DescendsAlong Q следует P.DescendsAlong W.

LaTeX

$$$ [P.DescendsAlong Q] \\implies [W ≤ Q] \\Rightarrow P.DescendsAlong W$$$

Lean4

theorem of_le [P.DescendsAlong Q] (hle : W ≤ Q) : P.DescendsAlong W where
  of_isPullback h hg hfst := DescendsAlong.of_isPullback h (hle _ hg) hfst

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

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

Разделы

Аффилиация

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