mathlib

52899945 - feat(analysis/calculus/mean_value): add generalized "fencing" inequality (#1838)

feat(analysis/calculus/mean_value): add generalized "fencing" inequality (#1838) * feat(analysis/calculus/mean_value): add generalized "fencing" inequality This version can be used to deduce, e.g., Gronwall inequality as well as its generalized version that deals with approximate solutions. * Adjust to merged branches, use `liminf` instead of `limsup`, add more variations * Go through dim-1 liminf estimates * Fix: use `b ∈ Ioc a c` as a hypothesis for `I??_mem_nhds_within_Iio` * Update src/analysis/calculus/mean_value.lean Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Drop `Prop`-valued `variables`, add some docs * More docstrings * Drop `Prop`-valued `variables`, drop assumption `x ∉ s`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>