mathlib documentation

core / init.data.setoid

@[protected, instance]
def setoid_has_equiv {α : Sort u} [setoid α] :
Equations
@[refl]
theorem setoid.refl {α : Sort u} [setoid α] (a : α) :
a a
@[symm]
theorem setoid.symm {α : Sort u} [setoid α] {a b : α} (hab : a b) :
b a
@[trans]
theorem setoid.trans {α : Sort u} [setoid α] {a b c : α} (hab : a b) (hbc : b c) :
a c