fderiv): define `has_strict_fderiv_at`
#2249

Merged

feat(analysis/calculus/fderiv): define `has_strict_fderiv_at` #2249

mergify merged 8 commits into master from strict-fderiv

Move code aroud

fac89a98

Use `maps_to` instead of `f '' _ ⊆ _`

d2b330d4

feat(analysis/calculus/fderiv): define `has_strict_fderiv_at`

edc3fec8

urkud added awaiting-review

sgouezel commented on 2020-03-27

Update src/analysis/calculus/fderiv.lean

bdbdec3a

Docs, var name

07bfbd43

Merge branch 'strict-fderiv' of git://github.com/leanprover-community…

28c0e21f

sgouezel removed awaiting-review

sgouezel added ready-to-merge

sgouezel approved these changes on 2020-03-28

Merge branch 'master' into strict-fderiv

6c936dfb

Merge branch 'master' into strict-fderiv

66469dde

mergify merged 5d9e7f58 into master 6 years ago

urkud deleted the strict-fderiv branch 6 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone