mathlib3

c4268a86 - feat(topology,analysis): there exists `y ∈ frontier s` at distance `inf_dist x sᶜ` from `x` (#10976)