Commit 2025-08-03 15:47 df4985fa

View on Github →

chore: fix wrong namespacing of Tendsto.num (#27893) Spotted by using the docs.

Estimated changes

Modified Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

added theorem Filter.Tendsto.den

added theorem Filter.Tendsto.num

added theorem Filter.Tendsto.num_atTop_iff_den_atTop

deleted theorem Tendsto.den

deleted theorem Tendsto.num

deleted theorem Tendsto.num_atTop_iff_den_atTop