Si (∀n)[uₙ ≤ vₙ], entonces lim uₙ ≤ lim vₙ
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
|
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:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
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 |