Let E be a finite dimensional real vector space, let μ be a Haar measure on E, let s be a
convex set in E. Then the frontier of s has measure zero (see convex.add_haar_frontier), hence
s is a measure_theory.null_measurable_set (see convex.null_measurable_set).
Haar measure of the frontier of a convex set is zero.
A convex set in a finite dimensional real vector space is null measurable with respect to an
additive Haar measure on this space.