#Calculemus: Demostraciones con Lean 4 del Reto 15 (Existe un k ∈ ℕ tal que, para todo n ∈ ℕ, (n + k)² ≤ 2ⁿ⁺ᵏ). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

#Calculemus: Demostraciones con Lean 4 del Reto 14 (Para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

#Calculemus: Demostraciones con Lean 4 del Reto 13 (Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

#Calculemus: Demostraciones con Lean 4 del Reto 12 (Si aₙ → L, bₙ → M y L < M, entonces eventualmente aₙ < bₙ). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

#Calculemus: Demostraciones con Lean 4 del Reto 11 (Si aₙ converge a L, entonces |aₙ| converge a |L|). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

#Calculemus: Demostraciones con Lean 4 del Reto 10 (Si aₙ → L con L ≠ 0, entonces |aₙ| ≥ |L|/2 eventualmente). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

#Calculemus: Demostraciones con Lean 4 del Reto 9 (Unicidad del límite). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

#Calculemus: Demostraciones con Lean 4 del Reto 8 (Sucesiones con infinitos términos grandes no convergen a límites pequeños). jaalonso.github.io/calculemus/p... #Math

#Calculemus: Demostraciones con Lean 4 del Reto 7 (La composición de funciones inyectivas es inyectiva). jaalonso.github.io/calculemus/p... #LeanProver #Math

#Calculemus: Demostraciones con Lean 4 del Reto 6 (teorema del emparedado). jaalonso.github.io/calculemus/p... #LeanProver #Math