Un monoide cancelativo por la izquierda es un monoide \(M\) que cumple la propiedad cancelativa por la izquierda; es decir, para todo \(a, b ∈ M\) \[ a·b = a·c ↔ b = c \]

En Lean4 la clase de los monoides cancelativos por la izquierda es LeftCancelMonoid y la propiedad cancelativa por la izquierda es

   mul_left_cancel : a * b = a * c → b = c

Demostrar con Lean4 que si \(M\) es un monoide cancelativo por la izquierda y \(a, b ∈ M\), entonces \[ a·b = a ↔ b = 1 \]

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

import Mathlib.Algebra.Group.Basic

variable {M : Type} [LeftCancelMonoid M]
variable {a b : M}

example : a * b = a ↔ b = 1 :=
by sorry

Read more…

Demostrar con Lean4 que si \(M\) es un monoide conmutativo y \(x, y, z ∈ M\) tales que \(x·y = 1\) y \(x·z = 1\), entonces \(y = z\).

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

import Mathlib.Algebra.Group.Basic

variable {M : Type} [CommMonoid M]
variable {x y z : M}

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
by sorry

Read more…

Sea \(M\) un monoide y \(a, b ∈ M\) tales que \(ab = 1\). Demostrar con Lean4 que \(a = 1\) si y sólo si \(b = 1\).

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

import Mathlib.Algebra.Group.Basic

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
by sorry

Read more…

En los monoides se define la potencia con exponentes naturales. En Lean la potencia x^n se se caracteriza por los dos siguientes lemas:

   pow_zero : x^0 = 1
   pow_succ : x^(succ n) = x * x^n

Demostrar con Lean4 que si \(M\) es un monoide, \(x ∈ M\) y \(m, n ∈ ℕ\), entonces \[ x^{m + n} = x^m x^n \]

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

import Mathlib.Algebra.Group.Defs
import Mathlib.Tactic

open Nat

variable {M : Type} [Monoid M]
variable (x : M)
variable (m n : ℕ)

example :
  x^(m + n) = x^m * x^n :=
by sorry

Read more…

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

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
import Mathlib.Tactic

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

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…