Commit 2026-10-13 09:24 387f8cc1
View on Github →chore(Analysis/Calculus/ContDiff/Operations): extract contDiffWithinAt_apply, and generalise (#44821)
Extract contDiffWithinAt_apply (which was just missing API), and generalise this lemma and its friends to a product of potentially different spaces F i instead of just a single space.
Extracted from #44371.