tangent_cone): prove that all intervals are `unique_diff_on`
#2108

Merged

feat(analysis/calculus/tangent_cone): prove that all intervals are `unique_diff_on` #2108

mergify merged 3 commits into master from unique-diff-on-intervals

jcommelin approved these changes on 2020-03-09

jcommelin commented on 2020-03-09

cipher1024 assigned

jcommelin 6 years ago

feat(analysis/calculus/tangent_cone): prove that all intervals are `u…

be721cd6

urkud force pushed from 91201c78 to be721cd6 6 years ago

urkud changed the title ~~feat(analysis/calculus/tangent_cone): prove that all closed intervals are `unique_diff_on`~~ feat(analysis/calculus/tangent_cone): prove that all intervals are `unique_diff_on` 6 years ago

Drop some unneeded assumptions

7f1fe578

sgouezel added ready-to-merge

Merge branch 'master' into unique-diff-on-intervals

3ae27760

jcommelin commented on 2020-03-10

mergify merged cdc56baf into master 6 years ago

mergify deleted the unique-diff-on-intervals branch 6 years ago

Reviewers

jcommelin

sgouezel

Assignees

jcommelin

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(analysis/calculus/tangent_cone): prove that all intervals are `unique_diff_on` #2108 Merged

feat(analysis/calculus/tangent_cone): prove that all intervals are `unique_diff_on` #2108

mathlib3
feat(analysis/calculus/tangent_cone): prove that all intervals are `unique_diff_on`
#2108

Merged