Sea una función \(f\) de \(ℝ\) en \(ℝ\). Se dice que \(f\) es creciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≤ f(y)\). Se dice que \(f\) es decreciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≥ f(y)\).

Demostrar con Lean4 que si \(f\) es creciente y \(g\) es decreciente, entonces \(g ∘ f\) es decreciente.

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

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

def creciente (f : ℝ → ℝ) : Prop :=
  ∀ {x y}, x ≤ y → f x ≤ f y

def decreciente (f : ℝ → ℝ) : Prop :=
  ∀ {x y}, x ≤ y → f x ≥ f y

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
by sorry

Read more…

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

Un monoide \(M\) es booleano si \[ (∀ x ∈ M)[x·x = 1] \] y es conmutativo si \[ (∀ x, y ∈ M)[x·y = y·x] \]

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 con Lean4 que los monoides booleanos son conmutativos.

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

import Mathlib.Algebra.Group.Basic

variable {M : Type} [Monoid M]

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
by sorry

Read more…

Demostrar con Lean4 que si \(M\) es un monoide, \(a ∈ M\) y \(m, n ∈ ℕ\), entonces \[ a^{m·n} = (a^m)^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 (a : M)
variable (m n : ℕ)

example : a^(m * n) = (a^m)^n :=
by sorry

Read more…

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b, c ∈ G\) tales que \(a·b = a·c\), entonces \(b = c\).

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

import Mathlib.Algebra.Group.Basic

variable {G : Type} [Group G]
variable {a b c : G}

example
  (h: a * b = a  * c)
  : b = c :=
sorry

Read more…

Demostrar con Lean4 que si \(G\) un grupo y \(a ∈ G\), entonces \[(a⁻¹)⁻¹ = a\]

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

import Mathlib.Algebra.Group.Basic

variable {G : Type} [Group G]
variable {a : G}

example : (a⁻¹)⁻¹ = a :=
sorry

Read more…

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\), entonces \((ab)^{-1} = b^{-1}a^{-1}\).

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

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (a b : G)

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
sorry

Read more…

Demostrar con Lean4 que si \(a\) es un elemento de un grupo \(G\), entonces \(a\) tiene un único inverso; es decir, si \(b\) es un elemento de \(G\) tal que \(a·b = 1\), entonces \(a⁻¹ = b\).

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

import Mathlib.Algebra.Group.Basic

variable {G : Type} [Group G]
variable {a b : G}

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

Read more…

Demostrar con Lean4 que un grupo sólo posee un elemento neutro.

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

import Mathlib.Algebra.Group.Basic

variable {G : Type} [Group G]

example
  (e : G)
  (h : ∀ x, x * e = x)
  : e = 1 :=
sorry

Read more…

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…