Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-03 13:41 74037cba

View on Github →

feat(topology/algebra/ordered): IVT for two functions (#2933) Also rename some is_connected_I* lemmas to is_preconnected_I*.

Estimated changes

modified theorem closure_le_eq
modified theorem closure_lt_subset_le
modified theorem intermediate_value_univ
added theorem is_closed.is_closed_le
deleted theorem is_connected_Icc
deleted theorem is_connected_Ioo
added theorem is_preconnected_Icc
added theorem is_preconnected_Ioo
modified theorem tendsto_abs_at_top_at_top