Realfun and subspaces #752
Conversation
zstone1
force-pushed
the
realfun_within
branch
from
565c705
to
e126466
Compare
zstone1
force-pushed
the
realfun_within
branch
from
e126466
to
3f4f457
Compare
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
| rewrite eqEsubset; split => z; rewrite /= itvxx. | ||
| by move=> ?; apply/eqP. | ||
| by move=>/eqP. | ||
| - by move=> ->; rewrite set_itv1; exact: continuous_subspace1. |
There was a problem hiding this comment.
I observe that when performing the rewrite the continuous notation is such that the goal is displayed as continuous f. Hasn't something changed in an undesirable way about this notation?
There was a problem hiding this comment.
Sadly I don't think {within A, continuous f} ever printed correctly. There are a handful of other notations in topology.v, like pointwise convergence. that have the same problem. Coq is not picking "specialized" notation. Surprisingly we don't have an open issue for fixing this. I'll add one.
There was a problem hiding this comment.
Could we achieve this with a specialised notation which detects subspace_... canonicals?
There was a problem hiding this comment.
Commit b4230 seems like a nice step in the right direction. For the purpose of completing this PR, I'm satisfied with the current improvement. If you agree, we should continue to discuss in #758. I'm quite interested in how you'd build notations that depend on the presence of canonicals.
There was a problem hiding this comment.
Should we try to address the other notation problems mentioned by issue #758 as part of this PR?
There was a problem hiding this comment.
I've updated with corresponding change for the other notations.
There was a problem hiding this comment.
It means that issue #758 is (mostly) fixed?
There was a problem hiding this comment.
Yeah, seems like it. The approach won't work for all notations, but it does work fine for swapping topologies. Once this is merged I'll close that ticket.
Motivation for this change
I need to deal with monotone, continuous
R->Rfunctions in homotopy theory. Thankfully, much of it already exists. However, when this was written we didn't have a nice way to talk about behavior at the endpoints of intervals. With the subspace topology infrastructure, we can clean this all up. All changed theorem have been improved:{in I, continuous f}to{within I, continuous f}. The problem is{ in [a,b], continuous f}relies on f being continuous from the left ata. That's bad news, because it depends on values outside of[a,b]. Instead{within I, continuous f}truly doesn't care about values outside ofI.{in ]a, b[, continuous f}to{within [a,b], continuous f}, which is slightly stronger by controlling the "from-the-right" continuity ata, and dually atb. The original result can be recovered with acontinuous_subspaceW+open_continuous_subspace.Several of the theorems that strengthen the result from
{in ]a, b[, continuous f}to{within [a,b], continuous f}are pretty tricky. The endpoints require a lot of annoying interval arithmetic to get right, but I did end up finding a way.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)[] added corresponding documentation in the headersAutomatic note to reviewers
Read this Checklist and put a milestone if possible.