#Calculemus - Sigmoid Social

0 posts0 participants0 posts today

José A. Alonso @Jose_A_Alonso@mathstodon.xyz

#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 · Apr 25Demostraciones 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

José A. Alonso @Jose_A_Alonso@mathstodon.xyz

#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 · Apr 24Demostraciones 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

José A. Alonso @Jose_A_Alonso@mathstodon.xyz

#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 · Apr 23Demostraciones 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

José A. Alonso @Jose_A_Alonso@mathstodon.xyz

#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 · Apr 22Demostraciones 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

José A. Alonso @Jose_A_Alonso@mathstodon.xyz

#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 · Jun 17, 2021Demostraciones 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

José A. Alonso @Jose_A_Alonso@mathstodon.xyz

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

José A. Alonso @Jose_A_Alonso@mathstodon.xyz

#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 · Jun 15, 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 import Mathlib.Tactic open Set variable {

José A. Alonso @Jose_A_Alonso@mathstodon.xyz

#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 · Jun 14, 2021Demostraciones 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

José A. Alonso @Jose_A_Alonso@mathstodon.xyz

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

José A. Alonso @Jose_A_Alonso@mathstodon.xyz

#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@mathstodon.xyz

#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@mathstodon.xyz

#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@mathstodon.xyz

#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@mathstodon.xyz

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@mathstodon.xyz

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@mathstodon.xyz

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@mathstodon.xyz

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@mathstodon.xyz

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@mathstodon.xyz

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@mathstodon.xyz

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

Drag & drop to upload