NRR.EMP.VariableBody.CanonicalCellContinuity — closed graph and continuity of cells

We upgrade the one-sided closed-graph result isClosed_canonicalCellLowerGraph to the exact graph of the canonical power cell and deduce continuity of each cell and of the finite family.

• CanonicalCellGraph — the exact relation {z | z.2 = canonicalCell sites hA hn z.1 i}.
• isClosed_canonicalCellGraph — the exact graph is closed.
• continuous_canonicalCell — each canonical cell varies continuously in the Hausdorff hyperspace.
• continuous_canonicalCells — the finite family of cells varies continuously.

The exact-graph closedness combines the one-sided lower-graph inclusion with area continuity and the convex-area rigidity of ConvexSubbody.eq_of_subset_of_area_eq: a Hausdorff limit D of the cells is contained in the limiting canonical cell, both have the common target area z.1.body.area / n (positive since 0 < A and 0 < n), so ConvexSubbody.eq_of_subset_of_area_eq forces equality. Continuity then follows from the compact closed-graph criterion continuous_of_isClosed_graph_of_compact (both the parameter space BodySpace K A × X and the codomain ConvexSubbody K are compact Hausdorff metric spaces), and the family continuity from continuous_pi.

def NRR.EMP.VariableBody.CanonicalCellGraph {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (i : Fin n) : Set ((BodySpace K A × X) × ConvexSubbody K)

The exact canonical-cell graph: parameter–subbody pairs (z, D) where the subbody D equals the canonical power cell of site i at z.

Equations

• NRR.EMP.VariableBody.CanonicalCellGraph sites hA hn i = {z : (NRR.BodySpace K A × X) × NRR.ConvexSubbody K | z.2 = NRR.EMP.VariableBody.canonicalCell sites hA hn z.1 i}

theorem NRR.EMP.VariableBody.isClosed_canonicalCellGraph {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (i : Fin n) : IsClosed (CanonicalCellGraph sites hA hn i)

Exact closedness of the canonical-cell graph. The relation identifying a subbody with the canonical power cell of its parameter is closed.

theorem NRR.EMP.VariableBody.continuous_canonicalCell {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (i : Fin n) : Continuous fun (z : BodySpace K A × X) => canonicalCell sites hA hn z i

Continuity of the canonical cell. Each canonical power cell depends continuously on the parameter, valued in the compact Hausdorff hyperspace ConvexSubbody K.

theorem NRR.EMP.VariableBody.continuous_canonicalCells {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) : Continuous fun (z : BodySpace K A × X) (i : Fin n) => canonicalCell sites hA hn z i

Continuity of the finite cell family. The whole finite family of canonical power cells depends continuously on the parameter.