Theorem ContDiffMapSupportedIn.monoCLM_eq_zero

Modification history

2026-03-18 18:00
Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean
feat: monotonicity of D^n(U) in n and in U as CLMs (#32401)
Added ContDiffMapSupportedIn.monoCLM_eq_zeroView on Github →