# mathlibdocumentation

analysis.convex.measure

# Convex sets are null-measurable #

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).

theorem convex.add_haar_frontier {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) {s : set E} (hs : s) :
μ (frontier s) = 0

Haar measure of the frontier of a convex set is zero.

@[protected]
theorem convex.null_measurable_set {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) {s : set E} (hs : s) :

A convex set in a finite dimensional real vector space is null measurable with respect to an additive Haar measure on this space.