Commit 2025-07-02 22:40 71f32514

View on Github →

feat: the image of an interval under a continuous monotone map is an interval (#26504)

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem AntitoneOn.sInf_image_Icc

added theorem AntitoneOn.sSup_image_Icc

added theorem MonotoneOn.sInf_image_Icc

added theorem MonotoneOn.sSup_image_Icc

Modified Mathlib/Topology/FiberBundle/Basic.lean

Modified Mathlib/Topology/Order/Compact.lean

added theorem ContinuousOn.image_Icc_of_antitoneOn

added theorem ContinuousOn.image_Icc_of_monotoneOn