単調増加

まずは数列の極限の証明を見て見ましょう。 $$\lim_{n\to\infty}n = \infty\hspace{20cm}$$ example : Tendsto (fun n:ℕ => n) atTop atTop := by exact tendsto_id exact一発で終わるということは全く同じか、より一般化された証明があるということです。この場合は少し一般化された定理tendsto_idがすでにmathlib4にあり、それが使われました。 tendsto_idという定理はFilter.tendsto_id.{u_1} {α : Type u_1} {x : Filter α} …