NRR.Geometry.ConvexBody — interior lemmas

This module develops focused interior lemmas for ConvexBody, especially the ones needed later for halfspace cuts and affine transformations. It provides:

• basic access to an interior point (exists_interior_point, chooseInteriorPoint);
• existence of an open (resp. closed) metric ball inside the body (exists_ball_subset, exists_closedBall_subset, exists_point_strictly_inside_ball);
• stability of nonempty interior under supersets (interior_nonempty_of_superset).

It does not treat affine images (deferred to a separate module), and it adds no new fields to ConvexBody.

Import policy

Following the library-wide policy, Basic.lean already pulls in import Mathlib, so no extra imports are required here; the metric lemmas used (mem_interior_iff_mem_nhds, Metric.isOpen_ball, Metric.mem_ball_self, Metric.closedBall_subset_ball, interior_mono) are all available transitively.

theorem NRR.Geometry.ConvexBody.exists_interior_point {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : ∃ (x : E), x ∈ interior K.carrier

A convex body has an interior point. (Alias of interior_nonempty in existential form.)

noncomputable def NRR.Geometry.ConvexBody.chooseInteriorPoint {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : E

A chosen interior point of a convex body.

Equations

• K.chooseInteriorPoint = ⋯.choose

theorem NRR.Geometry.ConvexBody.choose_interior_point_mem_interior {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : K.chooseInteriorPoint ∈ interior K.carrier

The chosen interior point indeed lies in the interior of the body.

theorem NRR.Geometry.ConvexBody.interior_nonempty_of_superset {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) {s : Set E} (hKs : K.carrier ⊆ s) : (interior s).Nonempty

If a convex body is contained in a set s, then s has nonempty interior.

theorem NRR.Geometry.ConvexBody.exists_ball_subset {E : Type u_1} [PseudoMetricSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : ∃ (x : E) (r : ℝ), 0 < r ∧ Metric.ball x r ⊆ K.carrier

A convex body contains an open metric ball of positive radius.

theorem NRR.Geometry.ConvexBody.exists_closedBall_subset {E : Type u_1} [PseudoMetricSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : ∃ (x : E) (r : ℝ), 0 < r ∧ Metric.closedBall x r ⊆ K.carrier

A convex body contains a closed metric ball of positive radius.

theorem NRR.Geometry.ConvexBody.exists_point_strictly_inside_ball {E : Type u_1} [PseudoMetricSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : ∃ (x : E) (r : ℝ), 0 < r ∧ Metric.closedBall x r ⊆ K.carrier

A halfspace-friendly restatement of exists_closedBall_subset: a convex body contains a closed metric ball of positive radius.