Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-03 19:27 d0816c0f

View on Github →

feat(analysis/calculus): support and cont_diff (#11976)

Add some lemmas about the support of the (f)derivative of a function
Add some equivalences for cont_diff

Estimated changes

Modified src/analysis/calculus/cont_diff.lean

added theorem cont_diff.continuous_deriv

added theorem cont_diff_at_one_iff

added theorem cont_diff_one_iff_deriv

added theorem cont_diff_one_iff_fderiv

added theorem cont_diff_top_iff_deriv

Modified src/analysis/calculus/deriv.lean

added theorem deriv_eq

added theorem has_compact_support.deriv

added theorem support_deriv_subset

Modified src/analysis/calculus/fderiv.lean

added theorem fderiv_eq

added theorem has_compact_support.fderiv

added theorem support_fderiv_subset

Modified src/data/set/lattice.lean

added theorem set.antitone_bforall