Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-01 10:20 d74804bd

View on Github →

add has_fderiv_at_filter

Estimated changes

Modified src/analysis/asymptotics.lean

added theorem asymptotics.is_bigo.congr

added theorem asymptotics.is_bigo.congr_of_sub

added theorem asymptotics.is_bigo.symm

added theorem asymptotics.is_bigo.trans_tendsto

added theorem asymptotics.is_bigo.tri

added theorem asymptotics.is_bigo_comm

added theorem asymptotics.is_bigo_congr

added theorem asymptotics.is_bigo_congr_left

added theorem asymptotics.is_bigo_congr_right

modified theorem asymptotics.is_bigo_neg_left

modified theorem asymptotics.is_bigo_norm_left

added theorem asymptotics.is_bigo_refl_left

added theorem asymptotics.is_littleo.congr

added theorem asymptotics.is_littleo.congr_of_sub

added theorem asymptotics.is_littleo.symm

added theorem asymptotics.is_littleo.trans_tendsto

added theorem asymptotics.is_littleo.tri

added theorem asymptotics.is_littleo_comm

added theorem asymptotics.is_littleo_congr

added theorem asymptotics.is_littleo_congr_left

added theorem asymptotics.is_littleo_congr_right

modified theorem asymptotics.is_littleo_neg_left

modified theorem asymptotics.is_littleo_norm_left

added theorem asymptotics.is_littleo_refl_left

Modified src/analysis/normed_space/bounded_linear_maps.lean

added theorem is_bounded_linear_map.is_bigo_comp

Modified src/analysis/normed_space/deriv.lean

deleted theorem chain_rule

deleted theorem chain_rule_at_within

deleted theorem continuous_at_of_has_fderiv_at

deleted theorem continuous_at_within_of_has_fderiv_at_within

added theorem has_fderiv_at.comp

modified theorem has_fderiv_at.congr

added theorem has_fderiv_at.continuous_at

modified theorem has_fderiv_at_add

added theorem has_fderiv_at_congr

added theorem has_fderiv_at_filter.comp

added theorem has_fderiv_at_filter.congr

added theorem has_fderiv_at_filter.is_bigo_sub

added theorem has_fderiv_at_filter.is_littleo

added theorem has_fderiv_at_filter.mono

added theorem has_fderiv_at_filter.tendsto_nhds

added def has_fderiv_at_filter

added theorem has_fderiv_at_filter_add

added theorem has_fderiv_at_filter_congr'

added theorem has_fderiv_at_filter_congr

added theorem has_fderiv_at_filter_const

added theorem has_fderiv_at_filter_equiv_aux

added theorem has_fderiv_at_filter_id

added theorem has_fderiv_at_filter_iff_tendsto

added theorem has_fderiv_at_filter_neg

added theorem has_fderiv_at_filter_of_has_fderiv_at

added theorem has_fderiv_at_filter_smul

added theorem has_fderiv_at_filter_sub

modified theorem has_fderiv_at_neg

modified theorem has_fderiv_at_sub

added theorem has_fderiv_at_within.comp

added theorem has_fderiv_at_within.continuous_at_within

modified theorem has_fderiv_at_within_add

added theorem has_fderiv_at_within_congr

deleted theorem has_fderiv_at_within_equiv_aux

modified theorem has_fderiv_at_within_neg

modified theorem has_fderiv_at_within_of_has_fderiv_at

modified theorem has_fderiv_at_within_sub

Modified src/order/filter/basic.lean

added theorem filter.congr_sets

added theorem filter.tendsto.congr'

deleted theorem filter.tendsto_cong

added theorem filter.tendsto_congr

Modified src/topology/continuity.lean

added theorem continuous_at_within.tendsto_nhds_within_image