NRR.EMP.VariableBody.ClosedGraph — the compact closed-graph criterion

This module provides the abstract topological input that turns uniqueness plus a closed relation into continuity of a selection map.

• continuous_of_isClosed_graph_of_compact: a function into a compact Hausdorff space, out of a compact Hausdorff space, whose graph is closed, is continuous. Mathlib does not carry this exact statement as a single named theorem, so it is proved here via the compact-projection route.
• isClosed_graph_of_isClosed_relation_of_unique: if a closed relation R contains the graph of f and selects each value uniquely, then the graph of f is closed (indeed equal to R).

The compactness of both the domain and the codomain is essential: the closed-graph theorem is false for continuity without it.

theorem NRR.EMP.VariableBody.continuous_of_isClosed_graph_of_compact {D : Type u_1} {Y : Type u_2} [TopologicalSpace D] [CompactSpace D] [T2Space D] [TopologicalSpace Y] [CompactSpace Y] (f : D → Y) (hgraph : IsClosed {z : D × Y | z.2 = f z.1}) : Continuous f

Compact closed-graph criterion. A map f : D → Y between compact Hausdorff spaces whose graph {z | z.2 = f z.1} is closed is continuous.

Proof route: for a closed F ⊆ Y, the set graph f ∩ (univ ×ˢ F) is closed in the compact product D × Y, hence compact; its image under the first projection is compact, hence closed since D is Hausdorff; and that image equals f ⁻¹' F.

theorem NRR.EMP.VariableBody.isClosed_graph_of_isClosed_relation_of_unique {D : Type u_1} {Y : Type u_2} [TopologicalSpace D] [TopologicalSpace Y] (R : Set (D × Y)) (hR : IsClosed R) (f : D → Y) (hf : ∀ (d : D), R (d, f d)) (huniq : ∀ (d : D) (y : Y), R (d, y) → y = f d) : IsClosed {z : D × Y | z.2 = f z.1}

Uniqueness closes the graph. If a closed relation R contains the graph of f (hf : ∀ d, R (d, f d)) and selects each value uniquely (huniq : ∀ d y, R (d, y) → y = f d), then the graph {z | z.2 = f z.1} is closed, being equal to R.