Commit 2020-12-06 20:08 8d54d527
View on Github →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.