Open Mapping Theorem

• Autorzy: Hideki Sakurai , Hisayoshi Kunimune , Yasunari Shidama
• Języki publikacji: EN

Abstrakty

EN

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

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2008
• Tom: 16
• Numer: 4
• Strony: 401-403

Daty

wydano

2008-01-01

online

2009-03-20

Twórcy

autor

Hideki Sakurai

• Shinshu University, Nagano, Japan

autor

Hisayoshi Kunimune

• Shinshu University, Nagano, Japan

autor

Yasunari Shidama

• Shinshu University, Nagano, Japan

Bibliografia

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

Identyfikatory

DOI

10.2478/v10037-008-0048-5