# Open Mapping Theorem

Hideki Sakurai; Hisayoshi Kunimune; Yasunari Shidama

Formalized Mathematics (2008)

- Volume: 16, Issue: 4, page 401-403
- ISSN: 1426-2630

## Access Full Article

top## Abstract

top## How to cite

topHideki Sakurai, Hisayoshi Kunimune, and Yasunari Shidama. "Open Mapping Theorem." Formalized Mathematics 16.4 (2008): 401-403. <http://eudml.org/doc/267453>.

@article{HidekiSakurai2008,

abstract = {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},

author = {Hideki Sakurai, Hisayoshi Kunimune, Yasunari Shidama},

journal = {Formalized Mathematics},

language = {eng},

number = {4},

pages = {401-403},

title = {Open Mapping Theorem},

url = {http://eudml.org/doc/267453},

volume = {16},

year = {2008},

}

TY - JOUR

AU - Hideki Sakurai

AU - Hisayoshi Kunimune

AU - Yasunari Shidama

TI - Open Mapping Theorem

JO - Formalized Mathematics

PY - 2008

VL - 16

IS - 4

SP - 401

EP - 403

AB - 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

LA - eng

UR - http://eudml.org/doc/267453

ER -

## References

top- [1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
- [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.

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.