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

Leer más…

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

Leer más…

Demostrar con Lean4 que si \(≤\) es un preorden, entonces \(<\) es transitiva.

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

import Mathlib.Tactic
variable {α : Type _} [Preorder α]
variable (a b c : α)

example : a < b → b < c → a < c :=
by sorry

Leer más…

Demostrar con Lean4 que si \(≤\) es un preorden, entonces \(<\) es irreflexiva.

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

import Mathlib.Tactic
variable {α : Type _} [Preorder α]
variable (a : α)

example : ¬a < a :=
by sorry

Leer más…

Demostrar con Lean4 que en los órdenes parciales, \[a < b ↔ a ≤ b ∧ a ≠ b\]

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

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable (a b : α)

example : a < b ↔ a ≤ b ∧ a ≠ b :=
by sorry

Leer más…

Demostrar con Lean4 que si \(a\) es una cota superior de \(s\) y \(a ≤ b\), entonces \(b\) es una cota superior de \(s\).

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

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable (s : Set α)
variable (a b : α)

-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.
def CotaSupConj (s : Set α) (a : α) :=
  ∀ {x}, x ∈ s → x ≤ a

example
  (h1 : CotaSupConj s a)
  (h2 : a ≤ b)
  : CotaSupConj s b :=
by sorry

Leer más…

Demostrar con Lean4 que, en los anillos ordenados, \[ \{a ≤ b, 0 ≤ c\} ⊢ ac ≤ bc \]

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

import Mathlib.Algebra.Order.Ring.Defs
variable {R : Type _} [StrictOrderedRing R]
variable (a b c : R)

example
  (h1 : a ≤ b)
  (h2 : 0 ≤ c)
  : a * c ≤ b * c :=
by sorry

Leer más…

Demostrar con Lean4 que en los anillos ordenados \[ 0 ≤ b - a → a ≤ b \]

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

import Mathlib.Algebra.Order.Ring.Defs
variable {R : Type _} [StrictOrderedRing R]
variable (a b c : R)

example : 0 ≤ b - a → a ≤ b :=
by sorry

Leer más…

Demostrar con Lean4 que en los anillos ordenados se verifica que \[ a ≤ b → 0 ≤ b - a \]

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

import Mathlib.Algebra.Order.Ring.Defs
variable {R : Type _} [StrictOrderedRing R]
variable (a b c : R)

example : a ≤ b → 0 ≤ b - a :=
by sorry

Leer más…

Demostrar con Lean4 que si \(R\) es un retículo tal que \[ (∀ x,\ y,\ z \in α) [x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)] \] entonces \[ (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) \] para todos los elementos del retículo.

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

import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (a b c : α)

example
  (h : ∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z))
  : (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) :=
by sorry

Leer más…