Is there theory about lifting a relation to a quotient somewhere? I mean something like this:

```
lemma "equiv UNIV eq"
definition "lifted r = {(eq `` {x}, eq `` {y}) |x y. (x, y) ∈ r}"
```

I have only found `Equiv_Relations.proj`

so far.

I have now found `BNF_Wellorder_Constructions.dir_image`

and `BNF_Greatest_Fixpoint.relImage`

but they are probably not intended to be used directly.

Last updated: Jun 07 2023 at 03:21 UTC