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 \(cuₙ\) es \(ca\).

Para ello, completar la siguiente teoría de Lean4:

1. Demostración en lenguaje natural

Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Tenemos que demostrar que
\[ (∃ N ∈ ℕ)(∀ n ≥ N)[|cuₙ – ca| < ε] \tag{1}\]
Distinguiremos dos casos según sea \(c = 0\) o no.

Primer caso: Supongamos que \(c = 0\). Entonces, (1) se reduce a
\[ (∃ N ∈ ℕ)(∀ n ≥ N)[|0·uₙ – 0·a| < ε] \]
es decir,
\[ (∃ N ∈ ℕ)(∀ n ≥ N)[0 < ε] \]
que se verifica para cualquier número \(N\), ya que \(ε > 0\).

Segundo caso: Supongamos que \(c ≠ 0\). Entonces, \(\dfrac{ε}{|c|}\) > 0 y, puesto que el límite de \(uₙ\) es \(a\), existe un \(k ∈ ℕ\) tal que
\[ (∀ n ≥ k)[|uₙ – a| < \frac{ε}{|c|}] \tag{2} \]
Veamos que con \(k\) se cumple (1). En efecto, sea \(n ≥ k\). Entonces,
\begin{align}
|cuₙ – ca| &= |c(uₙ – a)| \\
&= |c||uₙ – a| \\
&< |c|\frac{ε}{|c|} &&\text{[por (2)]} \\
&= ε
\end{align}

2. Demostraciones con Lean4

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

Escribe un comentario