mathlib

40de35aa - feat(order/conditionally_complete_lattice, topology/algebra/ordered): inherited order properties for `ord_connected` subset (#3991)

feat(order/conditionally_complete_lattice, topology/algebra/ordered): inherited order properties for `ord_connected` subset (#3991) If `α` is `densely_ordered`, then so is the subtype `s`, for any `ord_connected` subset `s` of `α`. Same result for `order_topology`. Same result for `conditionally_complete_linear_order`, under the hypothesis `inhabited s`.