Commit 2023-12-02 16:31 c0f7586a

View on Github →

chore: Add limit spelling variation (#8477) Adding Tendsto (fun n : ℕ ↦ 1/(n : ℝ)) atTop (𝓝 0). We already have an equivalent statement but it is very hard to find and I've seen several students struggling to find it. I also took the opportunity to fix mapsto arrows in this file, but tendsto_one_div_atTop_nhds_0_nat is the only new content.

Estimated changes

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

modified theorem NNReal.hasSum_geometric

modified theorem NNReal.summable_geometric

modified theorem aux_hasSum_of_le_geometric

modified theorem hasSum_geometric_two'

modified theorem hasSum_geometric_two

modified theorem summable_geometric_two'

modified theorem summable_geometric_two

modified theorem tendsto_const_div_atTop_nhds_0_nat

modified theorem tendsto_inverse_atTop_nhds_0_nat

modified theorem tendsto_nat_ceil_div_atTop

modified theorem tendsto_nat_floor_div_atTop

added theorem tendsto_one_div_atTop_nhds_0_nat