Commit 2023-04-24 22:52 3393c046

View on Github →

feat: port Analysis.Convex.Normed (#3626)

Estimated changes

added theorem Convex.cthickening
added theorem Convex.thickening
added theorem bounded_convexHull
added theorem convexHull_diam
added theorem convexHull_ediam
added theorem convexOn_dist
added theorem convexOn_norm
added theorem convexOn_univ_dist
added theorem convexOn_univ_norm
added theorem convex_ball
added theorem convex_closedBall