Mathlib v3 is deprecated. Go to Mathlib v4

Theorem uniform_cauchy_seq_on_ball_of_fderiv

Modification history

2022-10-27 07:38

src/analysis/calculus/uniform_limits_deriv.lean

feat(analysis/calculus/uniform_limits_deriv): pointwise convergence out of derivative convergence on a preconnected set (#17123) …

Added uniform_cauchy_seq_on_ball_of_fderiv View on Github →