Theorem ContinuousOn.image_Icc_of_monotoneOn

Modification history

2026-07-02 13:28
Mathlib/Topology/Order/Compact.lean
feat(Topology/Order/IntermediateValue): images of intervals under monotone continuous functions (#41130) …
Modified ContinuousOn.image_Icc_of_monotoneOnView on Github →
2025-07-02 22:40
Mathlib/Topology/Order/Compact.lean
feat: the image of an interval under a continuous monotone map is an interval (#26504)
Added ContinuousOn.image_Icc_of_monotoneOnView on Github →