Open Mapping Theorem

In this article we formalize one of the most important theorems of linear operator theory the Open Mapping Theorem commonly used in a standard book such as [8] in chapter 2.4.2. It states that a surjective continuous linear operator between Banach spaces is an open map.

MML identifier: LOPBAN 6, version: 7.10.01 4.111.1036