José A. Alonso3d ago
#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
José A. AlonsoApr 27
#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
La sucesión 1, -1, 1, -1, ... no es convergente

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

Calculemus
José A. AlonsoApr 11
#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
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

Calculemus
José A. AlonsoJan 10
#Calculemus: Propiedad arquimediana de los números reales. https://jaalonso.github.io/calculemus/posts/2026/01/10-propiedad-arquimediana/ #LeanProver #Matemática
José A. AlonsoDec 23
#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
José A. AlonsoApr 25, 2025
#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
Demostraciones de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]"

Demostrar con Lean4 y con Isabelle/HOL que \[ s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v] \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Function open Set variable {α β : Type _} varia

Calculemus
José A. AlonsoApr 24, 2025
#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
Demostraciones de "f[s] ∩ v = f[s ∩ f⁻¹[v]​]​"

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s] ∩ v = f[s ∩ f⁻¹[v]] \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable

Calculemus
José A. AlonsoApr 23, 2025
#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
Demostraciones de "f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v"

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable

Calculemus
José A. AlonsoApr 22, 2025
#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
Demostraciones de "f[s] ∩ t = f[s ∩ f⁻¹[t]]"

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s] ∩ t = f[s ∩ f⁻¹[t]] \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable

Calculemus
José A. AlonsoApr 21, 2025
#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
Demostraciones de "f[s] \ f[t] ⊆ f[s \ t]"

Demostrar con Lean4 y con Isabelle/HOL que \[f[s] \setminus f[t] ⊆ f[s \setminus t] \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Function import Mathlib.Tactic open S

Calculemus