Commit 2023-06-10 09:37 4354bcb1

View on Github →

feat: add ContinuousAt.comp_of_eq (#4904) Forward-port of leanprover-community/mathlib#18877 (2 files)

Estimated changes

Modified Mathlib/Analysis/Calculus/FDeriv/Prod.lean

deleted theorem DifferentiableAt.fderivWithin_prod

added theorem DifferentiableWithinAt.fderivWithin_prod

Modified Mathlib/Topology/Basic.lean

added theorem ContinuousAt.comp_of_eq