Commit 2021-02-11 09:21 59daf530
View on Github →refactor(topology/subset_properties.lean): split the subset_properties.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.