Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes