mathlib

2aebabca - feat(topology/continuous_function/basic): add `continuous_map.Icc_extend` (#8952)