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.

Estimated changes

added theorem is_clopen_iff
added theorem is_connected.closure
added theorem is_connected.image
added theorem is_connected.nonempty
added theorem is_connected.union
added def is_connected
added theorem is_connected_range
added theorem is_connected_singleton
added theorem is_preconnected.image
added theorem is_preconnected.union
added def is_preconnected
added theorem is_preconnected_empty
added theorem is_preconnected_sUnion
added theorem nonempty_inter
deleted def connected_component
deleted theorem is_clopen_iff
deleted theorem is_connected.closure
deleted theorem is_connected.image
deleted theorem is_connected.nonempty
deleted theorem is_connected.union
deleted def is_connected
deleted theorem is_connected_range
deleted theorem is_connected_singleton
deleted theorem is_preconnected.closure
deleted theorem is_preconnected.image
deleted theorem is_preconnected.union
deleted def is_preconnected
deleted theorem is_preconnected_empty
deleted theorem is_preconnected_of_forall
deleted theorem is_preconnected_sUnion
deleted theorem mem_connected_component
deleted theorem nonempty_inter
deleted theorem subtype.connected_space