En ℝ, |a| = |a – b + b|
Demostrar con Lean4 que en \(ℝ\), \(|a| = |a – b + b|\)
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : |a| = |a - b + b| := by sorry |
Las funciones f(x,y) = (x + y)² y g(x,y) = x² + 2xy + y² son iguales
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:
|
1 2 3 4 |
import Mathlib.Data.Real.Basic example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) := by sorry |
Read More «Las funciones f(x,y) = (x + y)² y g(x,y) = x² + 2xy + y² son iguales»
La raíz cuadrada de 2 es irracional
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:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic import Mathlib.Data.Nat.Prime import Std.Data.Nat.Gcd open Nat variable {m n : ℕ} example : ¬∃ m n, coprime m n ∧ m ^ 2 = 2 * n ^ 2 := by sorry |
Si n² es par, entonces n es par
Demostrar con Lean4 que si \(n²\) es par, entonces \(n\) es par.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic open Nat variable (n : ℕ) example (h : 2 ∣ n ^ 2) : 2 ∣ n := by sorry |
Existen infinitos números primos
Demostrar con Lean4 que existen infinitos números primos.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic import Mathlib.Data.Nat.Prime open Nat example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by sorry |
(P → Q) ↔ ¬P ∨ Q
Demostrar con Lean4 que
\[ (P → Q) ↔ ¬P ∨ Q \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable (P Q : Prop) example : (P → Q) ↔ ¬P ∨ Q := by sorry |
¬¬P → P
Demostrar con Lean4 que
\[ ¬¬P → P \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Tactic variable (P : Prop) example : ¬¬P → P := by sorry |
En ℝ, x² = y² → x = y ∨ x = -y
Demostrar con Lean4 que en \(ℝ\),
\[x² = y² → x = y ∨ x = -y\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) example (h : x^2 = y^2) : x = y ∨ x = -y := by sorry |
En ℝ, si x² = 1 entonces x = 1 ó x = -1
Demostrar con Lean4 que en \(ℝ\), si \(x² = 1\) entonces \(x = 1\) ó \(x = -1\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) example (h : x^2 = 1) : x = 1 ∨ x = -1 := by sorry |
Si (∃ x, y ∈ ℝ)[z = x² + y² ∨ z = x² + y² + 1], entonces z ≥ 0
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:
|
1 2 3 4 5 6 7 8 |
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 |
Read More «Si (∃ x, y ∈ ℝ)[z = x² + y² ∨ z = x² + y² + 1], entonces z ≥ 0»