La sucesión aₙ = 1/n converge a 0

En Lean, una sucesión \(a₀, a₁, a₂, ...\) se puede representar mediante una función \((a : ℕ → ℝ)\) de forma que \(a(n)\) es \(aₙ\). Se define que \(L\) es el límite de la sucesión \(a\), por def LimS