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
[Merged by Bors] - feat(topology/path_connected): add lemmas about paths and continuous families of paths #4063
Conversation
src/topology/path_connected.lean
Outdated
|
||
/-! #### Portion of a path -/ | ||
|
||
/-- `γ.portion t` is the path which starts by following the path `γ`, |
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 don't like this definition, because it is somewhat arbitrary that you only keep the beginning of the path. You could have path.truncate_left
, path.truncate_right
and path.truncate
, for instance (or just path.truncate
, where you allow truncation on both sides, and where you could use 0
on the left if you want to copy the functionality of your "portion")
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 don't think it's so arbitrary, because the path is clearly oriented, and I think truncating means keeping the beginning.
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.
To be honest I was also not completely okay with my portion
, so I just made your truncate
. I'll have to modify my proof in the sphere eversion project but I've made a few tests and it should hopefully not be much longer.
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.
LGTM, although some proofs are a bit long.
@kckennylau @sgouezel do you have any comments?
LGTM |
Co-authored-by: Johan Commelin <johan@commelin.net>
Thanks! bors r+ |
…families of paths (#4063) From the sphere eversion project (see leanprover-community/sphere-eversion#12) Co-authored-by: Anatole <anatolededecker@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Anatole Dedecker <48656793+ADedecker@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
From the sphere eversion project (see leanprover-community/sphere-eversion#12)