mathlib

d565adb7 - feat(analysis/convex/topology): Separating by convex sets (#11458)

feat(analysis/convex/topology): Separating by convex sets (#11458) When `s` is compact, `t` is closed and both are convex, we can find disjoint open convex sets containing `s` and `t`.