Closed graphs and continuity on a set

A function whose graph over a set s is closed and whose values on s lie in a compact set is continuous on s. This is the relative form of Mathlib's continuous_of_isClosed_graph; it identifies a bounded single-valued closure of a graph with a continuous function. Conversely, ContinuousOn.closure_graphOn_inter recovers a continuous function's graph from its restriction to a relatively dense subset. This permits extending a description of a graph across an exceptional locus without making any choices of values there.

theorem TauCeti.continuousOn_of_isClosed_graphOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {K : Set Y} (hf : IsClosed (Set.graphOn f s)) (hK : IsCompact K) (hfK : Set.MapsTo f s K) : ContinuousOn f s

A function whose graph over s is closed and which maps s into a compact set is continuous on s.

theorem ContinuousOn.closure_graphOn_inter {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} {s t : Set X} (hf : ContinuousOn f s) (hts : t ⊆ s) (hst : s ⊆ closure t) : closure (Set.graphOn f t) ∩ s ×ˢ Set.univ = Set.graphOn f s

A continuous function on s is recovered from its graph on a relatively dense subset t: the graph closure, restricted back to points over s, is exactly its graph on s.