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
.