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.

Author: PatrickMassot