Demostrar con Lean4 el teorema del emparedado.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
import Mathlib.Data.Real.Basic variable (u v w : ℕ → ℝ) variable (a : ℝ) def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε example (hu : limite u a) (hw : limite w a) (h1 : ∀ n, u n ≤ v n) (h2 : ∀ n, v n ≤ w n) : limite v a := by sorry |
Demostrar con Lean4 que si \(uₙ\) y \(vₙ\) convergen a \(0\), entonces \(uₙvₙ\) converge a \(0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u v : ℕ → ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (hu : limite u 0) (hv : limite v 0) : limite (u * v) 0 := by sorry |
Read More «Si uₙ y vₙ convergen a 0, entonces uₙvₙ converge a 0»
Demostrar con Lean4 que el límite de \(uₙ\) es \(a\) si, y sólo si, el de \(uₙ-a\) es \(0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} variable {a c x : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example : limite u a ↔ limite (fun i ↦ u i - a) 0 := by sorry |
Demostrar con Lean4 que si el límite de la sucesión \(uₙ\) es \(a\) y \(c ∈ ℝ\), entonces el límite de \(cuₙ\) es \(ca\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (u v : ℕ → ℝ) variable (a c : ℝ) def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (h : limite u a) : limite (fun n ↦ c * (u n)) (c * a) := by |
Read More «Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de cuₙ es ca»
Demostrar con Lean4 que si el límite de la sucesión \(uₙ\) es \(a\) y \(c ∈ ℝ\), entonces el límite de \(uₙ+c\) es \(a+c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} variable {a c : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (h : limite u a) : limite (fun i ↦ u i + c) (a + c) := by sorry |
Read More «Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de uₙ+c es a+c»