Uniform Boundedness Principle
Hideki Sakurai ; Hisayoshi Kunimune ; Yasunari Shidama
Formalized Mathematics, Tome 16 (2008), p. 19-21 / Harvested from The Polish Digital Mathematics Library
Access to full text
Full (PDF)

In this article at first, we proved the lemma of the inferior limit and the superior limit. Next, we proved the Baire category theorem (Banach space version) [20], [9], [3], quoted it and proved the uniform boundedness principle. Moreover, the proof of the Banach-Steinhaus theorem is added.MML identifier: LOPBAN 5, version: 7.8.05 4.89.993

Publié le : 2008-01-01
EUDML-ID : urn:eudml:doc:266597 
@article{bwmeta1.element.doi-10_2478_v10037-008-0003-5,
     author = {Hideki Sakurai and Hisayoshi Kunimune and Yasunari Shidama},
     title = {Uniform Boundedness Principle},
     journal = {Formalized Mathematics},
     volume = {16},
     year = {2008},
     pages = {19-21},
     language = {en},
     url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_v10037-008-0003-5}
}

Hideki Sakurai; Hisayoshi Kunimune; Yasunari Shidama. Uniform Boundedness Principle. Formalized Mathematics, Tome 16 (2008) pp. 19-21. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_v10037-008-0003-5/

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

[2] Czesław Byliński. Introduction to real linear topological spaces. Formalized Mathematics, 13(1):99-107, 2005.

[3] N. J. Dunford and T. Schwartz. Linear operators I. Interscience Publ., 1958. | Zbl 0084.10402

[4] 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.

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

[6] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607-610, 1990.

[7] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273-275, 1990.

[8] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990.

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

[10] Andrzej Nedzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401-407, 1990.

[11] Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269-275, 2004.

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

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

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

[15] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329-334, 1990.

[16] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.

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

[18] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.

[19] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231-237, 1990.

[20] Kosaku Yoshida. Functional Analysis. Springer, 1980.

[21] Bo Zhang, Hiroshi Yamazaki, and Yatsuka Nakamura. Inferior limit and superior limit of sequences of real numbers. Formalized Mathematics, 13(3):375-381, 2005.