Commit 2022-09-13 09:02 c64fb26a
View on Github →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).