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
refactor(topology,calculus): change subset condition for composition #1549
refactor(topology,calculus): change subset condition for composition #1549
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 made a very quick pass. The image vs preimage thing is clear: preimages are much better. But I left two docstring comments.
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.
Nice! I left a couple of stylistic suggestions, mostly hoping to help a bit making you even more efficient.
Thanks a lot for your comments @PatrickMassot. I think I have addressed them all. |
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.
You introduced two docstring typos. Tip: if you had pushed your PR branch to the community repository instead of your fork I could have fixed the typos myself.
…eanprover-community#1549) * refactor(topology,calculus): change subset condition for composition * improve docstrings * add is_open Ioi * reviewer's comments * typo
A grab bag of small additions that I need in further developments. I don't really think it makes sense to split it into several smaller PRs, but if you insist I will.
The main change is the reformulation of the subset condition for composition. For instance, for
continuous_on
, the condition for continuity of the composition off
(continuous ons
) andg
(continuous ont
) wasf '' s ⊆ t
. I change it everywhere tos ⊆ f ⁻¹' t
, which is equivalent but computes a lot better (belonging to the image is something complicated, with an existential quantifier, while belonging to the preimage is much simpler). This opened the way to much better simp automation for manifolds.