References
- Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: a survey of proof assistants and libraries. Mathematical Structures in Computer Science, pages 1–38, 2014.
- Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formal proof of the Lax-Milgram theorem. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 79–89, New York, NY, USA, 2017. Association for Computing Machinery. doi:10.1145/3018610.3018625.
- 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.
- Johannes Hölzl, Fabian Immler, and Brian Hu man. Type classes and filters for mathematical analysis in Isabelle/HOL. In Interactive Theorem Proving, pages 279–294. Springer, 2013.
- Isao Miyadera. Functional Analysis. Riko-Gaku-Sya, 1972.
- Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Implicit function theorem. Part I. Formalized Mathematics, 25(4):269–281, 2017. doi:10.1515/forma-2017-0026.
- Lawrence Narici and Edward Beckenstein. Topological Vector Spaces. Chapman and Hall/CRC, 2010. doi:10.1201/9781584888673.
- Keiko Narita, Noboru Endou, and Yasunari Shidama. Weak convergence and weak* convergence. Formalized Mathematics, 23(3):231–241, 2015. doi:10.1515/forma-2015-0019.
- Colin Rothgang, Artur Korniłowicz, and Florian Rabe. A new export of the Mizar Mathematical Library. In Fairouz Kamareddine and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics, pages 205–210, Cham, 2021. Springer International Publishing. doi:10.1007/978-3-030-81097-917.
- Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.
- Laurent Schwartz. Cours d’analyse. Hermann, 1981.
- Kôsaku Yosida. Functional Analysis. Springer, 1980.