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:
|
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)]"