NRR.Geometry.ConvexBody — bundled compact convex bodies with nonempty interior

This module introduces the central bundled object

NRR.Geometry.ConvexBody E

a compact convex subset of a topological ℝ-module E with nonempty interior. downstream modules are expected to use ConvexBody through the accessor/extensionality API below without ever unfolding its fields.

Relationship to Mathlib's ConvexBody

Mathlib already ships a bundled

_root_.ConvexBody V -- carrier, convex', isCompact', nonempty'

(see Mathlib.Analysis.Convex.Body), but its solidity requirement is only that the carrier be nonempty (nonempty'), not that the interior be nonempty. The fair-partition development needs the stronger solid condition (nonempty interior, hence positive Lebesgue measure in finite dimensions), so we introduce a dedicated bundled structure whose proof field is interior_nonempty'. To avoid clashing with the root ConvexBody used elsewhere in the library, this structure lives in the NRR.Geometry namespace; the two never collide because that namespace is not opened by the modules that use Mathlib's _root_.ConvexBody.

Design notes

• Typeclasses are kept minimal: the whole API only needs [TopologicalSpace E], [AddCommMonoid E], [Module ℝ E] (enough to state Convex ℝ, IsCompact, and interior). Finite dimensionality / inner-product structure is intentionally not required here and is added by downstream modules where genuinely needed.
• We coerce to Set E (via a Coe instance) and provide a Membership instance, but do not coerce ConvexBody to a type.
• No area/perimeter/measure fields, and no separate full-dimensionality field: nonempty interior already encodes solidity.

Import policy

Following the library-wide policy fixed in AI_CONTEXT.md, this file uses the whole-library import Mathlib. The concrete dependencies are lightweight (Convex, IsCompact, interior, Set membership/extensionality).

structure NRR.Geometry.ConvexBody (E : Type u_2) [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] : Type u_2

A convex body (in the solid sense used throughout this development): a compact convex subset of a topological ℝ-module with nonempty interior.

• carrier : Set E

  The underlying set of points of the convex body.

• convex' : Convex ℝ self.carrier

  The carrier is convex.

• isCompact' : IsCompact self.carrier

  The carrier is compact.

• interior_nonempty' : (interior self.carrier).Nonempty

  The carrier has nonempty interior (solidity).

@[instance_reducible]

instance NRR.Geometry.ConvexBody.instCoeSet {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] : Coe (ConvexBody E) (Set E)

Coercion of a convex body to its underlying set of points.

Equations

• NRR.Geometry.ConvexBody.instCoeSet = { coe := NRR.Geometry.ConvexBody.carrier }

@[instance_reducible]

instance NRR.Geometry.ConvexBody.instMembership {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] : Membership E (ConvexBody E)

Membership x ∈ K unfolds to membership in the carrier.

Equations

• NRR.Geometry.ConvexBody.instMembership = { mem := fun (K : NRR.Geometry.ConvexBody E) (x : E) => x ∈ K.carrier }

@[simp]

theorem NRR.Geometry.ConvexBody.mem_coe {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) (x : E) : x ∈ K.carrier ↔ x ∈ K

theorem NRR.Geometry.ConvexBody.convex {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : Convex ℝ K.carrier

The carrier of a convex body is convex.

theorem NRR.Geometry.ConvexBody.isCompact {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : IsCompact K.carrier

The carrier of a convex body is compact.

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

The carrier of a convex body has nonempty interior.

theorem NRR.Geometry.ConvexBody.nonempty {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : K.carrier.Nonempty

A convex body is nonempty (its interior is nonempty and the interior is contained in it).

theorem NRR.Geometry.ConvexBody.ext {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] {K L : ConvexBody E} (h : K.carrier = L.carrier) : K = L

Extensionality: two convex bodies with equal carriers are equal. The remaining proof fields are equal by proof irrelevance.

theorem NRR.Geometry.ConvexBody.ext_iff {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] {K L : ConvexBody E} : K = L ↔ K.carrier = L.carrier

theorem NRR.Geometry.ConvexBody.ext_iff_mem {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] {K L : ConvexBody E} : K = L ↔ ∀ (x : E), x ∈ K.carrier ↔ x ∈ L.carrier

Membership extensionality: two convex bodies are equal iff they have the same points.

@[simp]

theorem NRR.Geometry.ConvexBody.coe_mk {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] (s : Set E) (hconv : Convex ℝ s) (hcomp : IsCompact s) (hint : (interior s).Nonempty) : { carrier := s, convex' := hconv, isCompact' := hcomp, interior_nonempty' := hint }.carrier = s