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
José A. AlonsoApr 20, 2025
#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
Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]

Demostrar con Lean4 y con Isabelle/HOL que si \(f\) es inyectiva, entonces \[ f[s] ∩ f[t] ⊆ f[s ∩ t] \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Function open Set Fu

Calculemus
José A. AlonsoApr 19, 2025
#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
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 18, 2025
#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
Demostraciones de "f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]​"

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

Calculemus