Commit 2022-05-04 15:53 d565adb7

View on Github →

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.

Estimated changes

Modified src/analysis/convex/basic.lean

modified theorem convex.neg

modified theorem convex_Inter

added theorem convex_Inter₂

Modified src/analysis/convex/topology.lean

added theorem convex.cthickening

added theorem convex.thickening

modified theorem convex_on_dist

modified theorem convex_on_norm

added theorem disjoint.exists_open_convexes

Modified src/topology/metric_space/hausdorff_distance.lean

added theorem disjoint.exists_cthickenings

added theorem disjoint.exists_thickenings

added theorem emetric.exists_pos_forall_le_edist