In this repository I am collecting the code of my formalization of CW-Complexes in Lean. My formalisation is based on mathlib. This project started as my bachelors thesis supervised by Prof. van Doorn. An (outdated) discussion of the code can be found in my thesis at Latex/Thesis/thesis.pdf I am continuing this work as a student assistant.

The examples are part of my project for the course "Practical Project in Mathematical Logic - Formalized Mathematics in Lean" taught by Prof. van Doorn. The corresponding code can be found in the folder CWcomplexes/Project. The slides of my presentation and the summary can be found in the folder Latex/Project LeanCourse.

(The second contributor is my dad helping me with git and Latex.)