20. Topological spaces🔗

The goal of this chapter is to give an introduction to the language of topology in Mathlib that requires minimal background. In particular, we do not assume the reader is familiar with filters. For an in depth tutorial of topology in Mathlib, see the topology chapter of Mathematics in Lean.

For an introduction to filters and how they are used to describe limits and convergence; see Limit statements and Proving limits.

1. 20.1. Basic language
2. 20.2. Continuous maps
3. 20.3. Properties of Topological Spaces