Difference_Between_Adjacent_Square_Roots_Converges
Provedlimits-of-sequencesproofwiki
The sequence sqrt(n+1) - sqrt(n) converges to 0.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Difference_Between_Adjacent_Square_Roots_Converges : Filter.Tendsto (fun n : ℕ => Real.sqrt ((n : ℝ) + 2) - Real.sqrt ((n : ℝ) + 1)) Filter.atTop (nhds 0) := by sorry
Source