Demostrar con Lean4 que en \(ℝ\),
\[ |x + y| ≤ |x| + |y| \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example : |x + y| ≤ |x| + |y| := by sorry |
Demostrar con Lean4 que en \(ℝ\), \(-x ≤ |x|\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x : ℝ} example : -x ≤ |x| := by sorry |
Demostrar con Lean4 que en \(ℝ\), \(x ≤ |x|\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x : ℝ} example : x ≤ |x| := by sorry |
Demostrar con Lean4 que en \(ℝ\), si \(x < |y|\), entonces \(x < y\) ó \(x < -y\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example : x < |y| → x < y ∨ x < -y := by sorry |
Demostrar con Lean4 que en \(ℝ\),
\[ -y > x² + 1 ⊢ y > 0 ∨ y < -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 : -y > x^2 + 1) : y > 0 ∨ y < -1 := by sorry |
Demostrar con Lean4 que en \(ℝ\), \(y > x^2 ⊢ y > 0 ∨ y < -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 : y > x^2) : y > 0 ∨ y < -1 := by sorry |
Demostrar con Lean4 que si \(≤\) es un preorden, entonces \(<\) es transitiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable {α : Type _} [Preorder α] variable (a b c : α) example : a < b → b < c → a < c := by sorry |
Demostrar con Lean4 que si \(≤\) es un preorden, entonces \(<\) es irreflexiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable {α : Type _} [Preorder α] variable (a : α) example : ¬a < a := by sorry |
Demostrar con Lean4 que en los órdenes parciales,
\[a < b ↔ a ≤ b ∧ a ≠ b\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
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:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic import src.CNS_de_no_monotona example : ¬Monotone fun x : ℝ ↦ -x := by sorry |