ManifoldSubset.separating_open_supersets

[mkoeppe]

For a finite family of pairwise disjoint compact subsets, separation theorems guarantee the existence of pairwise disjoint open supersets.

We provide a method that returns these open supersets, at least abstractly. In some cases, for example when the restrictions that define the subsets in a common chart are linear inequalities, more concrete constructions are possible.

CC: @egourgoulhon @mjungmath @tscrim

Component: manifolds

Issue created by migration from https://trac.sagemath.org/ticket/31741