Theorem LinearMap.continuous_of_isClosed_graph

Modification history

2026-09-11 13:59
Mathlib/Analysis/Normed/Operator/Banach.lean
feat(Topology/Maps): add `Continuous.isClosed_graph` and `continuous_of_isClosed_graph` (#43275) …
Deleted LinearMap.continuous_of_isClosed_graphView on Github →
2023-05-20 01:21
Mathlib/Analysis/NormedSpace/Banach.lean
feat: port Analysis.NormedSpace.Banach (#4122)
Added LinearMap.continuous_of_isClosed_graphView on Github →