instHasEqualizerFstPiMapSndPiMap

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Multiequalizer.instHasEqualizerFstPiMapSndPiMap

English

There exists an equalizer of fstPiMap and sndPiMap.

Русский

Существует эллипсоид (равнозначитель) fstPiMap и sndPiMap.

LaTeX

$$$\exists E\,\text{IsEqualizer }(I.fstPiMap,I.sndPiMap)$$$

Lean4

instance : HasEqualizer I.fstPiMap I.sndPiMap :=
  ⟨⟨⟨_, IsLimit.ofPreservesConeTerminal I.multiforkEquivPiFork.functor (limit.isLimit _)⟩⟩⟩

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

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

Разделы

Аффилиация

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