fac_right

Mathlib.CategoryTheory.CommSq

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CommSq.fac_right

English

If there is a lift, then lift ∘ p = g.

Русский

Если есть подъём, то lift ∘ p = g.

LaTeX

$$$lift \circ p = g$$$

Lean4

@[reassoc (attr := simp)]
theorem fac_right [hsq : HasLift sq] : sq.lift ≫ p = g :=
  hsq.exists_lift.some.fac_right

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

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

Разделы

Аффилиация

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