The goal of this article is to show some examples of topological manifolds: planes and spheres in Euclidean space. In doing it, the article introduces the stereographic projection [25].
Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599-603, 1991.
Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605-608, 1991.
Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35-40, 1990.
Katarzyna Jankowska. Matrices. Abelian group of matrices. Formalized Mathematics, 2(4):475-480, 1991.
Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607-610, 1990.
Artur Korniłowicz and Yasunari Shidama. Intersections of intervals and balls in εn/T Formalized Mathematics, 12(3):301-306, 2004.
Artur Korniłowicz and Yasunari Shidama. Some properties of circles on the plane. Formalized Mathematics, 13(1):117-124, 2005.
Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990.
Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990.
John M. Lee. Introduction to Topological Manifolds. Springer-Verlag, New York Berlin Heidelberg, 2000.
Robert Milewski. Bases of continuous lattices. Formalized Mathematics, 7(2):285-294, 1998.
Yatsuka Nakamura, Artur Korniłowicz, Nagato Oya, and Yasunari Shidama. The real vector spaces of finite sequences are finite dimensional. Formalized Mathematics, 17(1):1-9, 2009, doi:10.2478/v10037-009-0001-2.[Crossref]
Henryk Oryszczyszyn and Krzysztof Prażmowski. Real functions spaces. Formalized Mathematics, 1(3):555-561, 1990.
Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990.