Mathlib v3 is deprecated. Go to Mathlib v4

Theorem uniform_cauchy_seq_on.cauchy_map

Modification history

2022-10-27 07:38
src/topology/uniform_space/uniform_convergence.lean
feat(analysis/calculus/uniform_limits_deriv): pointwise convergence out of derivative convergence on a preconnected set (#17123) …
Added uniform_cauchy_seq_on.cauchy_mapView on Github →