Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 13:55 c1c0fa4a

View on Github →

feat(analysis/calculus/{f,}deriv): add some iff lemmas (#11363)

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem has_deriv_at_deriv_iff

added theorem has_deriv_within_at_deriv_within_iff

Modified src/analysis/calculus/fderiv.lean

added theorem filter.eventually_eq.differentiable_at_iff

added theorem filter.eventually_eq.differentiable_within_at_iff

added theorem filter.eventually_eq.differentiable_within_at_iff_of_mem

added theorem filter.eventually_eq.has_fderiv_at_iff

added theorem filter.eventually_eq.has_fderiv_within_at_iff

added theorem filter.eventually_eq.has_fderiv_within_at_iff_of_mem