Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-15 01:46 fca7ebaf

View on Github →

chore(analysis/calculus/deriv): composition of g : 𝕜 → 𝕜 with f : E → 𝕜 (#4871)

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem has_deriv_at.comp_has_fderiv_at

added theorem has_deriv_at.comp_has_fderiv_within_at

added theorem has_deriv_at_filter.comp_has_fderiv_at_filter

added theorem has_deriv_within_at.comp_has_fderiv_within_at

Modified src/topology/continuous_on.lean

added theorem continuous_within_at.tendsto_nhds_within