Demostrar con Lean4 que. en \(ℝ\), \(x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x\).
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 ∧ ¬ 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:
|
1 2 3 4 5 6 |
import Mathlib.Data.Nat.Prime import Mathlib.Tactic example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by sorry |
Read More «Existen números primos m y n tales que 4 < m < n < 10"
Demostrar con Lean4 que si \((∃z ∈ ℝ)[x < z < y]\), entonces \(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 : (∃ z : ℝ, x < z ∧ z < y) → x < y := by sorry |
Demostrar con Lean4 que \((∃x ∈ ℝ)[2 < x < 3]\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 |
import Mathlib.Data.Real.Basic example : ∃ x : ℝ, 2 < x ∧ x < 3 := by sorry |
Demostrar con Lean4 que si (m ∣ n ∧ m ≠ n), entonces (m ∣ n ∧ ¬(n ∣ m)).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Nat.GCD.Basic variable {m n : ℕ} example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by sorry |
Demostrar con Lean4 que
\[x ≤ y ∧ x ≠ y ⊢ y ≰ x\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by sorry |
Demostrar con Lean4 que
\[\{x ≤ y, y ≰ x\} ⊢ x ≤ y ∧ x ≠ y\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by sorry |
Demostrar con Lean4 que si \(0 < 0\), entonces \(a > 37\) para cualquier número \(a\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable (a : ℕ) example (h : 0 < 0) : a > 37 := by sorry |
Read More «Si 0 < 0, entonces a > 37 para cualquier número a»
Demostrar con Lean4 que si \(f\) no es monótona, entonces \(∃x∃y[x ≤ y ∧ f(y) < f(x)]\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable (f : ℝ → ℝ) example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by sorry |
Read More «Si f no es monótona, entonces ∃x∃y[x ≤ y ∧ f(y) < f(x)]"
Demostrar con Lean4 que si \(¬(∀a)(∃x)[f(x) > a]\), entonces \(f\) está acotada superiormente.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) example (h : ¬∀ a, ∃ x, f x > a) : acotadaSup f := by sorry |
Read More «Si ¬(∀a)(∃x)[f(x) > a], entonces f está acotada superiormente»