If x is the limit of u and y is an upper bound of u, then x ≤ y
In Lean4, we can define that \(a\) is the limit of the sequence \(u\) by:
def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε
and that \(a\) is an upper bound of \(u\) by:
def is_upper_bound (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a
Prove that if \(x\) is the limit of the sequence \(u\) and \(y\) is an upper bound of \(u\), then \(x ≤ y\).
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (u : ℕ → ℝ) variable (x y : ℝ) def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε def is_upper_bound (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a example (hx : is_limit u x) (hy : is_upper_bound u y) : x ≤ y := by sorry