José A. Alonso

En los monoides, los inversos a la izquierda y a la derecha son iguales

PorJosé A. Alonso 3 mayo 20243 mayo 2024

Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.

En Lean4, está definida la clase de los monoides (como Monoid) y sus propiedades características son

   mul_assoc : (a * b) * c = a * (b * c)
   one_mul :   1 * a = a
   mul_one :   a * 1 = a

mul_assoc : (a * b) * c = a * (b * c)

one_mul : 1 * a = a

mul_one : a * 1 = a

Demostrar que si \(M\) es un monoide, \(a ∈ M\), \(b\) es un inverso de \(a\) por la izquierda y \(c\) es un inverso de \(a\) por la derecha, entonces \(b = c\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Algebra.Group.Defs

variable {M : Type} [Monoid M]
variable {a b c : M}

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
by sorry

import Mathlib.Algebra.Group.Defs

variable {M : Type} [Monoid M]

variable {a b c : M}

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

by sorry

Teorema de Cantor

PorJosé A. Alonso 2 mayo 2024

Demostrar con Lean4 el teorema de Cantor; es decir, que no existe ninguna aplicación suprayectiva de un conjunto en el conjunto de sus subconjuntos.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Set.Basic
open Function

variable {α : Type}

example : ∀ f : α → Set α, ¬Surjective f :=
by sorry

import Mathlib.Data.Set.Basic

open Function

variable {α : Type}

example : ∀ f : α → Set α, ¬Surjective f :=

by sorry

Imagen inversa de la intersección general

PorJosé A. Alonso 1 mayo 20241 mayo 2024

Demostrar con Lean4 que
\[ f⁻¹\left[\bigcap_{i \in I} B_i\right] = \bigcap_{i \in I} f⁻¹[B_i] \]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α β I : Type _}
variable (f : α → β)
variable (B : I → Set β)

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α β I : Type _}

variable (f : α → β)

variable (B : I → Set β)

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=

by sorry

Imagen inversa de la unión general

PorJosé A. Alonso 30 abril 202430 abril 2024

Demostrar con Lean4 que
\[ f⁻¹\left[⋃ᵢ Bᵢ\right] = ⋃ᵢ f⁻¹[Bᵢ] \]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α β I : Type _}
variable (f : α → β)
variable (B : I → Set β)

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α β I : Type _}

variable (f : α → β)

variable (B : I → Set β)

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=

by sorry

Imagen de la interseccion general mediante aplicaciones inyectivas

PorJosé A. Alonso 29 abril 202430 abril 2024

Demostrar con Lean4 que si \(f\) es inyectiva, entonces
\[⋂ᵢf[Aᵢ] ⊆ f\left[⋂ᵢAᵢ\right] \]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set Function

variable {α β I : Type _}
variable (f : α → β)
variable (A : I → Set α)

example
  (i : I)
  (injf : Injective f)
  : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=
by
sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set Function

variable {α β I : Type _}

variable (f : α → β)

variable (A : I → Set α)

example

(i : I)

(injf : Injective f)

: (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=

sorry

Imagen de la intersección general

PorJosé A. Alonso 26 abril 202426 abril 2024

Demostrar con Lean4 que
\[ f\left[\bigcap_{i ∈ I} A_i\right] ⊆ \bigcap_{i ∈ I} f[A_i] \]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α β I : Type _}
variable (f : α → β)
variable (A : I → Set α)

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α β I : Type _}

variable (f : α → β)

variable (A : I → Set α)

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=

by sorry

Imagen de la unión general

PorJosé A. Alonso 25 abril 202425 abril 2024

Demostrar con Lean4 que
\[ f[⋃ᵢAᵢ] = ⋃ᵢf[Aᵢ] \]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α β I : Type _}
variable (f : α → β)
variable (A : ℕ → Set α)

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α β I : Type _}

variable (f : α → β)

variable (A : ℕ → Set α)

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=

by sorry

Read More «Imagen de la unión general»

Unión con la imagen inversa

PorJosé A. Alonso 24 abril 202424 abril 2024

Demostrar con Lean4 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 _}
variable (f : α → β)
variable (s : Set α)
variable (v : Set β)

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=
by sorry

import Mathlib.Data.Set.Function

open Set

variable {α β : Type _}

variable (f : α → β)

variable (s : Set α)

variable (v : Set β)

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=

by sorry

Read More «Unión con la imagen inversa»

Intersección con la imagen

PorJosé A. Alonso 23 abril 202422 abril 2024

Demostrar con Lean4 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 {α β : Type _}
variable (f : α → β)
variable (s : Set α)
variable (v : Set β)

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=
by sorry

import Mathlib.Data.Set.Function

import Mathlib.Tactic

open Set

variable {α β : Type _}

variable (f : α → β)

variable (s : Set α)

variable (v : Set β)

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=

by sorry

Read More «Intersección con la imagen»

Unión con la imagen

PorJosé A. Alonso 22 abril 202422 abril 2024

Demostrar con Lean4 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 (α β : Type _)
variable (f : α → β)
variable (s : Set α)
variable (v : Set β)

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=
by sorry

import Mathlib.Data.Set.Function

import Mathlib.Tactic

open Set

variable (α β : Type _)

variable (f : α → β)

variable (s : Set α)

variable (v : Set β)

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=

by sorry