Theorem ContDiffOn.fun_div

Modification history

2026-06-23 09:25
Mathlib/Analysis/Calculus/ContDiff/Operations.lean
feat: tag the pointwise Continuous/ContDiff/Measurable operation families with to_fun (#40872) …
Deleted ContDiffOn.fun_divView on Github →
2025-05-13 11:52
Mathlib/Analysis/Calculus/ContDiff/Operations.lean
feat: fun_prop for ContDiff (#24056) …
Added ContDiffOn.fun_divView on Github →