[[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-x]Search 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-0024]Search 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-0007]Search 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-0030]Search 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