Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-14 10:24 ade99c8c

View on Github →

feat(analysis/normed_space/deriv): more material on derivatives (#966)

  • feat(analysis/normed_space/deriv): more material on derivatives
  • feat(analysis/normed_space/deriv): minor improvements
  • feat(analysis/normed_space/deriv) rename fderiv_at_within to fderiv_within_at
  • feat(analysis/normed_space/deriv): more systematic renaming
  • feat(analysis/normed_space/deriv): fix style
  • modify travis.yml as advised by Simon Hudon
  • fix travis.yml, second try
  • feat(analysis/normed_space/deriv): add two missing lemmas

Estimated changes

added structure is_bounded_bilinear_map
added theorem differentiable.add
added theorem differentiable.congr'
added theorem differentiable.congr
added theorem differentiable.mul
added theorem differentiable.neg
added theorem differentiable.prod
added theorem differentiable.smul'
added theorem differentiable.smul
added theorem differentiable.sub
added def differentiable
added theorem differentiable_at.add
added theorem differentiable_at.comp
added theorem differentiable_at.mul
added theorem differentiable_at.neg
added theorem differentiable_at.prod
added theorem differentiable_at.smul
added theorem differentiable_at.sub
added theorem differentiable_at_id
added theorem differentiable_const
added theorem differentiable_id
added theorem differentiable_on.add
added theorem differentiable_on.comp
added theorem differentiable_on.mono
added theorem differentiable_on.mul
added theorem differentiable_on.neg
added theorem differentiable_on.prod
added theorem differentiable_on.smul
added theorem differentiable_on.sub
added theorem differentiable_on_id
added theorem differentiable_on_univ
added theorem fderiv.comp
added def fderiv
added theorem fderiv_add
deleted theorem fderiv_at_filter_unique
deleted theorem fderiv_at_unique
added theorem fderiv_const
added theorem fderiv_id
added theorem fderiv_mul
added theorem fderiv_neg
added theorem fderiv_smul'
added theorem fderiv_smul
added theorem fderiv_sub
added theorem fderiv_within.comp
added def fderiv_within
added theorem fderiv_within_add
added theorem fderiv_within_const
added theorem fderiv_within_id
added theorem fderiv_within_mul
added theorem fderiv_within_neg
added theorem fderiv_within_smul'
added theorem fderiv_within_smul
added theorem fderiv_within_sub
added theorem fderiv_within_univ
added theorem has_fderiv_at.add
added theorem has_fderiv_at.fderiv
added theorem has_fderiv_at.mul
added theorem has_fderiv_at.neg
added theorem has_fderiv_at.prod
added theorem has_fderiv_at.smul'
added theorem has_fderiv_at.smul
added theorem has_fderiv_at.sub
modified def has_fderiv_at
deleted theorem has_fderiv_at_add
modified theorem has_fderiv_at_filter.mono
modified def has_fderiv_at_filter
deleted theorem has_fderiv_at_filter_add
deleted theorem has_fderiv_at_filter_neg
deleted theorem has_fderiv_at_filter_smul
deleted theorem has_fderiv_at_filter_sub
modified theorem has_fderiv_at_iff_tendsto
deleted theorem has_fderiv_at_neg
deleted theorem has_fderiv_at_smul
deleted theorem has_fderiv_at_sub
added theorem has_fderiv_at_unique
deleted theorem has_fderiv_at_within.comp
deleted theorem has_fderiv_at_within.mono
deleted theorem has_fderiv_at_within_add
deleted theorem has_fderiv_at_within_id
deleted theorem has_fderiv_at_within_neg
deleted theorem has_fderiv_at_within_smul
deleted theorem has_fderiv_at_within_sub
added theorem is_open.unique_diff_on
added def tangent_cone_at
added theorem tangent_cone_mono
added theorem tangent_cone_univ
added theorem unique_diff_on.eq
added def unique_diff_on
added theorem unique_diff_on_inter
added def linear_map.prod
added theorem continuous_at.prod
modified theorem continuous_inclusion
added theorem continuous_on.prod
added theorem continuous_on.comp
added theorem continuous_on.mono
added theorem continuous_on_const