mathlib3

3398efa6 - feat(topology/homeomorph): homeo of continuous equivalence from compact to T2 (#11072)