José A. Alonso

Si (∀n)[uₙ ≤ vₙ], entonces lim uₙ ≤ lim vₙ

PorJosé A. Alonso 31 mayo 202431 mayo 2024

En Lean4, una sucesión \(u_0, u_1, u_2, \dots\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es el \(n\)-ésimo término de la sucesión.

Se define que \(a\) límite de la sucesión \(u\) como sigue

   def limite (u : ℕ → ℝ) (c : ℝ) :=
     ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

1 2	def limite (u : ℕ → ℝ) (c : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, \|u n - c\| < ε

Demostrar que si \((∀ n)[u_n ≤ v_n]\), \(a\) es límite de \(u_n\) y \(c\) es límite de \(v_n\), entonces \(a ≤ c\).

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

import Mathlib.Data.Real.Basic

variable (u v : ℕ → ℝ)
variable (a c : ℝ)

def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

example
  (hu : limite u a)
  (hv : limite v c)
  (huv : ∀ n, u n ≤ v n)
  : a ≤ c :=
by sorry

import Mathlib.Data.Real.Basic

variable (u v : ℕ → ℝ)

variable (a c : ℝ)

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

example

(hu : limite u a)

(hv : limite v c)

(huv : ∀ n, u n ≤ v n)

: a ≤ c :=

by sorry

Si x, y ∈ ℝ tales que (∀ z)[y < z → x ≤ z], entonces x ≤ y

PorJosé A. Alonso 30 mayo 202429 mayo 2024

Demostrar con Lean4 que si \(x, y ∈ ℝ\) tales que \((∀ z)[y < z → x ≤ z]\), entonces \(x ≤ y\).

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

import Mathlib.Data.Real.Basic

variable {x y : ℝ}

example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
by sorry

import Mathlib.Data.Real.Basic

variable {x y : ℝ}

example

(h : ∀ z, y < z → x ≤ z) :

x ≤ y :=

by sorry

La paradoja del barbero

PorJosé A. Alonso 29 mayo 202428 mayo 2024

Demostrar con Lean4 la paradoja del barbero; es decir, que no existe un hombre que afeite a todos los que no se afeitan a sí mismo y sólo a los que no se afeitan a sí mismo.

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

import Mathlib.Tactic

variable (Hombre : Type)
variable (afeita : Hombre → Hombre → Prop)

example :
  ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=
by sorry

import Mathlib.Tactic

variable (Hombre : Type)

variable (afeita : Hombre → Hombre → Prop)

example :

¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=

by sorry

Las sucesiones convergentes están acotadas

PorJosé A. Alonso 28 mayo 202426 mayo 2024

Demostrar con Lean4 que si \(u_n\) es una sucesión convergente, entonces está acotada; es decir,
\[ (∃ k ∈ ℕ)(∃ b ∈ ℝ)(∀ n ∈ ℕ)[n ≥ k → |u_n| ≤ b] \]

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {u : ℕ → ℝ}

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
by sorry

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

variable {u : ℕ → ℝ}

-- (limite u c) expresa que el límite de u es c.

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.

def convergente (u : ℕ → ℝ) :=

∃ a, limite u a

example

(h : convergente u)

: ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=

by sorry

Un número es par si y solo si lo es su cuadrado

PorJosé A. Alonso 27 mayo 202423 mayo 2024

Demostrar con Lean4 que un número es par si y solo si lo es su cuadrado.

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

import Mathlib.Data.Int.Parity
import Mathlib.Tactic
open Int

variable (n : ℤ)

example :
  Even (n^2) ↔ Even n :=
by sorry

import Mathlib.Data.Int.Parity

import Mathlib.Tactic

open Int

variable (n : ℤ)

example :

Even (n^2) ↔ Even n :=

by sorry

Los supremos de las sucesiones crecientes son sus límites

PorJosé A. Alonso 24 mayo 202422 mayo 2024

Sea \(u\) una sucesión creciente. Demostrar con Lean4 que si \(S\) es un supremo de \(u\), entonces el límite de \(u\) es \(S\).

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

import Mathlib.Data.Real.Basic

variable (u : ℕ → ℝ)
variable (S : ℝ)

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - c| ≤ ε

-- (supremo u S) expresa que el supremo de u es S.
def supremo (u : ℕ → ℝ) (S : ℝ) :=
  (∀ n, u n ≤ S) ∧ ∀ ε > 0, ∃ k, u k ≥ S - ε

example
  (hu : Monotone u)
  (hS : supremo u S)
  : limite u S :=
by sorry

import Mathlib.Data.Real.Basic

variable (u : ℕ → ℝ)

variable (S : ℝ)

-- (limite u c) expresa que el límite de u es c.

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - c| ≤ ε

-- (supremo u S) expresa que el supremo de u es S.

def supremo (u : ℕ → ℝ) (S : ℝ) :=

(∀ n, u n ≤ S) ∧ ∀ ε > 0, ∃ k, u k ≥ S - ε

example

(hu : Monotone u)

(hS : supremo u S)

: limite u S :=

by sorry

Si `f(x) ≤ f(y) → x ≤ y`, entonces f es inyectiva

PorJosé A. Alonso 23 mayo 202421 mayo 2024

Demostrar con Lean4 que si \(f\) una función de \(ℝ\) en \(ℝ\) tal que
\[ (∀ x, y)[f(x) ≤ f(y) → x ≤ y] \]
entonces \(f\) es inyectiva.

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

import Mathlib.Data.Real.Basic
open Function

variable (f : ℝ → ℝ)

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : Injective f :=
by sorry

import Mathlib.Data.Real.Basic

open Function

variable (f : ℝ → ℝ)

example

(h : ∀ {x y}, f x ≤ f y → x ≤ y)

: Injective f :=

by sorry

Si una función es creciente e involutiva, entonces es la identidad

PorJosé A. Alonso 22 mayo 202420 mayo 2024

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 involutiva si para todo \(x\) se tiene que \(f(f(x)) = x\).

En Lean4 que \(f\) sea creciente se representa por Monotone f y que sea involutiva por Involutive f

Demostrar con Lean4 que si \(f\) es creciente e involutiva, entonces \(f\) es la identidad.

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

import Mathlib.Data.Real.Basic
open Function

variable (f : ℝ → ℝ)

example
  (hc : Monotone f)
  (hi : Involutive f)
  : f = id :=
by sorry

import Mathlib.Data.Real.Basic

open Function

variable (f : ℝ → ℝ)

example

(hc : Monotone f)

(hi : Involutive f)

: f = id :=

by sorry

La composición de una función creciente y una decreciente es decreciente

PorJosé A. Alonso 21 mayo 202417 mayo 2024

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

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

Los monoides booleanos son conmutativos

PorJosé A. Alonso 20 mayo 202416 mayo 2024

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

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

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