Splitting Topology part 3: Separation axioms #1338
Open
+1,087
−1,002
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.
Continuing with #1167, this moves all the stuff about separation axioms into a separate file. I included a few other things that aren't explicitly "T0-T6", but felt comfortable here, such as zero-dimensional and perfect sets.
There are still some critical results about separation axioms (AKA urysohn's lemma and friends) that are trapped in normedtype.v due to some boring facts about the reals. We need to build the
edist
function for a pseudoMetric, which requires a few small things aboutR
. Some results generalize to anyorderTopologicalType
such as\min
is continuous. Others can live inereal.v
. It'll take some effort to break that stuff up, though. So I'll leave it for a later PR.Checklist
added corresponding entries in
CHANGELOG_UNRELEASED.md
added corresponding documentation in the headers
Reference: How to document
Reminder to reviewers