mathlib

9524dee3 - feat(topology): real.image_Icc (#3224)

feat(topology): real.image_Icc (#3224) The image of a segment under a real-valued continuous function is a segment. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>