Theorem contDiffWithinAt_apply

Modification history

2026-10-13 09:24

Mathlib/Analysis/Calculus/ContDiff/Operations.lean

chore(Analysis/Calculus/ContDiff/Operations): extract `contDiffWithinAt_apply`, and generalise (#44821) …

Added contDiffWithinAt_apply View on Github →