mathlib

c64fb26a - feat(topology/algebra/order/intermediate_value): intervals are connected (#16473)

feat(topology/algebra/order/intermediate_value): intervals are connected (#16473) `topology.algebra.order.intermediate_value` has a series of lemmas that different kinds of intervals are preconnected. Add a corresponding series of lemmas that intervals are connected (with appropriate extra conditions on the order or the endpoints as needed).