Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-25 15:23 9f75d75a

View on Github →

feat(analysis/convex/measure): a convex set is null-measurable (#13138)

Estimated changes

Created src/analysis/convex/measure.lean

added theorem convex.add_haar_frontier

Modified src/analysis/convex/topology.lean

added theorem convex.closure_subset_image_homothety_interior_of_one_lt

Modified src/data/set/basic.lean

added theorem subtype.preimage_coe_inter_self

Modified src/topology/continuous_on.lean

added theorem frontier_inter_open_inter