feat(Topology/Homotopy): add Path.subpathOn for restricting paths to subintervals #34557
Conversation
This file contains hidden or 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
…subintervals This PR adds `Path.subpathOn`, which extracts a subpath from a path γ on an interval [a, b] ⊆ [0, 1] by reparametrizing via the affine map t ↦ a + t(b - a). Main results: - `Path.subpathOn`: definition of the restricted path - `Path.subpathOn_trans`: composing subpaths is homotopic to the combined subpath - `Path.subpathOn_self`: the trivial subpath [a,a] is homotopic to the constant path - `Path.subpathOn_zero_one`: the full subpath [0,1] is homotopic to the original path - Quotient-level versions of these theorems This is split out from leanprover-community#31576 to allow independent review. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
6 tasks
github-actions
bot
added
the
t-topology
PR summary 17e9ef1cfcImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
jcommelin
reviewed
Jan 29, 2026
jcommelin
added
the
awaiting-author
Refactors `Path.subpathOn` to use `Set.Icc.convexCombo` directly, removing redundant inline proofs. Also adds: - `Set.Icc.convexCombo_same`: simp lemma for `convexCombo x x t = x` - `Set.Icc.convexCombo_zero_one`: simp lemma for endpoints - `Set.Icc.continuous_convexCombo`: continuity with `@[fun_prop]` - New file `Topology/UnitInterval/ConvexSpace.lean` with `unitInterval.convexCombo` for abstract convex spaces Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
…lemma - Move `unitInterval.half` and `coe_half` from Path.lean to UnitInterval.lean - Delete duplicate `continuous_convexCombo₃` (identical to `continuous_convexCombo`) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
kim-em
removed
the
awaiting-author
Member
|
/claude learn new skill: run |
jcommelin
added
the
awaiting-author
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
This PR adds
Path.subpathOn, which extracts a subpath from a path γ on an interval [a, b] ⊆ [0, 1] by reparametrizing via the affine map t ↦ a + t(b - a).Main results
Path.subpathOn: definition of the restricted pathPath.subpathOn_trans: composing subpaths is homotopic to the combined subpathPath.subpathOn_self: the trivial subpath [a,a] is homotopic to the constant pathPath.subpathOn_zero_one: the full subpath [0,1] is homotopic to the original pathThis material is split out from #31576 to allow independent review. PR #31576 will depend on this PR once merged.
🤖 Prepared with Claude Code