Open Mapping Theorem
Hideki Sakurai ; Hisayoshi Kunimune ; Yasunari Shidama
Formalized Mathematics, Tome 16 (2008), p. 401-403 / Harvested from The Polish Digital Mathematics Library
Access to full text
Full (PDF)

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

Publié le : 2008-01-01
EUDML-ID : urn:eudml:doc:267453 
@article{bwmeta1.element.doi-10_2478_v10037-008-0048-5,
     author = {Hideki Sakurai and Hisayoshi Kunimune and Yasunari Shidama},
     title = {Open Mapping Theorem},
     journal = {Formalized Mathematics},
     volume = {16},
     year = {2008},
     pages = {401-403},
     language = {en},
     url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_v10037-008-0048-5}
}

Hideki Sakurai; Hisayoshi Kunimune; Yasunari Shidama. Open Mapping Theorem. Formalized Mathematics, Tome 16 (2008) pp. 401-403. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_v10037-008-0048-5/

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. | Zbl 06213858

[2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.

[3] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.

[4] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Convex sets and convex combinations. Formalized Mathematics, 11(1):53-58, 2003.

[5] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Dimension of real unitary space. Formalized Mathematics, 11(1):23-28, 2003.

[6] Noboru Endou, Yasunari Shidama, and Katsumasa Okamura. Baire's category theorem and some spaces generated from real normed space. Formalized Mathematics, 14(4):213-219, 2006.

[7] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35-40, 1990.

[8] Isao Miyadera. Functional Analysis. Riko-Gaku-Sya, 1972.

[9] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990.

[10] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111-115, 1991.

[11] Hideki Sakurai, Hisayoshi Kunimune, and Yasunari Shidama. Uniform boundedness principle. Formalized Mathematics, 16(1):19-21, 2008.

[12] Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39-48, 2004.

[13] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.

[14] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990.

[15] Mariusz Żynel and Adam Guzowski. T0 topological spaces. Formalized Mathematics, 5(1):75-77, 1996.