Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(geometry/manifold/cont_mdiff): generalize some lemmas to arbitrary charts#17668

Closed
fpvandoorn wants to merge 19 commits intomasterfrom
manifold_extend
Closed

[Merged by Bors] - feat(geometry/manifold/cont_mdiff): generalize some lemmas to arbitrary charts#17668
fpvandoorn wants to merge 19 commits intomasterfrom
manifold_extend

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn commented Nov 21, 2022 •
edited by github-actions bot
Loading

  • This PR generalizes some smoothness results from ext_chart_at to arbitrary members of the maximal atlas
  • Useful for smooth vector bundle refactor
  • Motivated by the sphere eversion project

Open in Gitpod

@fpvandoorn fpvandoorn added awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI The author would like to see what CI has to say before doing more work. labels Nov 21, 2022
@ghost ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Nov 21, 2022
@fpvandoorn fpvandoorn removed the awaiting-author A reviewer has asked the author a question or requested changes label Nov 21, 2022
@fpvandoorn fpvandoorn mentioned this pull request Nov 22, 2022
Closed
3 tasks
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Dec 2, 2022
@ghost
Copy link
Copy Markdown

ghost commented Dec 2, 2022

This PR/issue depends on:

@fpvandoorn fpvandoorn added the awaiting-review The author would like community review of the PR label Dec 6, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jan 6, 2023
@sgouezel
Copy link
Copy Markdown
Collaborator

sgouezel commented Jan 6, 2023

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jan 6, 2023
bors bot pushed a commit that referenced this pull request Jan 6, 2023
@fpvandoorn
feat(geometry/manifold/cont_mdiff): generalize some lemmas to arbitra…
e644458 
…ry charts (#17668)

* This PR generalizes some smoothness results from `ext_chart_at` to arbitrary members of the maximal atlas
* Useful for smooth vector bundle refactor
* Motivated by the sphere eversion project
@bors
Copy link
Copy Markdown

bors bot commented Jan 6, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(geometry/manifold/cont_mdiff): generalize some lemmas to arbitrary charts [Merged by Bors] - feat(geometry/manifold/cont_mdiff): generalize some lemmas to arbitrary charts Jan 6, 2023
@bors bors bot closed this Jan 6, 2023
@bors bors bot deleted the manifold_extend branch January 6, 2023 22:53
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@fpvandoorn @sgouezel