Theorem ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm_withOrder

Modification history

2026-03-07 10:30

Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

refactor(Distributions): remove "WithOrder" duplication (#36301) …

Deleted ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm_withOrder View on Github →

2025-11-27 16:17

Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

feat(Analysis/Distribution/ContDiffMapSupportedIn): add withSeminorms statement (#30236) …

Added ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm_withOrder View on Github →