Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-26 20:52 53f98786

View on Github →

refactor(analysis/normed_space): use bundled type for fderiv (#956)

  • feat(analysis/normed_space): refactor fderiv to use bounded_linear_map
  • uniqueness remains sorry'd
  • more simp lemmas about bounded_linear_map
  • refactor uniqueness proof
  • fix(analysis/normed_space/operator_norm): rename bound_le_op_norm to op_norm_le_bound
  • so that the inequality goes the correct way.

Estimated changes

modified theorem fderiv_at_filter_unique
modified theorem fderiv_at_unique
modified theorem has_fderiv_at.comp
modified theorem has_fderiv_at.congr
modified theorem has_fderiv_at.continuous_at
deleted theorem has_fderiv_at.is_o
modified def has_fderiv_at
modified theorem has_fderiv_at_add
modified theorem has_fderiv_at_congr
modified theorem has_fderiv_at_filter.comp
modified theorem has_fderiv_at_filter.congr
deleted theorem has_fderiv_at_filter.is_o
modified theorem has_fderiv_at_filter.mono
modified def has_fderiv_at_filter
modified theorem has_fderiv_at_filter_add
modified theorem has_fderiv_at_filter_congr'
modified theorem has_fderiv_at_filter_congr
modified theorem has_fderiv_at_filter_id
modified theorem has_fderiv_at_filter_neg
modified theorem has_fderiv_at_filter_smul
modified theorem has_fderiv_at_filter_sub
modified theorem has_fderiv_at_id
modified theorem has_fderiv_at_iff_tendsto
modified theorem has_fderiv_at_neg
modified theorem has_fderiv_at_smul
modified theorem has_fderiv_at_sub
modified theorem has_fderiv_at_within.comp
modified theorem has_fderiv_at_within.congr
modified theorem has_fderiv_at_within.mono
modified def has_fderiv_at_within
modified theorem has_fderiv_at_within_add
modified theorem has_fderiv_at_within_congr
modified theorem has_fderiv_at_within_id
modified theorem has_fderiv_at_within_neg
modified theorem has_fderiv_at_within_smul
modified theorem has_fderiv_at_within_sub