Separability of Real Normed Spaces and Its Basic Properties

[1] Jonathan Backer, Piotr Rudnicki, and Christoph Schwarzweller. Ring ideals. Formalized Mathematics, 9(3):565–582, 2001.Search in Google Scholar

[2] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.Search in Google Scholar

[3] Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543–547, 1990.Search in Google Scholar

[4] Grzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 1990.Search in Google Scholar

[5] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.Search in Google Scholar

[6] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.Search in Google Scholar

[7] Nicolas Bourbaki. Topological vector spaces: Chapters 1-5. Springer, 1981.Search in Google Scholar

[8] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990.Search in Google Scholar

[9] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990.Search in Google Scholar

[10] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.Search in Google Scholar

[11] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.Search in Google Scholar

[12] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.Search in Google Scholar

[13] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.Search in Google Scholar

[14] N. J. Dunford and T. Schwartz. Linear operators I. Interscience Publ., 1958.Search in Google Scholar

[15] 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.10.2478/v10037-006-0024-xSearch in Google Scholar

[16] Andrey Kolmogorov and Sergei Fomin. Elements of the Theory of Functions and Functional Analysis [Two Volumes in One]. Martino Fine Books, 2012.Search in Google Scholar

[17] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841–845, 1990.Search in Google Scholar

[18] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.Search in Google Scholar

[19] Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Topological properties of real normed space. Formalized Mathematics, 22(3):209–223, 2014. doi:10.2478/forma-2014-0024.10.2478/forma-2014-0024Search in Google Scholar

[20] 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.10.2478/forma-2014-0007Search in Google Scholar

[21] Keiko Narita, Noboru Endou, and Yasunari Shidama. Bidual spaces and reflexivity of real normed spaces. Formalized Mathematics, 22(4):303–311, 2014. doi:10.2478/forma-2014-0030.10.2478/forma-2014-0030Search in Google Scholar

[22] Bogdan Nowak and Andrzej Trybulec. Hahn-Banach theorem. Formalized Mathematics, 4(1):29–34, 1993.Search in Google Scholar

[23] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.Search in Google Scholar

[24] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111–115, 1991.Search in Google Scholar

[25] Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39–48, 2004.Search in Google Scholar

[26] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1): 115–122, 1990.Search in Google Scholar

[27] Wojciech A. Trybulec. Subspaces and cosets of subspaces in real linear space. Formalized Mathematics, 1(2):297–301, 1990.Search in Google Scholar

[28] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990.Search in Google Scholar

[29] Wojciech A. Trybulec. Linear combinations in real linear space. Formalized Mathematics, 1(3):581–588, 1990.Search in Google Scholar

[30] Wojciech A. Trybulec. Basis of real linear space. Formalized Mathematics, 1(5):847–850, 1990.Search in Google Scholar

[31] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.Search in Google Scholar

[32] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.Search in Google Scholar

[33] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.Search in Google Scholar

[34] Kosaku Yoshida. Functional Analysis. Springer, 1980.Search in Google Scholar