Skip to content

Commit

Permalink
refactor(topology/subset_properties.lean): split the subset_propertie…
Browse files Browse the repository at this point in the history 
…s.lean file (#6161)

split the file subset_properties.lean into another file called connected.lean which contains the properties that relate to connectivity. This is in preparation for a future PR proving properties about the quotient of a space by its connected components and it would add roughly 300 lines.
  • Loading branch information
@callesonne
callesonne committed Feb 11, 2021
1 parent 97a56e6 commit 59daf53
Show file tree
Hide file tree
Showing 3 changed files with 575 additions and 539 deletions.

0 comments on commit 59daf53

Please sign in to comment.