Commit 2026-09-11 13:59 63025c44
View on Github →feat(Topology/Maps): add Continuous.isClosed_graph and continuous_of_isClosed_graph (#43275)
Add new results relating continuity of f : X → Y to closedness of Function.graph f into Topology/Maps
Continuous.isClosed_graph: when Y is Hausdorff and f is continuous then f has a closed graph.continuous_of_isClosed_graph: when Y is a compact space and f has a closed graph then f is continuous.continuous_iff_isClosed_graph: the bidirectional result when Y is both compact and Hausdorff.