f: ℝ → ℝ no es monótona syss (∃x,y)[x ≤ 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:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable {f : ℝ → ℝ} example : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := sorry |
Read More «f: ℝ → ℝ no es monótona syss (∃x,y)[x ≤ y ∧ f(x) > f(y)]»