-
Notifications
You must be signed in to change notification settings - Fork 49
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
extended distance #986
extended distance #986
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I suggest to move inf/sup lemmas to reals.v and to rename imply_orE to implyE which seems to agree better with the naming convention used so far. I think I spotted a few missing trivial lemmas and that a few computational steps could be shortened, hence the last commit.
Nice! I would rather advocate for a curried distance function |
Yes, stating continuity from the product does not require dealing with function space topologies. Uncurrying is not generally continuous, and requires extra assumptions on the domain (like locally compact). However, continuity from the product is stronger, and true here. So it's the right thing to prove regardless. I suppose we could define edist as curried, and prove I have #926 proving all this stuff about continuity of curry/uncurry, anyway. (It's barely a draft. Proofs are done, it just need a linting/reorganizing pass). |
* extended distance * adding docs * shorten computations, factor out lemmas --------- Co-authored-by: Reynald Affeldt <[email protected]>
* extended distance * adding docs * shorten computations, factor out lemmas --------- Co-authored-by: Reynald Affeldt <[email protected]>
* extended distance * adding docs * shorten computations, factor out lemmas --------- Co-authored-by: Reynald Affeldt <[email protected]>
Motivation for this change
Rather than wait on HB to introduce a structure with a "standard" distance, we can introduce this "extended" distance function for pseudometrics to finish Urysohn's Lemma. This is part of track A of #965.
Things done/to do
CHANGELOG_UNRELEASED.md
Compatibility with MathComp 2.0
TODO: HB port
to make sure someone ports this PR tothe
hierarchy-builder
branch or I already opened an issue or PR (please cross reference).Automatic note to reviewers
Read this Checklist and put a milestone if possible.