Si a, b ∈ ℝ tales que a ≤ b y f(b) < f(a), entonces f no es monótona
Demostrar con Lean4 que si \(a, b ∈ ℝ\) tales que \(a ≤ b\) y \(f(b) < f(a)\), entonces \(f\) no es monótona
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable (a b : ℝ) example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := by sorry |
Demostración en lenguaje natural
Usaremos el lema
\[ a ≥ b → a ≮ b \tag{L1} \]
Lo demostraremos por reducción al absurdo. Para ello, supongamos que \(f\) es monótona. Entonces, como \(a ≤ b\), se tiene \(f(a) ≤ f(b)\) y, por el lema L1, \(f(b) ≮ f(a)\), en contradicción con la hipótesis.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 |
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable (a b : ℝ) -- 1ª demostración -- =============== example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := by intro h3 -- h3 : Monotone f -- ⊢ False have h4 : f a ≤ f b := h3 h1 have h5 : ¬(f b < f a) := not_lt_of_ge h4 exact h5 h2 -- 2ª demostración -- =============== example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := by intro h3 -- h3 : Monotone f -- ⊢ False have h5 : ¬(f b < f a) := not_lt_of_ge (h3 h1) exact h5 h2 -- 3ª demostración -- =============== example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := by intro h3 -- h3 : Monotone f -- ⊢ False exact (not_lt_of_ge (h3 h1)) h2 -- 4ª demostración -- =============== example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := fun h3 ↦ (not_lt_of_ge (h3 h1)) h2 -- Lemas usados -- ============ -- #check (not_lt_of_ge : a ≥ b → ¬a < b) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.
