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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…