mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(analysis/convex/side): connectedness of sides

Open jsm28 opened this issue 3 years ago • 0 comments

Add lemmas that, in a real normed space, the sets of points on the same side of an affine subspace as a given point, or on the opposite side from a given point, are connected (or, under weaker conditions, preconnected).

Open in Gitpod

jsm28 avatar Oct 12 '22 19:10 jsm28