Stream: Beginner Questions

Topic: Lifting a relation to a quotient


view this post on Zulip Lukas Stevens (Apr 29 2021 at 09:15):

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.

view this post on Zulip Lukas Stevens (Apr 29 2021 at 09:21):

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: Sep 25 2022 at 23:25 UTC