Lean-Intro-Topology

This project is an introduction to Lean as a supplement to a course in proof writing. The project then delves into some basic topology, as an application of proof writing.

Getting Lean

To install Lean 4, go to https://leanprover-community.github.io/get_started.html

Cloning this repository

To clone this repository, go to the file folder you want to clone it to, then type into the terminal (if you're not sure how to open the terminal, go to the terminal section of this document):

git clone https://github.com/rafaelgrenier/lean-intro-topology.git

cd lean-intro-topology

lake exe cache get

And if you already have VSCode downloaded, type the following command to immediately start working on the project:

code .

Terminal

For Windows Users, you can install Git here, and then use the Git BASH terminal. For Mac Users, the Terminal app exists.