Commit 2026-02-03 23:11 ea1575fd

View on Github →

chore(Analysis/SchwartzSpace): make some definitions private (#34552)

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean

deleted theorem SchwartzMap.bounds_bddBelow

deleted theorem SchwartzMap.bounds_nonempty

deleted theorem SchwartzMap.decay_add_le_aux

deleted theorem SchwartzMap.decay_neg_aux

deleted theorem SchwartzMap.decay_smul_aux

deleted theorem SchwartzMap.le_seminormAux

deleted theorem SchwartzMap.seminormAux_add_le

deleted theorem SchwartzMap.seminormAux_le_bound

deleted theorem SchwartzMap.seminormAux_nonneg

deleted theorem SchwartzMap.seminormAux_smul_le

deleted theorem SchwartzMap.seminormAux_zero

added theorem SchwartzMap.seminorm_apply