Commit 2022-09-19 07:18 77fa4dcf

feat(data/set/intervals/ord_connected): lemmas about order_dual etc (#16534)

• add dual_interval;
• add ord_connected_preimage for an order_hom_class, use it to golf ord_connected_image;
• add dual_ord_connected_iff and dual_ord_connected;
• one implication from ord_connected_iff_interval_subset_left doesn't need (hx : x ∈ s).