Banach’s Continuous Inverse Theorem and Closed Graph Theorem
Hideki Sakurai, Hiroyuki Okazaki, Yasunari Shidama · Formalized Mathematics · 2012
Summary In this article we formalize one of the most important theorems of linear operator theory - the Closed Graph Theorem commonly used in a standard text book such as [10] in Chapter 24.3. It states that a surjective closed linear operator between Banach spaces is bounded.