lanLiftUnit_desc

Mathlib.CategoryTheory.Bicategory.Kan.HasKan

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.lanLiftUnit_desc

← MathLib Explorer

English

For HasLeftKanLift f g and s, lanUnit f g ≫ f ◁ lanDesc s = s.unit.

Русский

Для HasLeftKanLift f g и s: lanUnit f g после f ◁ lanDesc s равно s.unit.

LaTeX

$$$\mathrm{lanUnit}(f,g) \circ (f \triangleleft \mathrm{lanDesc}(s)) = s.\mathrm{unit}$$$

Lean4

@[reassoc (attr := simp)]
theorem lanLiftUnit_desc [HasLeftKanLift f g] (s : LeftLift f g) : lanLiftUnit f g ≫ lanLiftDesc s ▷ f = s.unit :=
  (lanLiftIsKan f g).fac s

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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