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:
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:
import Mathlib.Tactic import Mathlib.Data.Nat.Prime.Defs open Nat example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by sorry
Implicación mediante disyunción y negación
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
Eliminación de la doble negación
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
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:
import Mathlib.Data.Real.Basic import Mathlib.Tactic 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:
import Mathlib.Data.Real.Basic import Mathlib.Tactic 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:
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
Si m divide a n o a k, entonces m divide a nk.
Demostrar con Lean4 que si \(m\) divide a \(n\) o a \(k\), entonces \(m\) divide a \(nk\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {m n k : ℕ} example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by sorry
En ℝ, si x ≠ 0 entonces x < 0 ó x > 0
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
En ℝ, |x + y| ≤ |x| + |y|
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