Commit 2023-02-06 08:18 7fedc16a

View on Github →

feat: port Topology.Algebra.Order.IntermediateValue (#2085)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Order/IntermediateValue.lean

added theorem Continuous.surjective'

added theorem Continuous.surjective

added theorem ContinuousOn.surjOn_Icc

added theorem ContinuousOn.surjOn_of_tendsto'

added theorem ContinuousOn.surjOn_of_tendsto

added theorem ContinuousOn.surjOn_uIcc

added theorem IsClosed.Icc_subset_of_forall_exists_gt

added theorem IsClosed.Icc_subset_of_forall_mem_nhdsWithin

added theorem IsClosed.mem_of_ge_of_forall_exists_gt

added theorem IsConnected.Icc_subset

added theorem IsConnected.Ioo_cinfₛ_csupₛ_subset

added theorem IsPreconnected.Icc_subset

added theorem IsPreconnected.Iio_csupₛ_subset

added theorem IsPreconnected.Ioi_cinfₛ_subset

added theorem IsPreconnected.eq_univ_of_unbounded

added theorem IsPreconnected.intermediate_value

added theorem IsPreconnected.intermediate_value_Ici

added theorem IsPreconnected.intermediate_value_Ico

added theorem IsPreconnected.intermediate_value_Iic

added theorem IsPreconnected.intermediate_value_Iii

added theorem IsPreconnected.intermediate_value_Iio

added theorem IsPreconnected.intermediate_value_Ioc

added theorem IsPreconnected.intermediate_value_Ioi

added theorem IsPreconnected.intermediate_value_Ioo

added theorem IsPreconnected.intermediate_value₂

added theorem IsPreconnected.intermediate_value₂_eventually₁

added theorem IsPreconnected.intermediate_value₂_eventually₂

added theorem IsPreconnected.mem_intervals

added theorem IsPreconnected.ordConnected

added theorem Set.OrdConnected.isPreconnected

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_uIcc

added theorem intermediate_value_univ

added theorem intermediate_value_univ₂

added theorem intermediate_value_univ₂_eventually₁

added theorem intermediate_value_univ₂_eventually₂

added theorem isConnected_Icc

added theorem isConnected_Ici

added theorem isConnected_Ico

added theorem isConnected_Iic

added theorem isConnected_Iio

added theorem isConnected_Ioc

added theorem isConnected_Ioi

added theorem isConnected_Ioo

added theorem isPreconnected_Icc

added theorem isPreconnected_Icc_aux

added theorem isPreconnected_Ici

added theorem isPreconnected_Ico

added theorem isPreconnected_Iic

added theorem isPreconnected_Iio

added theorem isPreconnected_Ioc

added theorem isPreconnected_Ioi

added theorem isPreconnected_Ioo

added theorem isPreconnected_iff_ordConnected

added theorem isPreconnected_uIcc

added theorem mem_range_of_exists_le_of_exists_ge

added theorem setOf_isPreconnected_eq_of_ordered

added theorem setOf_isPreconnected_subset_of_ordered

Modified Mathlib/Topology/Order/Basic.lean

added theorem nhdsWithin_Iio_neBot'

deleted theorem nhdsWithin_Iio_ne_bot'

added theorem nhdsWithin_Iio_self_neBot'

deleted theorem nhdsWithin_Iio_self_ne_bot'

added theorem nhdsWithin_Ioi_self_neBot'

deleted theorem nhdsWithin_Ioi_self_ne_bot'