Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-08 14:15 054b4676

View on Github →

feat(analysis/calculus): derivatives of f : E → Π i, F i (#6075)

Estimated changes

added theorem asymptotics.is_O_pi
added theorem asymptotics.is_o_pi
added theorem deriv_pi
added theorem deriv_within_pi
added theorem has_deriv_at_filter_pi
added theorem has_deriv_at_pi
added theorem has_deriv_within_at_pi
added theorem has_strict_deriv_at_pi
added theorem differentiable_at_pi
added theorem differentiable_on_pi
added theorem differentiable_pi
added theorem fderiv_pi
added theorem fderiv_within_pi
added theorem has_fderiv_at_pi'
added theorem has_fderiv_at_pi