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 con Lean4 que si \(f\) es creciente y \(g\) es decreciente, entonces \(g ∘ f\) es decreciente.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
import Mathlib.Data.Real.Basic variable (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) := by sorry |
1. Demostración en lenguaje natural
Sean \(x, y ∈ ℝ\) tales que \(x ≤ y\). Entonces, por ser \(f\) creciente,
\[ f(x) ≥ f(y) \]
y, por ser g decreciente,
\[ g(f(x)) ≤ g(f(y)) \]
Por tanto,
\[ (g ∘ f)(x) ≤ (g ∘ f)(y) \]
2. 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 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 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 |
import Mathlib.Data.Real.Basic variable (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) := by intro x y h -- x y : ℝ -- h : x ≤ y -- ⊢ (g ∘ f) x ≥ (g ∘ f) y have h1 : f x ≤ f y := hf h show (g ∘ f) x ≥ (g ∘ f) y exact hg h1 -- 2ª demostración -- =============== example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := by intro x y h -- x y : ℝ -- h : x ≤ y -- ⊢ (g ∘ f) x ≥ (g ∘ f) y show (g ∘ f) x ≥ (g ∘ f) y exact hg (hf h) -- 3ª demostración -- =============== example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := fun {_ _} h ↦ hg (hf h) -- 4ª demostración -- =============== example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := by intros x y hxy calc (g ∘ f) x = g (f x) := rfl _ ≥ g (f y) := hg (hf hxy) _ = (g ∘ f) y := rfl -- 5ª demostración -- =============== example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := by unfold creciente decreciente at * -- hf : ∀ {x y : ℝ}, x ≤ y → f x ≤ f y -- hg : ∀ {x y : ℝ}, x ≤ y → g x ≥ g y -- ⊢ ∀ {x y : ℝ}, x ≤ y → (g ∘ f) x ≥ (g ∘ f) y intros x y h -- x y : ℝ -- h : x ≤ y -- ⊢ (g ∘ f) x ≥ (g ∘ f) y unfold Function.comp -- ⊢ g (f x) ≥ g (f y) apply hg -- ⊢ f x ≤ f y apply hf -- ⊢ x ≤ y exact h -- 6ª demostración -- =============== example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := by intros x y h -- x y : ℝ -- h : x ≤ y -- ⊢ (g ∘ f) x ≥ (g ∘ f) y apply hg -- ⊢ f x ≤ f y apply hf -- ⊢ x ≤ y exact h -- 7ª demostración -- =============== example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := by intros x y h -- x y : ℝ -- h : x ≤ y -- ⊢ (g ∘ f) x ≥ (g ∘ f) y apply hg -- ⊢ f x ≤ f y exact hf h -- 8ª demostración -- =============== example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := by intros x y h -- x y : ℝ -- h : x ≤ y -- ⊢ (g ∘ f) x ≥ (g ∘ f) y exact hg (hf h) -- 9ª demostración -- =============== example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := by tauto |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones 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 48 49 50 51 |
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 (metis antimonoE monoD) 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)" using assms(1) assms(2) monotone_on_o by blast end |
