setoid

Mathlib.Order.Antisymmetrization

URI: https://scilib.ai/kg/mathlib#AntisymmRel.setoid

Lean4

/-- The antisymmetrization relation as an equivalence relation. -/
@[simps]
def setoid : Setoid α :=
  ⟨AntisymmRel r, .refl r, .symm, .trans⟩

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

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

Разделы

Аффилиация

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