References
- Nelson Dunford and Jacob T. Schwartz. Linear operators I. Interscience Publ., 1958.
- Noboru Endou and Yasunari Shidama. Differentiation in normed spaces. Formalized Mathematics, 21(2):95–102, 2013. doi:10.2478/forma-2013-0011.
- Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153–245, 2010.
- Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.
- Isao Miyadera. Functional Analysis. Riko-Gaku-Sya, 1972.
- Kazuhisa Nakasho and Yasunari Shidama. Higher-order differentiation and inverse function theorem in real normed spaces. Formalized Mathematics, 32(1):247–269, 2024. doi:10.2478/forma-2024-0021.
- Laurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.
- Laurent Schwartz. Calcul différentiel, tome 2. Analyse. Hermann, 1997.
- Yasunari Shidama. Differentiable functions on normed linear spaces. Formalized Mathematics, 20(1):31–40, 2012. doi:10.2478/v10037-012-0005-1.
- Kôsaku Yosida. Functional Analysis. Springer, 1980.