Compactness of the fixed-parent convex subbody hyperspace

This module proves that the fixed-parent hyperspace NRR.ConvexSubbody K is a compact space under its inherited Hausdorff metric.

The argument combines two ingredients on the hyperspace TopologicalSpace.NonemptyCompacts Plane:

• the set of nonempty compact subsets of the fixed compact parent K is compact (NonemptyCompacts.isCompact_subsets_of_isCompact);
• the locus of convex carriers is closed (BodySpace.isClosed_convex_nonemptyCompacts).

Their intersection, convexSubbodyLocus K, is therefore compact, and it coincides with the range of the isometric embedding ConvexSubbody.toNonemptyCompacts. Transferring compactness through that embedding yields compactness of Set.univ in ConvexSubbody K, hence the canonical CompactSpace instance. No new metric, hyperspace topology, or convex-body type is introduced, and compactness is grounded in the fixed compact parent rather than in an unproved Blaschke selection.

def NRR.convexSubbodyLocus (K : Geometry.ConvexBody Geometry.Plane) : Set (TopologicalSpace.NonemptyCompacts Geometry.Plane)

The convex subbody locus of a fixed parent K: the nonempty compact planar sets that are both contained in K and convex. This is the image of ConvexSubbody K in the Hausdorff hyperspace.

Equations

• NRR.convexSubbodyLocus K = {C : TopologicalSpace.NonemptyCompacts NRR.Geometry.Plane | ↑C ⊆ K.carrier ∧ Convex ℝ ↑C}

theorem NRR.isCompact_convexSubbodyLocus (K : Geometry.ConvexBody Geometry.Plane) : IsCompact (convexSubbodyLocus K)

The convex subbody locus is compact: it is the intersection of the compact set of nonempty compact subsets of the parent K with the closed locus of convex carriers.

theorem NRR.ConvexSubbody.range_toNonemptyCompacts (K : Geometry.ConvexBody Geometry.Plane) : Set.range toNonemptyCompacts = convexSubbodyLocus K

The range of the forgetful embedding toNonemptyCompacts is exactly the convex subbody locus of K.

theorem NRR.ConvexSubbody.isCompact_univ (K : Geometry.ConvexBody Geometry.Plane) : IsCompact Set.univ

Compactness of the subbody hyperspace. The whole space ConvexSubbody K is compact: its image under the isometric embedding into NonemptyCompacts Plane is the compact locus convexSubbodyLocus K.

instance NRR.ConvexSubbody.instCompactSpace {K : Geometry.ConvexBody Geometry.Plane} : CompactSpace (ConvexSubbody K)

The canonical compact-space instance on ConvexSubbody K, obtained from compactness of the whole space.

theorem NRR.ConvexSubbody.compact_range {K : Geometry.ConvexBody Geometry.Plane} {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (f : C(X, ConvexSubbody K)) : IsCompact (Set.range ⇑f)

The image of a compact space under a continuous map into ConvexSubbody K has compact range.