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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : LimSuc 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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : LimSuc a L) (hb : LimSuc b M) : LimSuc (a + b) (L + M) := by sorry
Demostrar que si aₙ converge a L, entonces 2aₙ converge a 2L.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a : ℕ → ℝ) def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : LimSuc a L) (hb : ∀ n, b n = 2 * a n) : LimSuc b (2 * L) := 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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε
También se define que \(a\) es convergente por
def SucConv (a : ℕ → ℝ) : Prop := ∃ L, LimSuc a L
Demostrar que si para todo \(n\), \(aₙ = (-1)^n\), entonces la sucesión \(a\) no es convergente.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a : ℕ → ℝ} def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε def SucConv (a : ℕ → ℝ) : Prop := ∃ L, LimSuc a L example (ha : ∀ n, a n = (-1) ^ n) : ¬ SucConv 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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε
Demostrar que si para todo \(n\), \(aₙ = \frac{1}{n}\), entonces la sucesión \(a\) converge a \(0\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a : ℕ → ℝ) def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : ∀ n, a n = 1 / n) : LimSuc a 0 := by sorry
Demostrar la propiedad arquimediana de los números reales; es decir, que para cualquier \(ε ∈ ℝ\) con \(0 < ε\), existe \(N ∈ ℕ\) tal que \(1/ε < N\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {ε : ℝ} variable (h : 0 < ε) example : ∃ (N : ℕ), 1 / ε < N := 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 LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε
Demostrar que si para todo \(n\), \(aₙ = L\), entonces la sucesión \(a\) converge a \(L\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a : ℕ → ℝ) variable (L : ℝ) def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (h : ∀ n, a n = L) : LimSuc a L := by sorry
Demostrar con Lean4 y con Isabelle/HOL que \[ s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v] \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (s : Set α) variable (v : Set β) example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) := by sorry
y la siguiente teoría de Isabelle/HOL:
theory Union_con_la_imagen_inversa imports Main begin lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)" sorry end
Demostrar con Lean4 y con Isabelle/HOL que \[ f[s] ∩ v = f[s ∩ f⁻¹[v]] \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable {α β : Type _} variable (f : α → β) variable (s : Set α) variable (v : Set β) example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) := by sorry
y la siguiente teoría de Isabelle/HOL:
theory Interseccion_con_la_imagen_inversa imports Main begin lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)" sorry end
Demostrar con Lean4 y con Isabelle/HOL que \[ f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable (α β : Type _) variable (f : α → β) variable (s : Set α) variable (v : Set β) example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v := by sorry
y la siguiente teoría de Isabelle/HOL:
theory Union_con_la_imagen imports Main begin lemma "f ` (s ∪ f -` v) ⊆ f ` s ∪ v" sorry end