Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-21 11:25 18b61ef3

View on Github →

feat(topology/uniform_space/uniform_convergence): more locally uniform limit API (#17092) Add more API around tendsto_locally_uniformly_on, needed for #17074.

Estimated changes

Modified src/analysis/calculus/uniform_limits_deriv.lean

added theorem has_deriv_at_of_tendsto_locally_uniformly_on'

added theorem has_deriv_at_of_tendsto_locally_uniformly_on

added theorem has_fderiv_at_of_tendsto_locally_uniformly_on'

added theorem has_fderiv_at_of_tendsto_locally_uniformly_on

Modified src/topology/uniform_space/uniform_convergence.lean

added theorem tendsto_locally_uniformly_iff_filter

added theorem tendsto_locally_uniformly_on.congr

added theorem tendsto_locally_uniformly_on.congr_right

added theorem tendsto_locally_uniformly_on.tendsto_at

added theorem tendsto_locally_uniformly_on.unique

added theorem tendsto_locally_uniformly_on_iff_filter

added theorem tendsto_locally_uniformly_on_iff_forall_is_compact

added theorem tendsto_locally_uniformly_on_tfae

added theorem tendsto_uniformly_on.congr_right