mathlib

77fa4dcf - feat(data/set/intervals/ord_connected): lemmas about `order_dual` etc (#16534)

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)`.