setoid

Mathlib.CategoryTheory.Abelian.Pseudoelements

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.Pseudoelement.setoid

Lean4

/-- The arrows with codomain `P` equipped with the equivalence relation of being pseudo-equal. -/
def setoid (P : C) : Setoid (Over P) :=
  ⟨_, ⟨pseudoEqual_refl, @pseudoEqual_symm _ _ _, @pseudoEqual_trans _ _ _ _⟩⟩

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

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

Разделы

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

Аффилиация

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