Commit 2020-07-02 18:55 e4fdc750

View on Github →

refactor(analysis/calculus/*deriv): use eventually_eq in congruence statements (#3261) Use eventually_eq instead of mem_sets for congruence lemmas in continuity and differentiability statements.

Estimated changes

Modified src/analysis/calculus/deriv.lean

deleted theorem deriv_congr_of_mem_nhds

deleted theorem deriv_within_congr_of_mem_nhds_within

added theorem filter.eventually_eq.deriv_eq

added theorem filter.eventually_eq.deriv_within_eq

added theorem filter.eventually_eq.has_deriv_at_filter_iff

added theorem has_deriv_at.congr_of_eventually_eq

deleted theorem has_deriv_at.congr_of_mem_nhds

added theorem has_deriv_at_filter.congr_of_eventually_eq

deleted theorem has_deriv_at_filter.congr_of_mem_sets

deleted theorem has_deriv_at_filter_congr_of_mem_sets

added theorem has_deriv_within_at.congr_of_eventually_eq

deleted theorem has_deriv_within_at.congr_of_mem_nhds_within

Modified src/analysis/calculus/fderiv.lean

added theorem differentiable_at.congr_of_eventually_eq

deleted theorem differentiable_at.congr_of_mem_nhds

added theorem differentiable_within_at.comp'

added theorem differentiable_within_at.congr_of_eventually_eq

deleted theorem differentiable_within_at.congr_of_mem_nhds_within

deleted theorem fderiv_congr_of_mem_nhds

deleted theorem fderiv_within_congr_of_mem_nhds_within

added theorem filter.eventually_eq.fderiv_eq

added theorem filter.eventually_eq.fderiv_within_eq

added theorem filter.eventually_eq.has_fderiv_at_filter_iff

added theorem filter.eventually_eq.has_strict_fderiv_at_iff

added theorem has_fderiv_at.congr_of_eventually_eq

deleted theorem has_fderiv_at.congr_of_mem_nhds

added theorem has_fderiv_at_filter.congr_of_eventually_eq

deleted theorem has_fderiv_at_filter.congr_of_mem_sets

deleted theorem has_fderiv_at_filter_congr_of_mem_sets

added theorem has_fderiv_within_at.congr_of_eventually_eq

deleted theorem has_fderiv_within_at.congr_of_mem_nhds_within

added theorem has_strict_fderiv_at.congr_of_eventually_eq

deleted theorem has_strict_fderiv_at.congr_of_mem_sets

deleted theorem has_strict_fderiv_at_congr_of_mem_sets

Modified src/analysis/calculus/inverse.lean

Modified src/analysis/calculus/specific_functions.lean

Modified src/analysis/special_functions/pow.lean

Modified src/geometry/manifold/basic_smooth_bundle.lean

Modified src/geometry/manifold/mfderiv.lean

added theorem filter.eventually_eq.mdifferentiable_within_at_iff

added theorem filter.eventually_eq.mfderiv_eq

added theorem filter.eventually_eq.mfderiv_within_eq

added theorem has_mfderiv_at.congr_of_eventually_eq

deleted theorem has_mfderiv_at.congr_of_mem_nhds

added theorem has_mfderiv_within_at.congr_of_eventually_eq

deleted theorem has_mfderiv_within_at.congr_of_mem_nhds_within

added theorem mdifferentiable_at.congr_of_eventually_eq

deleted theorem mdifferentiable_at.congr_of_mem_nhds

added theorem mdifferentiable_within_at.congr_of_eventually_eq

deleted theorem mdifferentiable_within_at.congr_of_mem_nhds_within

deleted theorem mdifferentiable_within_at_congr_of_mem_nhds_within

deleted theorem mfderiv_congr_of_mem_nhds

deleted theorem mfderiv_within_congr_of_mem_nhds_within

Modified src/order/filter/basic.lean

added theorem filter.eventually.exists_mem

added theorem filter.eventually_eq.exists_mem

added theorem filter.eventually_eq_iff_exists_mem

added theorem filter.eventually_eq_of_mem

added theorem filter.eventually_iff_exists_mem

Modified src/topology/continuous_on.lean

added theorem continuous_on.comp'

added theorem continuous_within_at.comp'

added theorem continuous_within_at.congr_of_eventually_eq

deleted theorem continuous_within_at.congr_of_mem_nhds_within