Sin categoría – Calculemus

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 G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c

PorJosé A. Alonso 16 mayo 202412 mayo 2024

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

import Mathlib.Algebra.Group.Basic

variable {G : Type} [Group G]

variable {a b c : G}

example

(h: a * b = a * c)

: b = c :=

sorry

Producto de potencias de la misma base en monoides

PorJosé A. Alonso 6 mayo 20245 mayo 2024

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

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

1 2	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.Algebra.GroupPower.Basic
open Nat

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

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

import Mathlib.Algebra.Group.Defs

import Mathlib.Algebra.GroupPower.Basic

open Nat

variable {M : Type} [Monoid M]

variable (x : M)

variable (m n : ℕ)

example :

x^(m + n) = x^m * x^n :=

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

Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]

PorJosé A. Alonso 4 abril 20244 abril 2024

Demostrar con Lean4 que si \(u ⊆ v\), entonces \(f⁻¹[u] ⊆ f⁻¹[v]\).

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

import Mathlib.Data.Set.Function
open Set

variable {α β : Type _}
variable (f : α → β)
variable (u v : Set β)

example
  (h : u ⊆ v)
  : f ⁻¹' u ⊆ f ⁻¹' v :=
by sorry

import Mathlib.Data.Set.Function

open Set

variable {α β : Type _}

variable (f : α → β)

variable (u v : Set β)

example

(h : u ⊆ v)

: f ⁻¹' u ⊆ f ⁻¹' v :=

by sorry

Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]]

PorJosé A. Alonso 2 abril 20242 abril 2024

Demostrar con Lean4 que si \(f\) es suprayectiva, entonces
\[ u ⊆ f[f⁻¹[u]] \]

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

import Mathlib.Data.Set.Function
open Set Function
variable {α β : Type _}
variable (f : α → β)
variable (u : Set β)

example
  (h : Surjective f)
  : u ⊆ f '' (f⁻¹' u) :=
by sorry

import Mathlib.Data.Set.Function

open Set Function

variable {α β : Type _}

variable (f : α → β)

variable (u : Set β)

example

(h : Surjective f)

: u ⊆ f '' (f⁻¹' u) :=

by sorry

Si n² es par, entonces n es par

PorJosé A. Alonso 26 enero 202426 enero 2024

Demostrar con Lean4 que si \(n²\) es par, entonces \(n\) es par.

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

import Mathlib.Tactic
open Nat
variable (n : ℕ)

example
  (h : 2 ∣ n ^ 2)
  : 2 ∣ n :=
by sorry

import Mathlib.Tactic

open Nat

variable (n : ℕ)

example

(h : 2 ∣ n ^ 2)

: 2 ∣ n :=

by sorry

Existen infinitos números primos

PorJosé A. Alonso 25 enero 202424 enero 2024

Demostrar con Lean4 que existen infinitos números primos.

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

import Mathlib.Tactic
import Mathlib.Data.Nat.Prime
open Nat

example
  (n : ℕ) :
  ∃ p, n ≤ p ∧ Nat.Prime p :=
by sorry

import Mathlib.Tactic

import Mathlib.Data.Nat.Prime

open Nat

example

(n : ℕ) :

∃ p, n ≤ p ∧ Nat.Prime p :=

by sorry

(P → Q) ↔ ¬P ∨ Q

PorJosé A. Alonso 24 enero 202419 enero 2024

Demostrar con Lean4 que
\[ (P → Q) ↔ ¬P ∨ Q \]

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

import Mathlib.Tactic
variable (P Q : Prop)

example
  : (P → Q) ↔ ¬P ∨ Q :=
by sorry

import Mathlib.Tactic

variable (P Q : Prop)

example

: (P → Q) ↔ ¬P ∨ Q :=

by sorry

¬¬P → P

PorJosé A. Alonso 23 enero 202417 enero 2024

Demostrar con Lean4 que
\[ ¬¬P → P \]

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

import Mathlib.Tactic
variable (P : Prop)

example : ¬¬P → P :=
by sorry

import Mathlib.Tactic

variable (P : Prop)

example : ¬¬P → P :=

by sorry