3. Topological Spaces in Lean
In this section we will see how some basic concepts of general topology are represented in Lean. The goal is not to develop the complete theory, but to show concrete examples of formal definitions and proofs, which serve as a first contact with working in Lean on topological spaces.
The mathematical definitions and results used are the usual ones in general topology. Although I initially based this work on the notes I took in the Elementary Topology course, I have later checked them against (Stephen Willard, 2012)Stephen Willard, 2012. “General topology”. Courier Corporation. as a standard reference.