[[1] Czesław Byliński. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661–668, 1990.]Search in Google Scholar
[[2] Adam Grabowski, Artur Korniłowicz, and Christoph Schwarzweller. On algebraic hierarchies in mathematical repository of Mizar. In M. Ganzha, L. Maciaszek, and M. Paprzycki, editors, Proceedings of the 2016 Federated Conference on Computer Science and Information Systems (FedCSIS), volume 8 of Annals of Computer Science and Information Systems, pages 363–371, 2016. doi:10.15439/2016F520.10.15439/2016F520]Search in Google Scholar
[[3] Miyadera Isao. Functional Analysis. Riko-Gaku-Sya, 1972.]Search in Google Scholar
[[4] Marco Riccardi. Pocklington’s theorem and Bertrand’s postulate. Formalized Mathematics, 14(2):47–52, 2006. doi:10.2478/v10037-006-0007-y.10.2478/v10037-006-0007-y]Open DOISearch in Google Scholar
[[5] Laurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.]Search in Google Scholar
[[6] Laurent Schwartz. Calcul différentiel, tome 2. Analyse. Hermann, 1997.]Search in Google Scholar
[[7] Kosaku Yoshida. Functional Analysis. Springer, 1980.]Search in Google Scholar
