mathlib

8d54d527 - chore(topology/algebra/ordered): generalize `intermediate_value_Icc` etc (#5235)

chore(topology/algebra/ordered): generalize `intermediate_value_Icc` etc (#5235) Several lemmas assumed that the codomain is a conditionally complete linear order while actually the statements are true for a linear order. Also introduce `mem_range_of_exists_le_of_exists_ge` and use it in `surjective_of_continuous`.