La composición de una función creciente y una decreciente es decreciente
Sea una función f de ℝ en ℝ. Se dice que f es creciente si para todo x e y tales que x ≤ y se tiene que f(x) ≤ f(y). Se dice que f es decreciente si para todo x e y tales que x ≤ y se tiene que f(x) ≥ f(y).
Demostrar que si f es creciente y g es decreciente, entonces (g ∘ f) es decreciente.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
import data.real.basic variables (f g : ℝ → ℝ) def creciente (f : ℝ → ℝ) : Prop := ∀ {x y}, x ≤ y → f x ≤ f y def decreciente (f : ℝ → ℝ) : Prop := ∀ {x y}, x ≤ y → f x ≥ f y example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := sorry |
[expand title=»Soluciones con Lean»]
|
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 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 |
import data.real.basic variables (f g : ℝ → ℝ) def creciente (f : ℝ → ℝ) : Prop := ∀ {x y}, x ≤ y → f x ≤ f y def decreciente (f : ℝ → ℝ) : Prop := ∀ {x y}, x ≤ y → f x ≥ f y -- 1ª demostración example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := begin intros x y hxy, calc (g ∘ f) x = g (f x) : rfl ... ≥ g (f y) : hg (hf hxy) ... = (g ∘ f) y : rfl, end -- 2ª demostración example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := begin unfold creciente decreciente at *, intros x y h, unfold function.comp, apply hg, apply hf, exact h, end -- 3ª demostración example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := begin intros x y h, apply hg, apply hf, exact h, end -- 4ª demostración example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := begin intros x y h, apply hg, exact hf h, end -- 5ª demostración example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := begin intros x y h, exact hg (hf h), end -- 6ª demostración example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := λ x y h, hg (hf h) -- 7ª demostración example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := assume x y, assume h : x ≤ y, have h1 : f x ≤ f y, from hf h, show (g ∘ f) x ≥ (g ∘ f) y, from hg h1 -- 8ª demostración example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := assume x y, assume h : x ≤ y, show (g ∘ f) x ≥ (g ∘ f) y, from hg (hf h) -- 9ª demostración example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := λ x y h, hg (hf h) -- 10ª demostración example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := -- by hint by tauto |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones con Isabelle/HOL»]
|
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 |
theory La_composicion_de_una_funcion_creciente_y_una_decreciente_es_decreciente imports Main HOL.Real begin (* 1ª demostración *) lemma fixes f g :: "real ⇒ real" assumes "mono f" "antimono g" shows "antimono (g ∘ f)" proof (rule antimonoI) fix x y :: real assume "x ≤ y" have "(g ∘ f) y = g (f y)" by (simp only: o_apply) also have "… ≤ g (f x)" using assms ‹x ≤ y› by (meson antimonoE monoE) also have "… = (g ∘ f) x" by (simp only: o_apply) finally show "(g ∘ f) x ≥ (g ∘ f) y" by this qed (* 2ª demostración *) lemma fixes f g :: "real ⇒ real" assumes "mono f" "antimono g" shows "antimono (g ∘ f)" proof (rule antimonoI) fix x y :: real assume "x ≤ y" have "(g ∘ f) y = g (f y)" by simp also have "… ≤ g (f x)" by (meson ‹x ≤ y› assms antimonoE monoE) also have "… = (g ∘ f) x" by simp finally show "(g ∘ f) x ≥ (g ∘ f) y" . qed (* 3ª demostración *) lemma assumes "mono f" "antimono g" shows "antimono (g ∘ f)" by (metis assms mono_def antimono_def comp_apply) end |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]
