mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(analysis/calculus/cont_diff): Prove that `fderiv_within` is `C^n` for functions with parameters

Open fpvandoorn opened this issue 3 years ago • 1 comments

  • Prove that fderiv_within is C^n (at a point within a set) for a function with parameters
  • Move existing lemmas (for functions without parameters) down in the file
  • There are some inconvenient side-conditions needed for the lemmas, that could maybe organized better
  • This is useful for lemmas about mfderiv
  • From the sphere eversion project
  • [ ] depends on: #16933

Open in Gitpod

fpvandoorn avatar Oct 13 '22 10:10 fpvandoorn

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16933~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Oct 18 '22 08:10 mathlib-dependent-issues-bot

Is it hard to split this PR into 2: (1) reorder/rename; (2) new features?

urkud avatar Nov 05 '22 07:11 urkud

Is it hard to split this PR into 2: (1) reorder/rename; (2) new features?

Ok, I opened #17585, which can be merged first

fpvandoorn avatar Nov 17 '22 16:11 fpvandoorn

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16933~~
  • ~~leanprover-community/mathlib#17585~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Nov 25 '22 18:11 mathlib-dependent-issues-bot

Can you merge master and change the PR description?

sgouezel avatar Nov 27 '22 13:11 sgouezel

oops, I did that request before I saw the latest review. Thanks for the initial review! EDIT: but now it can be reviewed again :-)

fpvandoorn avatar Dec 02 '22 14:12 fpvandoorn

:v: fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors[bot] avatar Jan 07 '23 17:01 bors[bot]

Thanks for the synchronization reminder, I might have forgotten it. It is leanprover/mathlib4#1833

fpvandoorn avatar Jan 25 '23 13:01 fpvandoorn

bors merge

fpvandoorn avatar Jan 25 '23 16:01 fpvandoorn

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Jan 25 '23 19:01 bors[bot]