Commit 2023-04-16 16:21 f25608ff

View on Github →

feat: port Analysis.Convex.Body (#3431)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Body.lean

added theorem ConvexBody.coe_add

added theorem ConvexBody.coe_mk

added theorem ConvexBody.coe_nsmul

added theorem ConvexBody.coe_smul'

added theorem ConvexBody.coe_smul

added theorem ConvexBody.coe_zero

added theorem ConvexBody.hausdorffDist_coe

added theorem ConvexBody.hausdorffEdist_coe

added theorem ConvexBody.hausdorffEdist_ne_top

added structure ConvexBody