Lukas Stevens (Apr 29 2021 at 09:15): 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.
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: Dec 30 2024 at 16:22 UTC