Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-01 10:20 6265d261

View on Github →

feat(analysis/normed_space/deriv): start on derivative

Estimated changes

Modified src/analysis/normed_space/bounded_linear_maps.lean

added theorem is_bounded_linear_map.is_bigo_id

added theorem is_bounded_linear_map.is_bigo_sub

added def is_bounded_linear_map.to_linear_map

Created src/analysis/normed_space/deriv.lean

added theorem chain_rule

added theorem continuous_of_has_fderiv

added theorem has_fderiv_add

added def has_fderiv_at

added theorem has_fderiv_at_within.congr

added def has_fderiv_at_within

added def has_fderiv_at_within_mono

added theorem has_fderiv_const

added theorem has_fderiv_equiv_aux

added theorem has_fderiv_id

added theorem has_fderiv_iff_littleo

added theorem has_fderiv_neg

added theorem has_fderiv_smul

added theorem has_fderiv_sub