OAI/Geometry/RCD/Metric/ConvexImageNoSupport.lean
1 declarations, 0 contain sorry, 0 declared as axioms
A convex image with no supporting direction has interior
- theorem
OAI.RegularPointCoordinates.convex_image_interior_of_no_supportline 12