NRR.Geometry.ConvexBody — topological accessor API

This module packages the topological facts about a ConvexBody (compactness, closedness, boundedness, nonemptiness, interior membership, closure and frontier) into a stable, namespaced accessor API. Downstream modules should obtain these facts through the wrappers below and never unfold the ConvexBody structure to get them.

Some facts are already provided in NRR.Geometry.ConvexBody.Basic (ConvexBody.isCompact, ConvexBody.nonempty, ConvexBody.interior_nonempty); those are re-used here rather than duplicated.

Import policy

Following the library-wide policy, Basic.lean already pulls in import Mathlib, so no extra imports are required here; the topological lemmas used (IsCompact.isClosed, IsCompact.isBounded, IsClosed.closure_eq, IsClosed.frontier_subset, interior_subset) are all available transitively.

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

The interior of a convex body is contained in the body.

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

A point in the interior of a convex body is a point of the body.

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

A convex body has an element.

theorem NRR.Geometry.ConvexBody.exists_mem_interior {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.

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

A convex body is closed (compact in a Hausdorff space).

@[simp]

theorem NRR.Geometry.ConvexBody.closure_eq {E : Type u_1} [TopologicalSpace E] [T2Space E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : closure K.carrier = K.carrier

The closure of a convex body is the body itself, since it is closed.

theorem NRR.Geometry.ConvexBody.frontier_subset {E : Type u_1} [TopologicalSpace E] [T2Space E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : frontier K.carrier ⊆ K.carrier

The frontier of a convex body is contained in the body, since it is closed.

theorem NRR.Geometry.ConvexBody.isBounded {E : Type u_1} [PseudoMetricSpace E] [AddCommMonoid E] [Module ℝ E] (K : ConvexBody E) : Bornology.IsBounded K.carrier

A convex body is bounded (compact in a metric space).