Theorem ContDiffMapSupportedIn.monoLM_apply

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.monoLM_applyView on Github →