Existe un número real entre 2 y 3
Demostrar con Lean4 que \((∃x ∈ ℝ)[2 < x < 3]\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic example : ∃ x : ℝ, 2 < x ∧ x < 3 := by sorry
Publicaciones sobre Números reales (publicaciones antiguas, página 2)
Si x ≤ y y x ≠ y, entonces y ≰ x
Demostrar con Lean4 que \[x ≤ y ∧ x ≠ y ⊢ y ≰ x\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by sorry
Si x ≤ y y y ≰ x, entonces x ≤ y ∧ x ≠ y
Demostrar con Lean4 que \[\{x ≤ y, y ≰ x\} ⊢ 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 (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by sorry
Si 0 < 0, entonces a > 37 para cualquier número a
Demostrar con Lean4 que si \(0 < 0\), entonces \(a > 37\) para cualquier número \(a\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable (a : ℕ) example (h : 0 < 0) : a > 37 := by sorry
En ℝ, a < b → ¬(b < a)
Demostrar con Lean4 que en \(ℝ\), \(a < b → ¬(b < a)\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (a b : ℝ) example (h : a < b) : ¬ b < a := by sorry
Hay algún número real entre 2 y 3
Demostrar con Lean4 que hay algún número real entre 2 y 3.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic example : ∃ x : ℝ, 2 < x ∧ x < 3 := by sorry
En ℝ, |a| - |b| ≤ |a - b|
Demostrar con Lean4 que si \(a\) y \(b\) números reales, entonces \[|a| - |b| \leq |a - b|\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : |a| - |b| ≤ |a - b| := by sorry
En ℝ, min(a,b)+c = min(a+c,b+c)
Demostrar con Lean4 que si \(a\), \(b\) y \(c\) números reales, entonces \[\min(a,b)+c = \min(a+c,b+c)\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a b c : ℝ} example : min a b + c = min (a + c) (b + c) := by sorry
En ℝ, min(min(a,b),c) = min(a,min(b,c))
Demostrar con Lean4 que \(a\), \(b\) y \(c\) números reales, entonces \(\min(\min(a, b), c) = \min(a, \min(b, c))\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable {a b c : ℝ} example : min (min a b) c = min a (min b c) := by sorry
En ℝ, max(a,b) = max(b,a)
Demostrar con Lean4 que si \(a\) y \(b\) son números reales, entonces \(\max(a, b) = \max(b, a)\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : max a b = max b a := by sorry