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
Si f no es monótona, entonces ∃x∃y[x ≤ y ∧ f(y) < f(x)]
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:
import Mathlib.Tactic variable (f : ℝ → ℝ) example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by sorry
Si ¬(∀a)(∃x)[f(x) > a], entonces f está acotada superiormente
Demostrar con Lean4 que si \(¬(∀a)(∃x)[f(x) > a]\), entonces \(f\) está acotada superiormente.
Para ello, completar la siguiente teoría de Lean4:
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
Si f no está acotada superiormente, entonces (∀a)(∃x)[f(x) > a]
Demostrar con Lean4 que si \(f\) no está acotada superiormente, entonces \((∀a)(∃x)[f(x) > a]\).
Para ello, completar la siguiente teoría de Lean4:
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 : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by sorry
Introducción de la doble negación
Demostrar con Lean4 que \(P → ¬¬P\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable (P : Prop) example (h : P) : ¬¬P := by sorry
Eliminación de la doble negación
Demostrar con Lean4 que \(¬¬P → P\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable (P : Prop) example (h : ¬¬P) : P := by sorry
Si (∃x)¬P(x), entonces ¬(∀x)P(x)
Demostrar con Lean4 que si \((∃x)¬P(x)\), entonces \(¬(∀x)P(x)\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x := by sorry
Si ¬(∀x)P(x), entonces (∃x)¬P(x)
Demostrar con Lean4 que si \(¬(∀x)P(x)\), entonces \((∃x)¬P(x)\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := by sorry