Commit 2023-06-02 13:42 99ad0c16

View on Github →

feat: port Analysis.Calculus.UniformLimitsDeriv (#4584)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean

added theorem UniformCauchySeqOnFilter.one_smulRight

added theorem cauchy_map_of_uniformCauchySeqOn_fderiv

added theorem difference_quotients_converge_uniformly

added theorem hasDerivAt_of_tendstoLocallyUniformlyOn

added theorem hasDerivAt_of_tendstoUniformly

added theorem hasDerivAt_of_tendstoUniformlyOn

added theorem hasDerivAt_of_tendstoUniformlyOnFilter

added theorem hasDerivAt_of_tendsto_locally_uniformly_on'

added theorem hasFDerivAt_of_tendstoLocallyUniformlyOn

added theorem hasFDerivAt_of_tendstoUniformly

added theorem hasFDerivAt_of_tendstoUniformlyOn

added theorem hasFDerivAt_of_tendstoUniformlyOnFilter

added theorem hasFDerivAt_of_tendsto_locally_uniformly_on'

added theorem uniformCauchySeqOnFilter_of_deriv

added theorem uniformCauchySeqOnFilter_of_fderiv

added theorem uniformCauchySeqOn_ball_of_deriv

added theorem uniformCauchySeqOn_ball_of_fderiv