hasColimit_mapGlueData_diagram — Mathlib

English

Under the stated assumptions, the diagram of the mapped glue data has a multicoequalizer.

Русский

При данных предположениях диаграмма отображённых данных сцепления имеет мультиеквализер.

LaTeX

$$$\\text{HasMulticoequalizer}((D.mapGlueData F).diagram)$$$

Lean4

theorem hasColimit_mapGlueData_diagram : HasMulticoequalizer (D.mapGlueData F).diagram :=
  hasColimit_of_iso (D.diagramIso F).symm

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