Theorem SchwartzMap.norm_toBoundedContinuousFunction_le

Modification history

2026-03-10 22:48
Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
feat(Analysis/SchwartzMap): estimates for `Lp` and `BCF` norms (#35953)
Added SchwartzMap.norm_toBoundedContinuousFunction_leView on Github →