En ℝ, x ≤ |x|
Demostrar con Lean4 que en \(ℝ\), \(x ≤ |x|\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {x : ℝ} example : x ≤ |x| := by sorry
Publicaciones sobre Análisis (publicaciones antiguas, página 4)
Subcategorías:En ℝ, si x < |y|, entonces x < y ó x < -y
Demostrar con Lean4 que en \(ℝ\), si \(x < |y|\), entonces \(x < y\) ó \(x < -y\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable {x y : ℝ} example : x < |y| → x < y ∨ x < -y := by sorry
En ℝ, si -y > x² + 1 entonces y > 0 ó y < -1
Demostrar con Lean4 que en \(ℝ\), \[ -y > x² + 1 ⊢ y > 0 ∨ y < -1 \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {x y : ℝ} example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by sorry
En ℝ, si y > x² entonces y > 0 ó y < -1
Demostrar con Lean4 que en \(ℝ\), \(y > x^2 ⊢ y > 0 ∨ y < -1\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {x y : ℝ} example (h : y > x^2) : y > 0 ∨ y < -1 := by sorry
La función x ↦ -x no es monótona creciente
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
La función real f no es monótona syss existen x, y tales que x ≤ y y f(x) > f(y)
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
Si |x + 3| < 5, entonces -8 < x < 2
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
En ℝ, x² + y² = 0 ↔ x = 0 ∧ y = 0
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
En ℝ, si x ≤ y, entonces y ≰ x ↔ x ≠ y
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
En ℝ, x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x
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