[Merged by Bors] - refactor(topology/bases): removing/adding the empty set from/to a basis #17133
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Add lemmas
is_topological_basis.insert/diff_empty
that allows adding the empty set to a basis and removing the empty set from a basis.Remove
(⋂₀ f).nonempty
fromis_topological_basis_of_subbasis
and golf the proof. This condition is unnatural and was only used to exclude the empty set in topological_space.second_countable_topology.to_separable_space, because we want to choose a point from each set in the basis. As a result, the proofexists_countable_basis
needs a slight modification.