Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-21 13:16 de13786a

View on Github →

chore(topology/algebra/ordered): move IVT to a new file (#9792)

Estimated changes

Modified src/topology/algebra/ordered/basic.lean

deleted theorem continuous.surjective'

deleted theorem continuous.surjective

deleted theorem continuous_on.surj_on_of_tendsto'

deleted theorem continuous_on.surj_on_of_tendsto

deleted theorem eq_Icc_cInf_cSup_of_connected_bdd_closed

deleted theorem intermediate_value_Icc'

deleted theorem intermediate_value_Icc

deleted theorem intermediate_value_Ico'

deleted theorem intermediate_value_Ico

deleted theorem intermediate_value_Ioc'

deleted theorem intermediate_value_Ioc

deleted theorem intermediate_value_Ioo'

deleted theorem intermediate_value_Ioo

deleted theorem intermediate_value_interval

deleted theorem intermediate_value_univ

deleted theorem intermediate_value_univ₂

deleted theorem intermediate_value_univ₂_eventually₁

deleted theorem intermediate_value_univ₂_eventually₂

deleted theorem is_closed.Icc_subset_of_forall_exists_gt

deleted theorem is_closed.Icc_subset_of_forall_mem_nhds_within

deleted theorem is_closed.mem_of_ge_of_forall_exists_gt

deleted theorem is_connected.Icc_subset

deleted theorem is_connected.Ioo_cInf_cSup_subset

deleted theorem is_preconnected.Icc_subset

deleted theorem is_preconnected.Iio_cSup_subset

deleted theorem is_preconnected.Ioi_cInf_subset

deleted theorem is_preconnected.eq_univ_of_unbounded

deleted theorem is_preconnected.intermediate_value

deleted theorem is_preconnected.intermediate_value_Ici

deleted theorem is_preconnected.intermediate_value_Ico

deleted theorem is_preconnected.intermediate_value_Iic

deleted theorem is_preconnected.intermediate_value_Iii

deleted theorem is_preconnected.intermediate_value_Iio

deleted theorem is_preconnected.intermediate_value_Ioc

deleted theorem is_preconnected.intermediate_value_Ioi

deleted theorem is_preconnected.intermediate_value_Ioo

deleted theorem is_preconnected.intermediate_value₂

deleted theorem is_preconnected.intermediate_value₂_eventually₁

deleted theorem is_preconnected.intermediate_value₂_eventually₂

deleted theorem is_preconnected.mem_intervals

deleted theorem is_preconnected.ord_connected

deleted theorem is_preconnected_Icc

deleted theorem is_preconnected_Ici

deleted theorem is_preconnected_Ico

deleted theorem is_preconnected_Iic

deleted theorem is_preconnected_Iio

deleted theorem is_preconnected_Ioc

deleted theorem is_preconnected_Ioi

deleted theorem is_preconnected_Ioo

deleted theorem is_preconnected_iff_ord_connected

deleted theorem is_preconnected_interval

deleted theorem mem_range_of_exists_le_of_exists_ge

deleted theorem set.ord_connected.is_preconnected

deleted theorem set_of_is_preconnected_eq_of_ordered

deleted theorem set_of_is_preconnected_subset_of_ordered

Modified src/topology/algebra/ordered/compact.lean

Created src/topology/algebra/ordered/intermediate_value.lean

added theorem continuous.surjective'

added theorem continuous.surjective

added theorem continuous_on.surj_on_of_tendsto'

added theorem continuous_on.surj_on_of_tendsto

added theorem eq_Icc_cInf_cSup_of_connected_bdd_closed

added theorem intermediate_value_Icc'

added theorem intermediate_value_Icc

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_interval

added theorem intermediate_value_univ

added theorem intermediate_value_univ₂

added theorem intermediate_value_univ₂_eventually₁

added theorem intermediate_value_univ₂_eventually₂

added theorem is_closed.Icc_subset_of_forall_exists_gt

added theorem is_closed.Icc_subset_of_forall_mem_nhds_within

added theorem is_closed.mem_of_ge_of_forall_exists_gt

added theorem is_connected.Icc_subset

added theorem is_connected.Ioo_cInf_cSup_subset

added theorem is_preconnected.Icc_subset

added theorem is_preconnected.Iio_cSup_subset

added theorem is_preconnected.Ioi_cInf_subset

added theorem is_preconnected.eq_univ_of_unbounded

added theorem is_preconnected.intermediate_value

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₂

added theorem is_preconnected.intermediate_value₂_eventually₁

added theorem is_preconnected.intermediate_value₂_eventually₂

added theorem is_preconnected.mem_intervals

added theorem is_preconnected.ord_connected

added theorem is_preconnected_Icc

added theorem is_preconnected_Ici

added theorem is_preconnected_Ico

added theorem is_preconnected_Iic

added theorem is_preconnected_Iio

added theorem is_preconnected_Ioc

added theorem is_preconnected_Ioi

added theorem is_preconnected_Ioo

added theorem is_preconnected_iff_ord_connected

added theorem is_preconnected_interval

added theorem mem_range_of_exists_le_of_exists_ge

added theorem set.ord_connected.is_preconnected

added theorem set_of_is_preconnected_eq_of_ordered

added theorem set_of_is_preconnected_subset_of_ordered