mathlib documentation

core / init.data.setoid

@[class]

structure setoid (α : Sort u) :

Sort (max 1 u)

r : α → α → Prop
iseqv : equivalence setoid.r

Instances

@[protected, instance]

def setoid_has_equiv {α : Sort u} [setoid α] :

Equations

setoid_has_equiv = {equiv := setoid.r _inst_1}

theorem setoid.refl {α : Sort u} [setoid α] (a : α) :

a ≈ a

theorem setoid.symm {α : Sort u} [setoid α] {a b : α} (hab : a ≈ b) :

b ≈ a

theorem setoid.trans {α : Sort u} [setoid α] {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) :

a ≈ c