Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-26 16:34 7e2d4b85

View on Github →

feat(analysis/calculus/extend_deriv): extend differentiability to the boundary (#1794)

feat(analysis/calculus/extend_deriv): extend differentiability to the boundary
fix build

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem has_deriv_within_at.congr

added theorem has_deriv_within_at.union

Created src/analysis/calculus/extend_deriv.lean

added theorem has_deriv_at_interval_left_endpoint_of_tendsto_deriv

added theorem has_fderiv_at_boundary_of_tendsto_fderiv

added theorem has_fderiv_at_boundary_of_tendsto_fderiv_aux

added theorem has_fderiv_at_interval_right_endpoint_of_tendsto_deriv

Modified src/analysis/calculus/fderiv.lean

added theorem has_fderiv_within_at.congr

added theorem has_fderiv_within_at.union

Modified src/analysis/specific_limits.lean

added theorem tendsto_inv_zero_at_top

Modified src/data/set/intervals/basic.lean

added theorem set.Iic_union_Ici

added theorem set.Iic_union_Ioi

added theorem set.Iio_union_Ici