isoForkOfι

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Fork.isoForkOfι

Lean4

/-- Every fork is isomorphic to one of the form `Fork.of_ι _ _`. -/
def isoForkOfι (c : Fork f g) : c ≅ Fork.ofι c.ι c.condition :=
  Fork.ext (by simp only [Fork.ofι_pt, Functor.const_obj_obj]; rfl) (by simp)

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

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

Разделы

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

Аффилиация

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