Theorem continuous_of_isClosed_graph

Modification history

2026-09-11 13:59
Mathlib/Topology/Maps/Proper/Basic.lean
feat(Topology/Maps): add `Continuous.isClosed_graph` and `continuous_of_isClosed_graph` (#43275) …
Added continuous_of_isClosed_graphView on Github →