Christian Lawson-Perfect @christianp

Recent searches

Search options

Only available when logged in.

3 posts3 participants0 posts today

**José A. Alonso** @Jose_A_Alonso · 21h

#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 · Jun 12, 2021Monotonía de la imagen de conjuntosDemostrar 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

**José A. Alonso** @Jose_A_Alonso · 2d

José A. Alonso @Jose_A_Alonso

#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 · Jun 11, 2021Si 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

**José A. Alonso** @Jose_A_Alonso · 5d

José A. Alonso @Jose_A_Alonso

#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 · Jun 10, 2021Demostraciones 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 : α → β

**José A. Alonso** @Jose_A_Alonso · Apr 8

Apr 8

José A. Alonso @Jose_A_Alonso

#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

Calculemus · Jun 9, 2021Si f es inyectiva, entonces f⁻¹[f[s]] ⊆ sDemostrar 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

**José A. Alonso** @Jose_A_Alonso · Apr 7

Apr 7

José A. Alonso @Jose_A_Alonso

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

Calculemus · Jun 8, 2021Demostraciones 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

**José A. Alonso** @Jose_A_Alonso · Apr 6

Apr 6

José A. Alonso @Jose_A_Alonso

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

Calculemus · Jun 7, 2021Demostraciones 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 ⊆

**José A. Alonso** @Jose_A_Alonso · Apr 5

Apr 5

José A. Alonso @Jose_A_Alonso

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

Calculemus · Jun 6, 2021Demostraciones 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 : α → β)

**José A. Alonso** @Jose_A_Alonso · Apr 4

Apr 4

José A. Alonso @Jose_A_Alonso

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

Calculemus · Jun 5, 2021Demostraciones 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 : α

**José A. Alonso** @Jose_A_Alonso · Apr 3

Apr 3

José A. Alonso @Jose_A_Alonso

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

Calculemus · Jun 4, 2021Demostraciones 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

**José A. Alonso** @Jose_A_Alonso · Apr 2

Apr 2

José A. Alonso @Jose_A_Alonso

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

Calculemus · Jun 3, 2021Demostraciones 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

**José A. Alonso** @Jose_A_Alonso · Apr 1

Apr 1

José A. Alonso @Jose_A_Alonso

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

Calculemus · Jun 2, 2021Demostraciones 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

**José A. Alonso** @Jose_A_Alonso · Mar 31

Mar 31

José A. Alonso @Jose_A_Alonso

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

Calculemus · Jun 1, 2021Los primos mayores que 2 son imparesDemostrar 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

**José A. Alonso** @Jose_A_Alonso · Mar 30

Mar 30

José A. Alonso @Jose_A_Alonso

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

Calculemus · May 31, 2021La unión del conjunto de los números naturales pares e impares es el cDemostrar 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

**José A. Alonso** @Jose_A_Alonso · Mar 29

Mar 29

José A. Alonso @Jose_A_Alonso

Demostraciones con Lean4 y con Isabelle/HOL de "(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)". https://jaalonso.github.io/calculemus/posts/2021/05/28-diferencia_de_union_e_interseccion/ #LeanProver #IsabelleHOL #Math #Calculemus

Calculemus · May 28, 2021Demostraciones 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

**José A. Alonso** @Jose_A_Alonso · Mar 29

Mar 29

José A. Alonso @Jose_A_Alonso

Readings shared March 28, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/28-readings_shared_03-28-25 #AI #Calculemus #CompSci #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #LogicProgramming #Math #Philosophy #Programming #Prolog

Vestigium · Mar 28Readings shared February 28, 2025The 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,

**José A. Alonso** @Jose_A_Alonso · Mar 28

Mar 28

José A. Alonso @Jose_A_Alonso

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

Calculemus · May 27, 2021Demostraciones 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

**José A. Alonso** @Jose_A_Alonso · Mar 27

Mar 27

José A. Alonso @Jose_A_Alonso

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

Calculemus · May 26, 2021Unión con su intersecciónDemostrar 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

**José A. Alonso** @Jose_A_Alonso · Mar 25

Mar 25

José A. Alonso @Jose_A_Alonso

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

Calculemus · May 25, 2021Demostraciones 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

**José A. Alonso** @Jose_A_Alonso · Mar 24

Mar 24

José A. Alonso @Jose_A_Alonso

Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ t = t ∩ s". https://jaalonso.github.io/calculemus/posts/2021/05/24-conmutatividad_de_la_interseccion/ #LeanProver #IsabelleHOL #Math #Calculemus

Calculemus · May 24, 2021Demostraciones 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

**José A. Alonso** @Jose_A_Alonso · Mar 23

Mar 23

José A. Alonso @Jose_A_Alonso

Demostraciones con Lean4 y con Isabelle/HOL de "s \ (t ∪ u) ⊆ (s \ t) \ u". https://jaalonso.github.io/calculemus/posts/2021/05/21-diferencia_de_diferencia_de_conjuntos_2 #LeanProver #IsabelleHOL #Math #Calculemus

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

Drag & drop to upload

Recent searches

Search options

Administered by:

Server stats:

#Calculemus