Demostrar con Lean4 que en los órdenes parciales, \[a < b ↔ a ≤ b ∧ a ≠ b\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {α : Type _} [PartialOrder α] variable (a b : α) example : a < b ↔ a ≤ b ∧ a ≠ b := by sorry
Demostrar con Lean4 que la función \(x ↦ -x\) no es monótona creciente.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic example : ¬Monotone fun x : ℝ ↦ -x := by sorry
Demostrar con Lean4 que \(f: ℝ → ℝ\) no es monótona syss \((∃x,y)[x ≤ y ∧ f(x) > f(y)]\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable {f : ℝ → ℝ} example : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := sorry
Demostrar con Lean4 que 3 divide al máximo común divisor de 6 y 15.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic open Nat example : 3 ∣ gcd 6 15 := by sorry
Demostrar con Lean4 que si \(|x + 3| < 5\), entonces \(-8 < x < 2\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (x y : ℝ) example : |x + 3| < 5 → -8 < x ∧ x < 2 := by sorry
Demostrar con Lean4 que si \(x, y ∈ ℝ\), entonces \[ x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {x y : ℝ} example : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := by sorry
Demostrar con Lean4 que si \(x\) e \(y\) son números reales tales que \(x ≤ y\), entonces \(y ≰ x ↔ x ≠ y\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by sorry
Demostrar con Lean4 que. en \(ℝ\), \(x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (x y : ℝ) example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by sorry
Demostrar con Lean4 que existen números primos \(m\) y \(n\) tales que \(4 < m < n < 10\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Nat.Prime.Defs import Mathlib.Tactic example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by sorry
Demostrar con Lean4 que si \((∃z ∈ ℝ)[x < z < y]\), entonces \(x < y\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (x y : ℝ) example : (∃ z : ℝ, x < z ∧ z < y) → x < y := by sorry