Theorems · Definition · order theory

Setoid.comap

{α : Type u_1} → {β : Type u_2} → (α → β) → Setoid β → Setoid α

Given a function f : α → β, an equivalence relation r on β induces an equivalence relation on α defined by 'x ≈ y iff f(x) is related to f(y) by r'. See note [reducible non-instances].

Defined in

Mathlib.Data.Setoid.Basic

Cited by

16 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms