fac_left

Mathlib.CategoryTheory.CommSq

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

English

If we have a lift in a square, then i ∘ lift = f.

Русский

Если есть подъем в квадрате, то i ∘ lift = f.

LaTeX

$$$i \circ lift = f$$$

Lean4

@[reassoc (attr := simp)]
theorem fac_left [hsq : HasLift sq] : i ≫ sq.lift = f :=
  hsq.exists_lift.some.fac_left

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

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

Разделы

Аффилиация

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