mathlib

79bc7323 - feat(order/galois_connection): formula for `upper_bounds (l '' s)` (#8478)

feat(order/galois_connection): formula for `upper_bounds (l '' s)` (#8478) * upgrade `galois_connection.upper_bounds_l_image_subset` and `galois_connection.lower_bounds_u_image` to equalities; * prove `bdd_above (l '' s) ↔ bdd_above s` and `bdd_below (u '' s) ↔ bdd_below s`; * move `galois_connection.dual` to the top and use it in some proofs; * use `order_iso.to_galois_connection` to transfer some of these results to `order_iso`s; * rename `rel_iso.to_galois_insertion` to `order_iso.to_galois_insertion`.