Theorem contDiffOn_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) …

Modified contDiffOn_apply View on Github →

2025-05-13 11:52

Mathlib/Analysis/Calculus/ContDiff/Operations.lean

feat: fun_prop for ContDiff (#24056) …

Added contDiffOn_apply View on Github →