stone_separation): Stone's separation theorem (#14677)

Commit

3 years ago

feat(analysis/convex/stone_separation): Stone's separation theorem (#14677) Disjoint convexes can be separated by a convex whose complement is also convex.

Author

YaelDillies

Parents

4111ed94

mathlib 381733a5 - feat(analysis/convex/stone_separation): Stone's separation theorem (#14677)

mathlib
381733a5 - feat(analysis/convex/stone_separation): Stone's separation theorem (#14677)