mayo 2024 – Página 3

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