Theorem differentiableWithinAt_congr_set_nhdsNE

Modification history

2026-02-04 18:01
Mathlib/Analysis/Calculus/FDeriv/Congr.lean
feat(FDeriv/Congr): generalize to TVS (#34843)
Added differentiableWithinAt_congr_set_nhdsNEView on Github →