Theorem MonotoneOn.sInf_image_Icc

Modification history

2025-07-02 22:40

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

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

Added MonotoneOn.sInf_image_Icc View on Github →