Theorems · Theorem · order theory

Setoid.eqvGen_eq

∀ {α : Type u_1} (r : α → α → Prop), Relation.EqvGen.setoid r = sInf {s | ∀ ⦃x y : α⦄, r x y → s x y}

The inductively defined equivalence closure of a binary relation r is the infimum of the set of all equivalence relations containing r.

Defined in

Mathlib.Data.Setoid.Basic

Cited by

4 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Quot.sound