theorem ClosedGraph.closed_graph_theorem_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [CompleteSpace V] {W : Type u_3} [NormedAddCommGroup W] [NormedSpace 𝕜 W] [CompleteSpace W] (T : V →ₗ[𝕜] W) : Continuous ⇑T ↔ IsClosed ↑T.graph

Closed Graph Theorem. Let $B_1, B_2$ be two Banach spaces, and let $T : B_1 \to B_2$ be a (not necessarily bounded) linear operator. Then $T \in \mathcal{B}(B_1, B_2)$ if and only if the graph of $T$, defined as $\Gamma(T) = \{(u, Tu) : u \in B_1\}$, is closed in $B_1 \times B_2$.