instIsLeftKanExtensionObjLanAppLanUnit

English

For any F, the left Kan extension object is a left Kan extension with unit given by L.lanUnit.app F.

Русский

Для любого F левое каноническое расширение является левым каноническим расширением, композиция с единицей задаётся L.lanUnit.app F.

LaTeX

$$LeftKanExtensionObjLanAppLanUnit$$

Lean4

instance (F : C ⥤ H) : (L.lan.obj F).IsLeftKanExtension (L.lanUnit.app F) :=
  by
  dsimp [lan, lanUnit]
  infer_instance

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