Demostrar la propiedad arquimediana de los números reales; es decir, que para cualquier \(ε ∈ ℝ\) con \(0 < ε\), existe \(N ∈ ℕ\) tal que \(1/ε < N\).

Para ello, completar la siguiente teoría de Lean 4:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {ε : ℝ}
variable (h : 0 < ε)

example : ∃ (N : ℕ), 1 / ε < N :=
by sorry

Leer más…

Demostrar con Lean4 que si \(x, y ∈ ℝ\) tales que \((∀ z)[y < z → x ≤ z]\), entonces \(x ≤ y\).

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

import Mathlib.Data.Real.Basic

variable {x y : ℝ}

example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
by sorry

Leer más…

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

Leer más…

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

Leer más…

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

Leer más…

Demostrar con Lean4 que en \(ℝ\), \[x² = y² → x = y ∨ x = -y\]

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (x y : ℝ)

example
  (h : x^2 = y^2)
  : x = y ∨ x = -y :=
by sorry

Leer más…

Demostrar con Lean4 que en \(ℝ\), si \(x² = 1\) entonces \(x = 1\) ó \(x = -1\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (x y : ℝ)

example
  (h : x^2 = 1)
  : x = 1 ∨ x = -1 :=
by sorry

Leer más…

Demostrar con Lean4 que si \((∃ x, y ∈ ℝ)[z = x² + y² ∨ z = x² + y² + 1]\), entonces \(z ≥ 0\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic
variable {z : ℝ}

example
  (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1)
  : z ≥ 0 :=
by sorry

Leer más…

Demostrar con Lean4 que en ℝ, si \(x ≠ 0\) entonces \(x < 0\) ó \(x > 0\).

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

import Mathlib.Data.Real.Basic
variable {x : ℝ}

example
  (h : x ≠ 0)
  : x < 0 ∨ x > 0 :=
by sorry

Leer más…

Demostrar con Lean4 que en \(ℝ\), \[ |x + y| ≤ |x| + |y| \]

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {x y : ℝ}

example : |x + y| ≤ |x| + |y| :=
by sorry

Leer más…