Commit 2023-06-09 16:10 45c9d611

View on Github →

feat: port Analysis.Convex.Measure (#4911)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Measure.lean

added theorem Convex.add_haar_frontier