#calculemus — Public Fediverse posts

#Calculemus: Demostraciones con Lean 4 de "La sucesión 1/n converge a 0". https://jaalonso.github.io/calculemus/posts/2026/05/10-la_sucesion_1_div_n_converge_a_0/ #LeanProver #Math

#Calculemus: Demostraciones con Lean 4 de "Si a converge a L, entonces (∃ N)(∀ n ≥ N)[aₙ ≥ L - 1]". https://jaalonso.github.io/calculemus/posts/2026/06/03-cota_inferior_de_sucesiones_convergentes/ #LeanProver #Math

#Calculemus: Demostraciones con Lean 4 de "Si aₙ converge a L y bₙ a M, entonces aₙ+bₙ converge a L+M". https://jaalonso.github.io/calculemus/posts/2026/06/01-suma_de_sucesiones_convergentes #LeanProver #Math

#Calculemus: Demostraciones con Lean 4 de "Si aₙ converge a L, entonces 2aₙ converge a 2L". https://jaalonso.github.io/calculemus/posts/2026/05/21-duplicar_una_sucesion_convergente/ #LeanProver #Math

#Calculemus: Demostraciones con Lean 4 de "La sucesión 1, -1, 1, -1, ... no es convergente". https://jaalonso.github.io/calculemus/posts/2026/04/27-no_convergencia_-1n/ #LeanProver #Math

#Calculemus: Demostraciones con Lean 4 de "La sucesión aₙ = 1/n converge a 0". https://jaalonso.github.io/calculemus/posts/2026/04/11-convergencia_de_la_sucesion_1_div_n/ #LeanProver #Math

#Calculemus: Propiedad arquimediana de los números reales. https://jaalonso.github.io/calculemus/posts/2026/01/10-propiedad-arquimediana/ #LeanProver #Matemática

#Calculemus: Demostraciones con Lean4 de "La sucesión constante aₙ = L converge a L". https://jaalonso.github.io/calculemus/posts/2025/12/23-convergencia_de_la_sucesion_constante_v2/ #LeanProver #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]". https://jaalonso.github.io/calculemus/posts/2025/04/25-union_con_la_imagen_inversa #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] ∩ v = f[s ∩ f⁻¹[v]​]​". https://jaalonso.github.io/calculemus/posts/2025/04/24-interseccion_con_la_imagen_inversa/ #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∪ f⁻¹[v]​] ⊆ f[s] ∪ v". https://jaalonso.github.io/calculemus/posts/2025/04/23-union_con_la_imagen/ #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] ∩ t = f[s ∩ f⁻¹[t]]". https://jaalonso.github.io/calculemus/posts/2025/04/22-interseccion_con_la_imagen/ #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] \ f[t] ⊆ f[s \ t]​". https://jaalonso.github.io/calculemus/posts/2021/06/17-imagen_de_la_diferencia_de_conjuntos/ #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]​". https://jaalonso.github.io/calculemus/posts/2021/06/16-imagen_de_la_interseccion_de_aplicaciones_inyectivas/ #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∩ t] ⊆ f[s] ∩ f[t]​". https://jaalonso.github.io/calculemus/posts/2021/06/15-imagen_de_la_interseccion/ #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]". https://jaalonso.github.io/calculemus/posts/2021/06/14-imagen_inversa_de_la_union/ #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]​". https://jaalonso.github.io/calculemus/posts/2021/06/13-monotonia_de_la_imagen_inversa/ #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Monotonía de la imagen de conjuntos". https://jaalonso.github.io/calculemus/posts/2021/06/12-monotonia_de_la_imagen_de_conjuntos/ #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]​]". https://jaalonso.github.io/calculemus/posts/2021/06/11-imagen_de_imagen_inversa_de_aplicaciones_suprayectivas/ #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[f⁻¹[u]​] ⊆ u". https://jaalonso.github.io/calculemus/posts/2021/06/10-imagen_de_la_imagen_inversa/ #LeanProver #IsabelleHOL #Math

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es inyectiva, entonces f⁻¹[f[s]] ⊆ s". https://jaalonso.github.io/calculemus/posts/2021/06/09-imagen_inversa_de_la_imagen_de_aplicaciones_inyectivas/ #LeanProver #IsabelleHOL #Math

Demostraciones con Lean4 y con Isabelle/HOL de "f(s) ⊆ u ↔ s ⊆ f⁻¹(u)". https://jaalonso.github.io/calculemus/posts/2021/06/08-subconjunto_de_la_imagen_inversa/ #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones con Lean4 y con Isabelle/HOL de "s ⊆ f⁻¹(f(s))". https://jaalonso.github.io/calculemus/posts/2021/06/07-imagen_inversa_de_la_imagen/ #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones con Lean4 y con Isabelle/HOL de "f(s ∪ t) = f(s) ∪ f(t)". https://jaalonso.github.io/calculemus/posts/2021/06/06-imagen_de_la_union/ #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v)". https://jaalonso.github.io/calculemus/posts/2021/06/05-imagen_inversa_de_la_interseccion/ #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s)". https://jaalonso.github.io/calculemus/posts/2021/06/04-union_con_interseccion_general/ #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones con Lean4 y con Isabelle/HOL de "⋂_i, (A(i) ∩ B(i)) = (⋂_i, A(i)) ∩ (⋂_i, B(i))". https://jaalonso.github.io/calculemus/posts/2021/06/03-interseccion_de_intersecciones/ #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ ⋃_i A(i) = ⋃_i (A(i) ∩ s)". https://jaalonso.github.io/calculemus/posts/2021/06/02-distributiva_de_la_interseccion_respecto_de_la_union_general/ #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones con Lean4 y con Isabelle/HOL de "Los primos mayores que 2 son impares". https://jaalonso.github.io/calculemus/posts/2021/06/01-interseccion_de_los_primos_y_los_mayores_que_dos/ #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones con Lean4 y con Isabelle/HOL de "La unión del conjunto de los números naturales pares e impares es el conjunto de los naturales". https://jaalonso.github.io/calculemus/posts/2021/05/31-union_de_pares_e_impares/ #LeanProver #IsabelleHOL #Math #Calculemus