## Stream: general

### Topic: galois correspondences

#### Johan Commelin (Nov 17 2018 at 06:29):

Do we already have the Galois correspondence for set.map and set.comap (aka, range and preimage)?
Is there machinery to glue Galois correspondences together? E.g. I would like to get a Galois correspondence for opens.map and opens.comap more or less for free.

#### Johannes Hölzl (Nov 17 2018 at 09:01):

its between set.image and set.preimage (and there is one between preimage and kern_image f s := {y | ∀x, f x = y → x ∈ s})

#### Johannes Hölzl (Nov 17 2018 at 09:01):

its in data.set.lattice

#### Johan Commelin (Nov 17 2018 at 09:02):

Thanks

Last updated: May 06 2021 at 22:13 UTC