NRR.Geometry.ConvexBody — positive area implies nonempty interior

This module proves that a compact convex planar set with positive (Lebesgue) area has nonempty interior.

The argument is the contrapositive: a convex set in the plane with empty interior has affine span strictly smaller than the whole plane (Convex.interior_nonempty_iff_affineSpan_eq_top), hence is contained in an affine line {x | ⟪u, x⟫ = c} with u ≠ 0. Such a line is Lebesgue-null (NRR.Halfspace.hyperplane_null, the project), so the set has zero area, contradicting positivity.

The compactness hypothesis is retained on the public statements for a uniform public interface; it is not actually needed for the proof (only convexity and finite-dimensionality of the plane are used).

theorem NRR.Geometry.ConvexBody.convex_emptyInterior_subset_affineLine {S : Set Plane} (hconv : Convex ℝ S) (hint : interior S = ∅) : ∃ (u : Plane) (c : ℝ), u ≠ 0 ∧ S ⊆ {x : Plane | inner ℝ u x = c}

A compact convex planar set with empty interior is contained in an affine line {x | ⟪u, x⟫ = c} with nonzero normal u.

The compactness hypothesis is not used; it is retained for a uniform interface.

theorem NRR.Geometry.ConvexBody.interior_nonempty_of_convex_positive_area {S : Set Plane} (hconv : Convex ℝ S) (harea : 0 < (MeasureTheory.volume S).toReal) : (interior S).Nonempty

A convex planar set with positive area has nonempty interior.