Commit 2026-07-02 13:28 4f548c10

View on Github →

feat(Topology/Order/IntermediateValue): images of intervals under monotone continuous functions (#41130) Add ContinuousOn.image_{Icc,Ico,Ioc,Ioo,uIcc,Ici,Iic,Ioi,Iio}_of_{monotone,antitone,strictMono,strictAnti}On, computing the image of a (bounded or unbounded) interval under a monotone/antitone continuous map, together with the unbounded intermediate value theorems intermediate_value_{Ici,Iic,Ioi,Iio} (and primed variants) they build on.

Estimated changes

Modified Mathlib/Topology/Order/Compact.lean

deleted theorem ContinuousOn.image_Icc_of_antitoneOn

deleted theorem ContinuousOn.image_Icc_of_monotoneOn

Modified Mathlib/Topology/Order/IntermediateValue.lean

added theorem Continuous.image_Icc_of_strictMono

added theorem Continuous.image_Ico_of_strictMono

added theorem Continuous.image_Ioc_of_strictMono

added theorem Continuous.image_Ioo_of_strictMono

added theorem ContinuousOn.image_Icc_of_antitoneOn

added theorem ContinuousOn.image_Icc_of_monotoneOn

added theorem ContinuousOn.image_Ici_of_antitoneOn

added theorem ContinuousOn.image_Ici_of_monotoneOn

added theorem ContinuousOn.image_Ico_of_strictAntiOn

added theorem ContinuousOn.image_Ico_of_strictMonoOn

added theorem ContinuousOn.image_Iic_of_antitoneOn

added theorem ContinuousOn.image_Iic_of_monotoneOn

added theorem ContinuousOn.image_Iio_of_strictAntiOn

added theorem ContinuousOn.image_Iio_of_strictMonoOn

added theorem ContinuousOn.image_Ioc_of_strictAntiOn

added theorem ContinuousOn.image_Ioc_of_strictMonoOn

added theorem ContinuousOn.image_Ioi_of_strictAntiOn

added theorem ContinuousOn.image_Ioi_of_strictMonoOn

added theorem ContinuousOn.image_Ioo_of_strictAntiOn

added theorem ContinuousOn.image_Ioo_of_strictMonoOn

added theorem ContinuousOn.image_uIcc_of_antitoneOn

added theorem ContinuousOn.image_uIcc_of_monotoneOn

added theorem intermediate_value_Ici'

added theorem intermediate_value_Ici

added theorem intermediate_value_Iic'

added theorem intermediate_value_Iic

added theorem intermediate_value_Iio'

added theorem intermediate_value_Iio

added theorem intermediate_value_Ioi'

added theorem intermediate_value_Ioi