Commit 2021-08-01 03:28 79bc7323

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_isos;
• rename rel_iso.to_galois_insertion to order_iso.to_galois_insertion.