Theorem HasSumUniformlyOn.of_norm_le_summable_eventually

Modification history

2025-08-11 19:22
Mathlib/Topology/Algebra/InfiniteSum/TsumUniformlyOn.lean
Iterated derivatives of tsum's within some open set. (#26016) …
Added HasSumUniformlyOn.of_norm_le_summable_eventuallyView on Github →