mathlib3
feat(analysis/calculus/mean_value): add generalized "fencing" inequality
#1838
Merged
Merged
sgouezel
commented
on 2019-12-29
sgouezel
commented
on 2019-12-29
feat(analysis/calculus/mean_value): add generalized "fencing" inequality
eff2bbda
Adjust to merged branches, use `liminf` instead of `limsup`, add more…
ca27897c
Go through dim-1 liminf estimates
98731fcd
Fix: use `b ∈ Ioc a c` as a hypothesis for `I??_mem_nhds_within_Iio`
4d4318b0
urkud
changed the title
sgouezel
commented
on 2020-01-04
Update src/analysis/calculus/mean_value.lean
4246a656
Drop `Prop`-valued `variables`, add some docs
f4133d49
Merge branch 'fence' of git://github.com/leanprover-community/mathlib…
e0dd4bde
More docstrings
d376bdd2
Merge branch 'master' into fence
b174becb
sgouezel
commented
on 2020-01-06
sgouezel
commented
on 2020-01-06
Merge branch 'master' into fence
1e8d2c26
Merge branch 'master' into fence
6e678115
Drop `Prop`-valued `variables`, drop assumption `x ∉ s`.
8d0d36c2
sgouezel
approved these changes
on 2020-01-09
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into fence
491d2138
Login to write a write a comment.
Login via GitHub