Open Mapping Theorem

Hideki Sakurai; Hisayoshi Kunimune; Yasunari Shidama

Formalized Mathematics (2008)

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

Abstract

top
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

How to cite

top

Hideki 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. [1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  2. [2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  3. [3] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  4. [4] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Convex sets and convex combinations. Formalized Mathematics, 11(1):53-58, 2003. 
  5. [5] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Dimension of real unitary space. Formalized Mathematics, 11(1):23-28, 2003. 
  6. [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. [7] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35-40, 1990. 
  8. [8] Isao Miyadera. Functional Analysis. Riko-Gaku-Sya, 1972. 
  9. [9] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990. 
  10. [10] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111-115, 1991. 
  11. [11] Hideki Sakurai, Hisayoshi Kunimune, and Yasunari Shidama. Uniform boundedness principle. Formalized Mathematics, 16(1):19-21, 2008. 
  12. [12] Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39-48, 2004. 
  13. [13] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  14. [14] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990. 
  15. [15] Mariusz Żynel and Adam Guzowski. T0 topological spaces. Formalized Mathematics, 5(1):75-77, 1996. 

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.