Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-16 07:01 ee981c28

View on Github →

refactor(analysis/calculus/fderiv): prove has_fderiv_within_at.lim for any filter (#1805)

  • refactor(analysis/calculus/fderiv): prove has_fderiv_within_at.lim for any filter Also prove two versions of "directional derivative agrees with has_fderiv_at": has_fderiv_at.lim and has_fderiv_at.lim_real.
  • Rename a lemma as suggested by @sgouezel

Estimated changes

added theorem has_fderiv_at.lim
added theorem has_fderiv_at.lim_real
modified theorem has_fderiv_within_at.lim
modified theorem tangent_cone_at.lim_zero