#Calculemus: Propiedad arquimediana de los números reales. jaalonso.github.io/calculemus/p... #LeanProver #Matemática

#Calculemus: Demostraciones con Lean4 de "La sucesión constante aₙ = L converge a L". jaalonso.github.io/calculemus/p... #LeanProver #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: Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]". jaalonso.github.io/calculemus/p... #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: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] ∩ v = f[s ∩ f⁻¹[v]​]​". jaalonso.github.io/calculemus/p... #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: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∪ f⁻¹[v]​] ⊆ f[s] ∪ v". jaalonso.github.io/calculemus/p... #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: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] ∩ t = f[s ∩ f⁻¹[t]]". jaalonso.github.io/calculemus/p... #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: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] \ f[t] ⊆ f[s \ t]​". jaalonso.github.io/calculemus/p... #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: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]​". jaalonso.github.io/calculemus/p... #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: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∩ t] ⊆ f[s] ∩ f[t]​". jaalonso.github.io/calculemus/p... #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: Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math

Monotonía de la imagen inversa Demostrar con Lean4 y con Isabelle/HOL que si \(u ⊆ v\), entonces \(f⁻¹[u] ⊆ f⁻¹[v]\). Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Function open Set variable {α β : Typ

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

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

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Monotonía de la imagen de conjuntos". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math

Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]​] Demostrar con Lean4 y con Isabelle/HOL que si \(f\) es suprayectiva, entonces \[ u ⊆ f[f⁻¹[u]] \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Function open Set Function

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

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

#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[f⁻¹[u]​] ⊆ u". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math

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

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

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

Demostraciones con Lean4 y con Isabelle/HOL de "f(s) ⊆ u ↔ s ⊆ f⁻¹(u)". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones de "s ⊆ f⁻¹(f(s))" Demostrar con Lean4 e Isabelle/HOL que si \(s\) es un subconjunto del dominio de la función \(f\), entonces \(s\) está contenido en la imagen inversa de la imagen de \(s\) por \(f\); es decir, \[ s ⊆

Demostraciones con Lean4 y con Isabelle/HOL de "s ⊆ f⁻¹(f(s))". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

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 variable {α β : Type _} variable (f : α → β)

Demostraciones con Lean4 y con Isabelle/HOL de "f(s ∪ t) = f(s) ∪ f(t)". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones de "f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v)" Demostrar con Lean4 y con Isabelle/HOL que f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v) Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Function variable {α β : Type _} variable (f : α

Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v)". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones de "s ∪ (⋂_i A_i) = ⋂_i (A_i ∪ s)" Demostrar con Lean4 y con Isabelle/HOL que \[ s ∪ (⋂_i A_i) = ⋂_i (A_i ∪ s) \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable

Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s)". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones de "⋂_i, (A(i) ∩ B(i)) = (⋂_i, A(i)) ∩ (⋂_i, B(i))" Demostrar con Lean4 y con Isabelle/HOL que \[ ⋂_i (A_i ∩ B_i) = (⋂_i A_i) ∩ (⋂_i B_i) \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Basic import Mathlib.Tactic open Se

Demostraciones con Lean4 y con Isabelle/HOL de "⋂_i, (A(i) ∩ B(i)) = (⋂_i, A(i)) ∩ (⋂_i, B(i))". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones de "s ∩ ⋃_i A_i = ⋃_i (A_i ∩ s)" Demostrar con Lean4 y con Isabelle/HOL que \[ s ∩ ⋃_i A_i = ⋃_i (A_i ∩ s) \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Lattice import Mat

Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ ⋃_i A(i) = ⋃_i (A(i) ∩ s)". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

Los primos mayores que 2 son impares Demostrar con Lean4 y con Isabelle/HOL que los primos mayores que 2 son impares. Para ello, completar la siguiente teoría de Lean4: import Mathlib.Algebra.Ring.Parity import Mathlib.Tactic open Nat

Demostraciones con Lean4 y con Isabelle/HOL de "Los primos mayores que 2 son impares". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

La unión del conjunto de los números naturales pares e impares es el c Demostrar con Lean4 y con Isabelle/HOL que la unión del conjunto de los números naturales pares e impares es el conjunto de los naturales. Para ello, completar la siguiente teoría de Lean4: import Mat

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". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones de "(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)" Demostrar con Lean4 y con Isabelle/HOL que \[ (s \setminus t) ∪ (t \setminus s) = (s ∪ t) \setminus (s ∩ t) \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Basic import M

Demostraciones con Lean4 y con Isabelle/HOL de "(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

Readings shared February 28, 2025 The readings shared in Bluesky on 28 March 2025 are A gentle introduction to Isabelle and Isabelle/HOL. ~ Gunnar Teege. #ITP #IsabelleHOL Verified collaboration: How Lean is transforming mathematics,

Readings shared March 28, 2025. jaalonso.github.io/vestigium/po... #AI #Calculemus #CompSci #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #LogicProgramming #Math #Philosophy #Programming #Prolog

Demostraciones de "(s \ t) ∪ t = s ∪ t" Demostrar con Lean4 y con Isabelle/HOL que \[ (s \setminus t) ∪ t = s ∪ t \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s

Demostraciones con Lean4 y con Isabelle/HOL de "(s \ t) ∪ t = s ∪ t". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

Unión con su intersección Demostrar con Lean4 y con Isabelle/HOL que \[ s ∪ (s ∩ t) = s \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t : Set α) e

Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (s ∩ t) = s". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones de "s ∩ (s ∪ t) = s" Demostrar con Lean4 y con Isabelle/HOL que \[ s ∩ (s ∪ t) = s \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α : Type} var

Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ (s ∪ t) = s". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus

Demostraciones de "s ∩ t = t ∩ s" Demostrar con Lean4 y con Isabelle/HOL que \[ s ∩ t = t ∩ s \] Para ello, completar la siguiente teoría de Lean4: import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t : Set α) exa

Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ t = t ∩ s". jaalonso.github.io/calculemus/p... #LeanProver #IsabelleHOL #Math #Calculemus