Countable products of metrics is metrizable #763
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
zstone1
force-pushed
the
countable_ent
branch
from
56d5533
to
705a06f
Compare
zstone1
force-pushed
the
countable_ent
branch
from
705a06f
to
13e937e
Compare
zstone1
force-pushed
the
countable_ent
branch
from
13e937e
to
8f6915f
Compare
|
Is there anything else required to merge this, or is this ready for an approval? |
affeldt-aist
changed the title
zstone1
force-pushed
the
countable_ent
branch
from
e1b6056
to
e099078
Compare
2 tasks
affeldt-aist
approved these changes
Feb 7, 2023
There was a problem hiding this comment.
I tried to improve a bit the scripts. I noticed uses of projT1/projT2 where proj1_sig a.k.a. as sval would have been in order (causing at least one useless manual conversion) but it appears that using sval makes it for unfolded expressions. I think that the definition of sval is at fault and PRed MathComp math-comp/math-comp#964 . We can maybe replace these expressions later.
zstone1
force-pushed
the
countable_ent
branch
from
e6c62b3
to
6ec0f09
Compare
hoheinzollern
pushed a commit
to hoheinzollern/analysis
that referenced
this pull request
Mar 9, 2023
* proving sups preserve countable ent * proof going through * unused proofs * linting * metric implies countable uniformity * fixing changelog * linting * metric for products * linting * fixing docs * use %:pos * fixing changelog * fix changelog * nitpicking --------- Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
proux01
pushed a commit
that referenced
this pull request
Mar 24, 2023
* proving sups preserve countable ent * proof going through * unused proofs * linting * metric implies countable uniformity * fixing changelog * linting * metric for products * linting * fixing docs * use %:pos * fixing changelog * fix changelog * nitpicking --------- Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Motivation for this change
Finally, we prove that countable products of metrics are metrizable! In particularly, the cantor set is metrizable. I have
countable_uniformity. Several lemmas use it, so it made sense to factor into a nicer definition. Note that this property is equivalent to metrizability, so it has little purpose outside of this family of proofs.countable_uniformity. The definition of sup entourages is kinda annoying, so the proof is on the large side. It's not a blocker, just an inconvenience.Things done/to do
CHANGELOG_UNRELEASED.md(do not edit former entries, only append new ones, be careful:
merge and rebase have a tendency to mess up
CHANGELOG_UNRELEASED.md)Automatic note to reviewers
Read this Checklist and put a milestone if possible.