mathlib3 documentation

core / init.data.setoid

source
@[class]
structure setoid (α : Sort u) :
Sort (max 1 u)
Instances of this typeclass
Instances of other typeclasses for setoid
source
@[protected, instance]
def setoid_has_equiv {α : Sort u} [setoid α] :
has_equiv α
Equations
source
@[refl]
theorem setoid.refl {α : Sort u} [setoid α] (a : α) :
a ≈ a
source
@[symm]
theorem setoid.symm {α : Sort u} [setoid α] {a b : α} (hab : a ≈ b) :
b ≈ a
source
@[trans]
theorem setoid.trans {α : Sort u} [setoid α] {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) :
a ≈ c