Theorem ContinuousOn.image_Ici_of_antitoneOn

Modification history

2026-07-02 13:28
Mathlib/Topology/Order/IntermediateValue.lean
feat(Topology/Order/IntermediateValue): images of intervals under monotone continuous functions (#41130) …
Added ContinuousOn.image_Ici_of_antitoneOnView on Github →