Theorem ContinuousLinearMap.norm_iteratedFDerivWithin_comp_left

Modification history

2025-12-10 17:42
Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
feat(Analysis/Calculus): norm bound for iterated derivatives of composition with CLM (#32572)
Added ContinuousLinearMap.norm_iteratedFDerivWithin_comp_leftView on Github →