instDecidableRelEquivOfDecidableEq

Mathlib.Data.Ordmap.Ordnode

URI: https://scilib.ai/kg/mathlib#Ordnode.instDecidableRelEquivOfDecidableEq

Lean4

instance [DecidableEq α] : DecidableRel (@Equiv α) := fun x y =>
  inferInstanceAs (Decidable (x.size = y.size ∧ x.toList = y.toList))

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

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

Разделы

Аффилиация

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