Demostrar con Lean4 que si la sucesión \(u\) converge a \(a\) y la \(v\) a \(b\), entonces \(u+v\) converge a \(a+b\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {s t : ℕ → ℝ} {a b c : ℝ} def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by sorry
En Lean, una sucesión \(s₀, s₁, s₂, ...\) se puede representar mediante una función \((s : ℕ → ℝ)\) de forma que \(s(n)\) es \(sₙ\).
Se define que a es el límite de la sucesión \(s\), por
def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε
Demostrar que el límite de la sucesión constante \(sₙ = c\) es \(c\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε example : limite (fun _ : ℕ ↦ c) c := by sorry
Demostrar con Lean4 que en \(ℝ\), si \(1 < a\), entonces \(a < aa\)
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable {a : ℝ} example (h : 1 < a) : a < a * a := by sorry
Demostrar con Lean4 que en \(ℝ\), \(|a| = |a - b + b|\)
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b : ℝ) example : |a| = |a - b + b| := by sorry
Demostrar con Lean4 que las funciones \(f(x,y) = (x + y)²\) y \(g(x,y) = x² + 2xy + y\)² son iguales.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) := by sorry
Demostrar con Lean4 que la raíz cuadrada de 2 es irracional; es decir, que no existen \(m, n ∈ ℕ\) tales que \(m\) y \(n\) son coprimos (es decir, que no tienen factores comunes distintos de uno) y \(m² = 2n²\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic import Mathlib.Data.Nat.Prime.Defs open Nat variable {m n : ℕ} example : ¬∃ m n, coprime m n ∧ m ^ 2 = 2 * n ^ 2 := by sorry
Demostrar con Lean4 que si (n²) es par, entonces (n) es par.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Nat variable (n : ℕ) example (h : 2 ∣ n ^ 2) : 2 ∣ n := by sorry
Demostrar con Lean4 que existen infinitos números primos.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic import Mathlib.Data.Nat.Prime.Defs open Nat example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by sorry
Demostrar con Lean4 que \[ (P → Q) ↔ ¬P ∨ Q \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable (P Q : Prop) example : (P → Q) ↔ ¬P ∨ Q := by sorry
Demostrar con Lean4 que \[ ¬¬P → P \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable (P : Prop) example : ¬¬P → P := by sorry