Interactions between relation homomorphisms and sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
It is likely that there are better homes for many of these statement,
in files further down the import graph.
subrel r p is the inherited relation on a subset.
The relation embedding from the inherited relation on a subset.
Restrict the codomain of a relation embedding.