mathlib3
0f1362e1 - chore(analysis/calculus/mean_value): use `𝓝[Ici x] x` instead of `𝓝[Ioi x] x` (#5472)

Commit
5 years ago
chore(analysis/calculus/mean_value): use `𝓝[Ici x] x` instead of `𝓝[Ioi x] x` (#5472) In many parts of the library we prefer `𝓝[Ici x] x` to `𝓝[Ioi x] x` (e.g., in assumptions line `continuous_within_at`). Fix MVT and Gronwall's inequality to use it if possible. Motivated by #4945
Author
Parents
Loading