Theorem ContDiffMapSupportedIn.seminorm_monoLM_eq

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