Lean 4 challenge 25: If the interleaving of two sequences converges to L, then both converge to L.
https://jaalonso.github.io/calculemus/en/posts/2026/10/26-convergencia_de_la_mezcla_de_sucesiones/
#lean4challenge — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #lean4challenge, aggregated by home.social.
-
Leab 4 Challenge 24: The sequence 1, -1, 1, -1,... is not convergent (2nd version).
https://jaalonso.github.io/calculemus/en/posts/2026/10/19-no_convergencia_-1n_v2/