mathlib
1a249186 - feat(analysis/calculus/uniform_limits_deriv): pointwise convergence out of derivative convergence on a preconnected set (#17123)

Commit
3 years ago
feat(analysis/calculus/uniform_limits_deriv): pointwise convergence out of derivative convergence on a preconnected set (#17123) Also cleanup the file `calculus/uniform_limits_deriv` by removing unnecessary typeclass assumptions, fixing lemma names and docstrings, and replacing convergence assumptions by Cauchyness assumption when the limit is not relevant.
Author
Parents
Loading