La composición de crecientes es creciente
Se dice que una función f de ℝ en ℝ es creciente si para todo x e y tales que x ≤ y se tiene que f(x) ≤ f(y).
En Lean que f sea creciente se representa por monotone f
.
Demostrar que la composición de dos funciones crecientes es una función creciente.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 |
import data.real.basic variables (f g : ℝ → ℝ) example (hf : monotone f) (hg : monotone g) : monotone (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 |
import data.real.basic variables (f g : ℝ → ℝ) -- 1ª demostración example (hf : monotone f) (hg : monotone g) : monotone (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 : monotone f) (hg : monotone g) : monotone (g ∘ f) := begin unfold monotone at *, intros x y h, unfold function.comp, apply hg, apply hf, exact h, end -- 3ª demostración example (hf : monotone f) (hg : monotone g) : monotone (g ∘ f) := begin intros x y h, apply hg, apply hf, exact h, end -- 4ª demostración example (hf : monotone f) (hg : monotone g) : monotone (g ∘ f) := begin intros x xy h, apply hg, exact hf h, end -- 5ª demostración example (hf : monotone f) (hg : monotone g) : monotone (g ∘ f) := begin intros x y h, exact hg (hf h), end -- 6ª demostración example (hf : monotone f) (hg : monotone g) : monotone (g ∘ f) := λ x y h, hg (hf h) -- 7ª demostración example (hf : monotone f) (hg : monotone g) : monotone (g ∘ f) := begin intros x y h, specialize hf h, exact hg hf, end -- 8ª demostración example (hf : monotone f) (hg : monotone g) : monotone (g ∘ f) := assume x y, assume h1 : x ≤ y, have h2 : f x ≤ f y, from hf h1, show (g ∘ f) x ≤ (g ∘ f) y, from calc (g ∘ f) x = g (f x) : rfl ... ≤ g (f y) : hg h2 ... = (g ∘ f) y : by refl -- 9ª demostración example (hf : monotone f) (hg : monotone g) : monotone (g ∘ f) := -- by hint by tauto -- 10ª demostración example (hf : monotone f) (hg : monotone g) : monotone (g ∘ f) := -- by library_search monotone.comp hg hf |
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_crecientes_es_creciente imports Main HOL.Real begin (* 1ª demostración *) lemma fixes f g :: "real ⇒ real" assumes "mono f" "mono g" shows "mono (g ∘ f)" proof (rule monoI) fix x y :: real assume "x ≤ y" have "(g ∘ f) x = g (f x)" by (simp only: o_apply) also have "… ≤ g (f y)" using assms ‹x ≤ y› by (simp only: monoD) also have "… = (g ∘ f) y" 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" "mono g" shows "mono (g ∘ f)" proof (rule monoI) fix x y :: real assume "x ≤ y" have "(g ∘ f) x = g (f x)" by simp also have "… ≤ g (f y)" by (simp add: ‹x ≤ y› assms monoD) also have "… = (g ∘ f) y" by simp finally show "(g ∘ f) x ≤ (g ∘ f) y" . qed (* 3ª demostración *) lemma assumes "mono f" "mono g" shows "mono (g ∘ f)" by (metis assms comp_def mono_def) 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]