Commit 2026-09-10 16:50 b8d3b9bd

feat(Logic/Relation): Map r f g ≤ s ↔ r ≤ s.bicompl f g (#38432) and the dual s ≤ Relation.Map r f g ↔ s.bicompl f g ≤ r which requires f and g to be bijective. Adds Galois{Connection/Insertion/Coinsertion} for the dual. The theorems are specialized to onFun instead of bicompl for when f = g. A GaloisConnection for the iff in the title requires f/g to be bijective, but then we can get an OrderIso which is stronger (see #38499).