NRR.ConvexSubbody — inherited Hausdorff topology and hyperspace embedding

This module exposes the Hausdorff metric/topology that ConvexSubbody K inherits, as a subtype, from Mathlib's root convex body _root_.ConvexBody Plane. It provides:

• the inherited MetricSpace / T2Space structure;
• the forgetful map ConvexSubbody.toNonemptyCompacts into the hyperspace of nonempty compact sets, shown to be an isometric embedding (continuous, IsInducing, IsEmbedding);
• the identification dist C D = hausdorffDist C.body D.body;
• closedness of the fixed-parent containment locus inside NonemptyCompacts Plane;
• filter-level convergence lemmas (tendsto_body, tendsto_hausdorffDist_zero) used by later prompts.

No new metric, hyperspace topology, or convex-body type is introduced: everything is inherited from the root Mathlib body and its Hausdorff metric.

@[instance_reducible]

noncomputable instance NRR.ConvexSubbody.instMetricSpace {K : Geometry.ConvexBody Geometry.Plane} : MetricSpace (ConvexSubbody K)

The inherited Hausdorff metric on ConvexSubbody K, taken as a subtype of Mathlib's root convex body _root_.ConvexBody Plane. Because ConvexSubbody is a def over a subtype, this instance is stated explicitly rather than inferred.

Equations

• One or more equations did not get rendered due to their size.

instance NRR.ConvexSubbody.instT2Space {K : Geometry.ConvexBody Geometry.Plane} : T2Space (ConvexSubbody K)

ConvexSubbody K is Hausdorff (inherited from its metric).

def NRR.ConvexSubbody.toNonemptyCompacts {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : TopologicalSpace.NonemptyCompacts Geometry.Plane

The forgetful map to the hyperspace of nonempty compact sets: a subbody is sent to its carrier, together with its compactness and nonemptiness witnesses.

Equations

• C.toNonemptyCompacts = { carrier := ↑C.body, isCompact' := ⋯, nonempty' := ⋯ }

@[simp]

theorem NRR.ConvexSubbody.toNonemptyCompacts_carrier {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : ↑C.toNonemptyCompacts = ↑C.body

theorem NRR.ConvexSubbody.isometry_toNonemptyCompacts {K : Geometry.ConvexBody Geometry.Plane} : Isometry toNonemptyCompacts

The forgetful map to NonemptyCompacts is an isometry: both sides measure the Hausdorff extended distance between the same carriers.

theorem NRR.ConvexSubbody.continuous_toNonemptyCompacts {K : Geometry.ConvexBody Geometry.Plane} : Continuous toNonemptyCompacts

theorem NRR.ConvexSubbody.inducing_toNonemptyCompacts {K : Geometry.ConvexBody Geometry.Plane} : Topology.IsInducing toNonemptyCompacts

The forgetful map to NonemptyCompacts is inducing (the inherited topology is the pullback of the hyperspace topology). Named inducing_toNonemptyCompacts; the current Mathlib predicate is Topology.IsInducing.

theorem NRR.ConvexSubbody.embedding_toNonemptyCompacts {K : Geometry.ConvexBody Geometry.Plane} : Topology.IsEmbedding toNonemptyCompacts

theorem NRR.ConvexSubbody.dist_eq_hausdorffDist {K : Geometry.ConvexBody Geometry.Plane} (C D : ConvexSubbody K) : dist C D = Metric.hausdorffDist ↑C.body ↑D.body

The inherited distance on ConvexSubbody K is the Hausdorff distance of the carriers.

theorem NRR.ConvexSubbody.isClosed_fixedParent_nonemptyCompacts {K : Geometry.ConvexBody Geometry.Plane} : IsClosed {C : TopologicalSpace.NonemptyCompacts Geometry.Plane | ↑C ⊆ K.carrier}

The fixed-parent containment locus — nonempty compact sets contained in the parent body K — is closed in the hyperspace NonemptyCompacts Plane.

theorem NRR.ConvexSubbody.tendsto_body {K : Geometry.ConvexBody Geometry.Plane} {α : Type u_1} {l : Filter α} {C : α → ConvexSubbody K} {C₀ : ConvexSubbody K} (hC : Filter.Tendsto C l (nhds C₀)) : Filter.Tendsto (fun (a : α) => (C a).toNonemptyCompacts) l (nhds C₀.toNonemptyCompacts)

Convergence of subbodies pushes forward to convergence of their hyperspace images.

theorem NRR.ConvexSubbody.tendsto_hausdorffDist_zero {K : Geometry.ConvexBody Geometry.Plane} {α : Type u_1} {l : Filter α} {C : α → ConvexSubbody K} {C₀ : ConvexSubbody K} (hC : Filter.Tendsto C l (nhds C₀)) : Filter.Tendsto (fun (a : α) => Metric.hausdorffDist ↑(C a).body ↑C₀.body) l (nhds 0)

Convergence of subbodies is witnessed by the Hausdorff distances tending to zero.