instHasLeftKanLiftComp

Mathlib.CategoryTheory.Bicategory.Kan.HasKan

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.LanLift.CommuteWith.instHasLeftKanLiftComp

English

If f,g have HasLeftKanLift and h: x ⟶ c, then HasLeftKanLift f (h ≫ g).

Русский

Если f,g имеют HasLeftKanLift и h: x ⟶ c, то HasLeftKanLift f (h ≫ g).

LaTeX

$$$[HasLeftKanLift f g] \Rightarrow [HasLeftKanLift f (h \gg g)].$$$

Lean4

instance : HasLeftKanLift f (h ≫ g) :=
  (LanLift.CommuteWith.isKan f g h).hasLeftKanLift

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

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

Разделы

Аффилиация

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