Pointwise membership stability for Hausdorff-convergent convex subbodies

For a family of convex subbodies C a → C₀ in the Hausdorff metric this module establishes the pointwise stability of membership in the underlying carriers:

• ConvexSubbody.mem_limit_of_tendsto — the membership graph is closed: if x a ∈ C a eventually, C a → C₀ and x a → x₀, then x₀ ∈ C₀ (needs a NeBot index filter);
• ConvexSubbody.exists_tendsto_points — every point of a limit body is the limit of a sequence of points chosen from the approximating bodies;
• ConvexSubbody.eventually_not_mem_of_not_mem — exterior stability: a point outside the closed limit body is eventually outside the approximating bodies;
• ConvexSubbody.eventually_mem_of_mem_interior — interior stability: a point in the interior of the limit body is eventually inside the approximating bodies;
• ConvexSubbody.eventually_mem_iff_of_not_mem_frontier — off the frontier, membership in the approximating bodies eventually agrees with membership in the limit body.

Interior stability is the geometric heart: it rests on the strict separation of an exterior point from a compact convex set by a unit normal, packaged as the auxiliary set lemmas exists_separating_unit and mem_of_hausdorffDist_lt.

theorem NRR.ConvexSubbody.exists_separating_unit {D : Set Geometry.Plane} (hconv : Convex ℝ D) (hcomp : IsCompact D) (hne : D.Nonempty) {x : Geometry.Plane} (hx : x ∉ D) : ∃ (u : Geometry.Plane), ‖u‖ = 1 ∧ ∀ y ∈ D, inner ℝ y u ≤ inner ℝ x u

theorem NRR.ConvexSubbody.mem_of_hausdorffDist_lt {D E : Set Geometry.Plane} (hDconv : Convex ℝ D) (hDcomp : IsCompact D) (hDne : D.Nonempty) (hEbdd : Bornology.IsBounded E) (hEne : E.Nonempty) {x : Geometry.Plane} {ε : ℝ} (hε : 0 < ε) (hball : Metric.closedBall x ε ⊆ E) (hdist : Metric.hausdorffDist D E < ε) : x ∈ D

theorem NRR.ConvexSubbody.mem_limit_of_tendsto {K : Geometry.ConvexBody Geometry.Plane} {α : Type u_1} {l : Filter α} [l.NeBot] {C : α → ConvexSubbody K} {C₀ : ConvexSubbody K} {x : α → Geometry.Plane} {x₀ : Geometry.Plane} (hC : Filter.Tendsto C l (nhds C₀)) (hx : Filter.Tendsto x l (nhds x₀)) (hmem : ∀ᶠ (a : α) in l, x a ∈ ↑(C a).body) : x₀ ∈ ↑C₀.body

theorem NRR.ConvexSubbody.exists_tendsto_points {K : Geometry.ConvexBody Geometry.Plane} {C : ℕ → ConvexSubbody K} {C₀ : ConvexSubbody K} (hC : Filter.Tendsto C Filter.atTop (nhds C₀)) {x : Geometry.Plane} (hx : x ∈ ↑C₀.body) : ∃ (xseq : ℕ → Geometry.Plane), (∀ (m : ℕ), xseq m ∈ ↑(C m).body) ∧ Filter.Tendsto xseq Filter.atTop (nhds x)

theorem NRR.ConvexSubbody.eventually_not_mem_of_not_mem {K : Geometry.ConvexBody Geometry.Plane} {α : Type u_1} {l : Filter α} {C : α → ConvexSubbody K} {C₀ : ConvexSubbody K} (hC : Filter.Tendsto C l (nhds C₀)) {x : Geometry.Plane} (hx : x ∉ ↑C₀.body) : ∀ᶠ (a : α) in l, x ∉ ↑(C a).body

theorem NRR.ConvexSubbody.eventually_mem_of_mem_interior {K : Geometry.ConvexBody Geometry.Plane} {α : Type u_1} {l : Filter α} {C : α → ConvexSubbody K} {C₀ : ConvexSubbody K} (hC : Filter.Tendsto C l (nhds C₀)) {x : Geometry.Plane} (hx : x ∈ interior ↑C₀.body) : ∀ᶠ (a : α) in l, x ∈ ↑(C a).body

theorem NRR.ConvexSubbody.eventually_mem_iff_of_not_mem_frontier {K : Geometry.ConvexBody Geometry.Plane} {α : Type u_1} {l : Filter α} {C : α → ConvexSubbody K} {C₀ : ConvexSubbody K} (hC : Filter.Tendsto C l (nhds C₀)) {x : Geometry.Plane} (hx : x ∉ frontier ↑C₀.body) : ∀ᶠ (a : α) in l, x ∈ ↑(C a).body ↔ x ∈ ↑C₀.body