A relation on α and β, aka a set-valued function, aka a partial multifunction -
The inverse relation : r.inv x y ↔ r y x. Note that this is not a groupoid inverse.
r.inv x y ↔ r y x
Domain of a relation
Codomain aka range of a relation
Composition of relation; note that it follows the category_theory/ order of arguments.
Image of a set under a relation
Preimage of a set under a relation r. Same as the image of s under r.inv
Core of a set s : set β w.r.t r : rel α β is the set of x : α that are related only
to elements of s.
s : set β
r : rel α β
x : α
Restrict the domain of a relation to a subtype.
The graph of a function as a relation.