a convex set is null measurable

Stream: Is there code for X?

[Yury G. Kudryashov]

Do we have a proof of the following fact: if s is a convex set in a finite dimensional real vector space, then its boundary has Lebesgue (additive Haar) measure zero, hence the set is a null_measurable_set?

[Yury G. Kudryashov]

I can't find it in mathlib but possibly some project has it. @Patrick Massot, do you have it in the sphere eversion project? If not, then I'll formalize it.

[Patrick Massot]

We have nothing like this in the sphere eversion project.

[Yury G. Kudryashov]

What about "a convex set with empty interior is a subset of a hyperplane"?

[Yaël Dillies]

Sounds like @Oliver Nash's stuff. We wanted stuff similar to that for Sperner's Lemma.

[Oliver Nash]

Yep, I imagine docs#interior_convex_hull_aff_basis should help.