Galois connection induced by an arbitrary relation

Stream: mathlib4

[Anthony Bordg]

Following ideas I learned from Olivia Caramello and Laurent Lafforgue, I formalised the Galois connection induced by an arbitrary relation between a pair of sets or classes , and the inverse bijections this induces between a pair of sets of associated "fixed points".
This formalisation is rather short, 107 lines including the header, but the file Mathlib/Order/GaloisConnection.leanhas already 947 lines, so I started a new file.
@maintainers Do you want me to include this in GaloisConnection.lean or keep this in a separate file in Mathlib/Order before making a PR?

[Matthew Ballard]

I think a separate file is appropriate

[Riccardo Brasca]

I agree. We can even split GaloisConnection.

[Oliver Nash]

Please be mindful when using the maintainer handle to summon our attention. It triggers a notification for numerous busy people. I’m not sure it was required here.

[Anthony Bordg]

PR #14908