Almost every point of a convex set is interior #
The frontier of a convex set in a finite-dimensional real normed space is null for any additive
Haar measure (Convex.addHaar_frontier). Consequently, almost every point of the set is in its
interior.
theorem
Convex.ae_mem_interior
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[MeasurableSpace E]
[BorelSpace E]
{μ : MeasureTheory.Measure E}
[μ.IsAddHaarMeasure]
{s : Set E}
(hs : Convex ℝ s)
:
Almost every point of a convex set in a finite-dimensional real normed space is an interior point, since the frontier of the set is null for every additive Haar measure.