Topological Properties of Real Normed Space

Kazuhisa Nakasho; Yuichi Futa; Yasunari Shidama

Formalized Mathematics (2014)

  • Volume: 22, Issue: 3, page 209-223
  • ISSN: 1426-2630

Abstract

top
In this article, we formalize topological properties of real normed spaces. In the first part, open and closed, density, separability and sequence and its convergence are discussed. Then we argue properties of real normed subspace. Then we discuss linear functions between real normed speces. Several kinds of subspaces induced by linear functions such as kernel, image and inverse image are considered here. The fact that Lipschitz continuity operators preserve convergence of sequences is also refered here. Then we argue the condition when real normed subspaces become Banach’s spaces. We also formalize quotient vector space. In the last session, we argue the properties of the closure of real normed space. These formalizations are based on [19](p.3-41), [2] and [34](p.3-67).

How to cite

top

Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. "Topological Properties of Real Normed Space." Formalized Mathematics 22.3 (2014): 209-223. <http://eudml.org/doc/270985>.

@article{KazuhisaNakasho2014,
abstract = {In this article, we formalize topological properties of real normed spaces. In the first part, open and closed, density, separability and sequence and its convergence are discussed. Then we argue properties of real normed subspace. Then we discuss linear functions between real normed speces. Several kinds of subspaces induced by linear functions such as kernel, image and inverse image are considered here. The fact that Lipschitz continuity operators preserve convergence of sequences is also refered here. Then we argue the condition when real normed subspaces become Banach’s spaces. We also formalize quotient vector space. In the last session, we argue the properties of the closure of real normed space. These formalizations are based on [19](p.3-41), [2] and [34](p.3-67).},
author = {Kazuhisa Nakasho, Yuichi Futa, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {functional analysis; normed linear space; topological vector space},
language = {eng},
number = {3},
pages = {209-223},
title = {Topological Properties of Real Normed Space},
url = {http://eudml.org/doc/270985},
volume = {22},
year = {2014},
}

TY - JOUR
AU - Kazuhisa Nakasho
AU - Yuichi Futa
AU - Yasunari Shidama
TI - Topological Properties of Real Normed Space
JO - Formalized Mathematics
PY - 2014
VL - 22
IS - 3
SP - 209
EP - 223
AB - In this article, we formalize topological properties of real normed spaces. In the first part, open and closed, density, separability and sequence and its convergence are discussed. Then we argue properties of real normed subspace. Then we discuss linear functions between real normed speces. Several kinds of subspaces induced by linear functions such as kernel, image and inverse image are considered here. The fact that Lipschitz continuity operators preserve convergence of sequences is also refered here. Then we argue the condition when real normed subspaces become Banach’s spaces. We also formalize quotient vector space. In the last session, we argue the properties of the closure of real normed space. These formalizations are based on [19](p.3-41), [2] and [34](p.3-67).
LA - eng
KW - functional analysis; normed linear space; topological vector space
UR - http://eudml.org/doc/270985
ER -

References

top
  1. [1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  2. [2] Nicolas Bourbaki, H.G. Eggleston, and S. Madan. Elements of mathematics: Topological vector spaces. Springer-Verlag, 1987. 
  3. [3] Czesław Bylinski. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990. 
  4. [4] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  5. [5] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  6. [6] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  7. [7] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  8. [8] Noboru Endou, Yasumasa Suzuki, and Yasunari Shidama. Real linear space of real sequences. Formalized Mathematics, 11(3):249-253, 2003. 
  9. [9] 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. doi:10.2478/v10037-006-0024-x.[Crossref] 
  10. [10] Adam Grabowski. On the boundary and derivative of a set. Formalized Mathematics, 13 (1):139-146, 2005. 
  11. [11] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477-481, 1990. 
  12. [12] Jarosław Kotowicz. Quotient vector spaces and functionals. Formalized Mathematics, 11 (1):59-68, 2003. 
  13. [13] Eugeniusz Kusak, Wojciech Leonczuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990. 
  14. [14] Keiko Narita, Noboru Endou, and Yasunari Shidama. Dual spaces and Hahn-Banach theorem. Formalized Mathematics, 22(1):69-77, 2014. doi:10.2478/forma-2014-0007.[Crossref] Zbl1298.46005
  15. [15] Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269-275, 2004. 
  16. [16] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990. 
  17. [17] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990. 
  18. [18] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111-115, 1991. 
  19. [19] Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991. 
  20. [20] Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39-48, 2004. 
  21. [21] Yasunari Shidama. The series on Banach algebra. Formalized Mathematics, 12(2):131-138, 2004. Zbl1276.11090
  22. [22] Yasumasa Suzuki, Noboru Endou, and Yasunari Shidama. Banach space of absolute summable real sequences. Formalized Mathematics, 11(4):377-380, 2003. 
  23. [23] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1): 115-122, 1990. 
  24. [24] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990. 
  25. [25] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341-347, 2003. 
  26. [26] Wojciech A. Trybulec. Subspaces and cosets of subspaces in real linear space. Formalized Mathematics, 1(2):297-301, 1990. 
  27. [27] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990. 
  28. [28] Wojciech A. Trybulec. Basis of real linear space. Formalized Mathematics, 1(5):847-850, 1990. 
  29. [29] Wojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Formalized Mathematics, 1(5):865-870, 1990. 
  30. [30] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  31. [31] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990. 
  32. [32] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990. 
  33. [33] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231-237, 1990. 
  34. [34] Kosaku Yoshida. Functional Analysis. Springer, 1980. 

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.