Closed graph theorem from the bounded inverse theorem (source code)

= Closed graph theorem from the bounded inverse theorem

For a closed graph, the projection $\Gamma(T)\to X$ is a bounded bijection between Banach spaces. Its bounded inverse followed by projection to $Y$ is $T$.