Demostrar que si la sucesión \(a\) converge a \(L\), entonces \[ (∃ N)(∀ n ≥ N)[aₙ ≥ L - 1] \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a : ℕ → ℝ} variable {L : ℝ} def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : SeqLim a L) : ∃ N, ∀ n ≥ N, a n ≥ L - 1 := by sorry
Demostrar que si \(aₙ\) converge a \(L\) y \(bₙ\) a \(M\), entonces \(aₙ+bₙ\) converge a \(L+M\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a b c : ℕ → ℝ} variable {L M : ℝ} def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : SeqLim a L) (hb : SeqLim b M) : SeqLim (a + b) (L + M) := by sorry
Demostrar que existen infinitos números primos.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Tactic import Mathlib.Data.Nat.Prime.Defs open Nat example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by sorry
Demostrar con Lean 4 que si la sucesión \(aₙ\) converge a \(L\), entonces \(2aₙ\) converge a \(2L\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a : ℕ → ℝ) def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : SeqLim a L) (hb : ∀ n, b n = 2 * a n) : SeqLim b (2 * L) := by sorry
Demostrar que la sucesión definida por 1, -1, 1, -1,... no converge.
Para ello, se propone completar la siguiente demostración en Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a : ℕ → ℝ} def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε def SeqConv (a : ℕ → ℝ) : Prop := ∃ L, SeqLim a L example (ha : ∀ n, a n = (-1) ^ n) : ¬ SeqConv a := by sorry
En Lean, una sucesión \(a₀, a₁, a₂,...\) se puede representar mediante una función \(a : ℕ → ℝ\) de forma que \(a(n)\) es \(aₙ\).
Se define que \(L\) es el límite de la sucesión \(a\), por
def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε
Demostrar que si para todo \(n\), \(aₙ = 1/n\), entonces la sucesión \(a\) converge a 0.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a : ℕ → ℝ) def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε example (ha : ∀ n, a n = 1 / n) : SeqLim a 0 := by sorry
He empezado a publicar la serie Retos matemáticos en Lean 4.
La dinámica es sencilla: cada semana propondré un problema matemático para que quienes estén interesados compartan sus soluciones en Lean 4.
Al terminar la semana publicaré las soluciones del reto, que seguirán este esquema:
grind.norm_num, ring, positivity o linarith.Con este refinamiento sucesivo se pretende que la demostración final se corresponda, en la medida de lo posible, con la escrita en lenguaje natural.
Demostrar con Lean4 e Isabelle/HOL que si \(s\) es un subconjunto del dominio de la función \(f\), entonces \(s\) está contenido en la imagen inversa de la imagen de \(s\) por \(f\); es decir, \[ s ⊆ f⁻¹[f[s]] \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (s : Set α) example : s ⊆ f ⁻¹' (f '' s) := by sorry
y la siguiente teoría de Isabelle/HOL:
theory Imagen_inversa_de_la_imagen imports Main begin lemma "s ⊆ f -` (f ` s)" sorry end
Demostrar con Lean4 y con Isabelle/HOL que \[ f(s ∪ t) = f(s) ∪ f(t) \] Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Set.Function variable {α β : Type _} variable (f : α → β) variable (s t : Set α) open Set example : f '' (s ∪ t) = f '' s ∪ f '' t := by sorry
y la siguiente teoría de Isabelle/HOL:
theory Imagen_de_la_union imports Main begin lemma "f ` (s ∪ t) = f ` s ∪ f ` t" sorry end
Demostrar con Lean4 y con Isabelle/HOL que
f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v)
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Set.Function variable {α β : Type _} variable (f : α → β) variable (u v : Set β) open Set example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := by sorry
y la siguiente teoría de Iasbelle/HOL:
theory Imagen_inversa_de_la_interseccion imports Main begin lemma "f -` (u ∩ v) = f -` u ∩ f -` v" sorry end