Closedness of convexity in the Hausdorff hyperspace

This module proves that the locus of convex nonempty compact planar sets is closed in the Hausdorff hyperspace TopologicalSpace.NonemptyCompacts Plane. This is the geometric ingredient needed for compactness of ConvexSubbody K.

The hyperspace carries the Hausdorff (extended) metric, under which edist between nonempty compact sets equals the Hausdorff extended distance of their carriers. The proof develops two convergence facts about this metric:

• mem_limit_of_tendsto_nonemptyCompacts: if x m ∈ C m, C m → C₀ and x m → x₀, then x₀ ∈ C₀ (closed membership under Hausdorff limits);
• exists_tendsto_points_of_tendsto_nonemptyCompacts: any point of a limit set C₀ is the limit of a sequence of points chosen from the approximating sets C m (point approximation).

Convexity of a limit set (convex_limit_of_tendsto) then follows by approximating the two endpoints of a segment and passing the convex combinations to the limit; closedness (isClosed_convex_nonemptyCompacts) is the sequential packaging of this fact.

theorem NRR.BodySpace.mem_limit_of_tendsto_nonemptyCompacts {C : ℕ → TopologicalSpace.NonemptyCompacts Geometry.Plane} {C₀ : TopologicalSpace.NonemptyCompacts Geometry.Plane} {x : ℕ → Geometry.Plane} {x₀ : Geometry.Plane} (hC : Filter.Tendsto C Filter.atTop (nhds C₀)) (hx : Filter.Tendsto x Filter.atTop (nhds x₀)) (hmem : ∀ (m : ℕ), x m ∈ ↑(C m)) : x₀ ∈ ↑C₀

If x m ∈ C m, the sets C m converge to C₀ in the Hausdorff hyperspace, and the points x m converge to x₀, then x₀ ∈ C₀.

theorem NRR.BodySpace.exists_tendsto_points_of_tendsto_nonemptyCompacts {C : ℕ → TopologicalSpace.NonemptyCompacts Geometry.Plane} {C₀ : TopologicalSpace.NonemptyCompacts Geometry.Plane} (hC : Filter.Tendsto C Filter.atTop (nhds C₀)) {x : Geometry.Plane} (hx : x ∈ ↑C₀) : ∃ (xseq : ℕ → Geometry.Plane), (∀ (m : ℕ), xseq m ∈ ↑(C m)) ∧ Filter.Tendsto xseq Filter.atTop (nhds x)

Every point of a Hausdorff limit set C₀ is the limit of a sequence of points drawn from the approximating sets C m.

theorem NRR.BodySpace.convex_limit_of_tendsto {C : ℕ → TopologicalSpace.NonemptyCompacts Geometry.Plane} {C₀ : TopologicalSpace.NonemptyCompacts Geometry.Plane} (hC : Filter.Tendsto C Filter.atTop (nhds C₀)) (hconv : ∀ (m : ℕ), Convex ℝ ↑(C m)) : Convex ℝ ↑C₀

The Hausdorff limit of convex nonempty compact sets is convex.

theorem NRR.BodySpace.isClosed_convex_nonemptyCompacts : IsClosed {C : TopologicalSpace.NonemptyCompacts Geometry.Plane | Convex ℝ ↑C}

Convexity is closed in the Hausdorff hyperspace. The set of convex nonempty compact planar sets is closed in TopologicalSpace.NonemptyCompacts Plane.