f'

Mathlib.CategoryTheory.GlueData

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GlueData'.f'

Lean4

/-- (Implementation detail) the constructed `GlueData.f` from a `GlueData'`. -/
abbrev f' (D : GlueData' C) (i j : D.J) : (if h : i = j then D.U i else D.V i j h) ⟶ D.U i :=
  if h : i = j then eqToHom (dif_pos h) else eqToHom (dif_neg h) ≫ D.f i j h

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

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

Разделы

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

Аффилиация

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