Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-04 11:19 ee58d669

View on Github →

feat(topology): variations on the intermediate value theorem (#6789)

Estimated changes

Modified src/order/filter/basic.lean

added theorem filter.comap_coe_ne_bot_of_le_principal

added theorem filter.eventually_comap'

Modified src/topology/algebra/ordered.lean

added theorem eventually_ge_of_tendsto_gt

added theorem eventually_le_of_tendsto_lt

added theorem intermediate_value_Ico'

added theorem intermediate_value_Ico

added theorem intermediate_value_Ioc'

added theorem intermediate_value_Ioc

added theorem intermediate_value_Ioo'

added theorem intermediate_value_Ioo

added theorem intermediate_value_univ₂_eventually₁

added theorem intermediate_value_univ₂_eventually₂

added theorem is_preconnected.intermediate_value_Ici

added theorem is_preconnected.intermediate_value_Ico

added theorem is_preconnected.intermediate_value_Iic

added theorem is_preconnected.intermediate_value_Iii

added theorem is_preconnected.intermediate_value_Iio

added theorem is_preconnected.intermediate_value_Ioc

added theorem is_preconnected.intermediate_value_Ioi

added theorem is_preconnected.intermediate_value_Ioo

added theorem is_preconnected.intermediate_value₂_eventually₁

added theorem is_preconnected.intermediate_value₂_eventually₂

added theorem left_nhds_within_Ioc_ne_bot

added theorem left_nhds_within_Ioo_ne_bot

added theorem right_nhds_within_Ico_ne_bot

added theorem right_nhds_within_Ioo_ne_bot