Demostrar con Lean4 que si f es monótona y f(a)<f(b), entonces a<b.
Para ello, completar la siguiente teoría de Lean4:
|
|
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable (a b : ℝ) example (h1 : Monotone f) (h2 : f a < f b) : a < b := by sorry |
Demostración en lenguaje natural
Usaremos los lemas
a≱b→a<ba≥b→a≮b
Por el lema L1, basta demostrar que a≱b. Lo haremos reducción al absurdo. Para ello, supongamos que a≥b. Como f es monótona, se tiene f(a)≥f(b) y, aplicando el lema L2, f(a)≮f(b), que contradice a 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 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 |
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable (a b : ℝ) -- 1ª demostración -- =============== example (h1 : Monotone f) (h2 : f a < f b) : a < b := by apply lt_of_not_ge -- ⊢ ¬a ≥ b intro h3 -- h3 : a ≥ b -- ⊢ False have h4 : f a ≥ f b := h1 h3 have h5 : ¬ f a < f b := not_lt_of_ge h4 exact h5 h2 -- 2ª demostración -- =============== example (h1 : Monotone f) (h2 : f a < f b) : a < b := by apply lt_of_not_ge -- ⊢ ¬a ≥ b intro h3 -- h3 : a ≥ b -- ⊢ False have h5 : ¬ f a < f b := not_lt_of_ge (h1 h3) exact h5 h2 -- 3ª demostración -- =============== example (h1 : Monotone f) (h2 : f a < f b) : a < b := by apply lt_of_not_ge -- ⊢ ¬a ≥ b intro h3 -- h3 : a ≥ b -- ⊢ False exact (not_lt_of_ge (h1 h3)) h2 -- 4ª demostración -- =============== example (h1 : Monotone f) (h2 : f a < f b) : a < b := by apply lt_of_not_ge -- ⊢ ¬a ≥ b exact fun h3 ↦ (not_lt_of_ge (h1 h3)) h2 -- 5ª demostración -- =============== example (h1 : Monotone f) (h2 : f a < f b) : a < b := lt_of_not_ge (fun h3 ↦ (not_lt_of_ge (h1 h3)) h2) -- Lemas usados -- ============ -- #check (lt_of_not_ge : ¬ a ≥ b → a < b) -- #check (not_lt_of_ge : a ≥ b → ¬ a < b) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
