La semana en Calculemus (25 de mayo de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Los monoides booleanos son conmutativos
- 2. La composición de una función creciente y una decreciente es decreciente
- 3. Si una función es creciente e involutiva, entonces es la identidad
- 4. Si
f(x) ≤ f(y) → x ≤ y, entonces f es inyectiva - 5. Los supremos de las sucesiones crecientes son sus límites
A continuación se muestran las soluciones.
1. Los monoides booleanos son conmutativos
Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.
Un monoide \(M\) es booleano si
\[ (∀ x ∈ M)[x·x = 1] \]
y es conmutativo si
\[ (∀ x, y ∈ M)[x·y = y·x] \]
En Lean4, está definida la clase de los monoides (como Monoid) y sus propiedades características son
|
1 2 3 |
mul_assoc : (a * b) * c = a * (b * c) one_mul : 1 * a = a mul_one : a * 1 = a |
Demostrar con Lean4 que los monoides booleanos son conmutativos.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [Monoid M] example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := by sorry |
1.1. Demostración en lenguaje natural
Sean \(a, b ∈ M\). Se verifica la siguiente cadena de igualdades
\begin{align}
a·b &= (a·b)·1 &&\text{[por mul_one]} \\
&= (a·b)·(a·a) &&\text{[por hipótesis, \(a·a = 1\)]} \\
&= ((a·b)·a)·a &&\text{[por mul_assoc]} \\
&= (a·(b·a))·a &&\text{[por mul_assoc]} \\
&= (1·(a·(b·a)))·a &&\text{[por one_mul]} \\
&= ((b·b)·(a·(b·a)))·a &&\text{[por hipótesis, \(b·b = 1\)]} \\
&= (b·(b·(a·(b·a))))·a &&\text{[por mul_assoc]} \\
&= (b·((b·a)·(b·a)))·a &&\text{[por mul_assoc]} \\
&= (b·1)·a &&\text{[por hipótesis, \((b·a)·(b·a) = 1\)]} \\
&= b·a &&\text{[por mul_one]}
\end{align}
1.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 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [Monoid M] -- 1ª demostración -- =============== example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := by intros a b calc a * b = (a * b) * 1 := (mul_one (a * b)).symm _ = (a * b) * (a * a) := congrArg ((a*b) * .) (h a).symm _ = ((a * b) * a) * a := (mul_assoc (a*b) a a).symm _ = (a * (b * a)) * a := congrArg (. * a) (mul_assoc a b a) _ = (1 * (a * (b * a))) * a := congrArg (. * a) (one_mul (a*(b*a))).symm _ = ((b * b) * (a * (b * a))) * a := congrArg (. * a) (congrArg (. * (a*(b*a))) (h b).symm) _ = (b * (b * (a * (b * a)))) * a := congrArg (. * a) (mul_assoc b b (a*(b*a))) _ = (b * ((b * a) * (b * a))) * a := congrArg (. * a) (congrArg (b * .) (mul_assoc b a (b*a)).symm) _ = (b * 1) * a := congrArg (. * a) (congrArg (b * .) (h (b*a))) _ = b * a := congrArg (. * a) (mul_one b) -- 2ª demostración -- =============== example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := by intros a b calc a * b = (a * b) * 1 := by simp only [mul_one] _ = (a * b) * (a * a) := by simp only [h a] _ = ((a * b) * a) * a := by simp only [mul_assoc] _ = (a * (b * a)) * a := by simp only [mul_assoc] _ = (1 * (a * (b * a))) * a := by simp only [one_mul] _ = ((b * b) * (a * (b * a))) * a := by simp only [h b] _ = (b * (b * (a * (b * a)))) * a := by simp only [mul_assoc] _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc] _ = (b * 1) * a := by simp only [h (b*a)] _ = b * a := by simp only [mul_one] -- 3ª demostración -- =============== example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := by intros a b calc a * b = (a * b) * 1 := by simp only [mul_one] _ = (a * b) * (a * a) := by simp only [h a] _ = (a * (b * a)) * a := by simp only [mul_assoc] _ = (1 * (a * (b * a))) * a := by simp only [one_mul] _ = ((b * b) * (a * (b * a))) * a := by simp only [h b] _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc] _ = (b * 1) * a := by simp only [h (b*a)] _ = b * a := by simp only [mul_one] -- 4ª demostración -- =============== example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := by intros a b calc a * b = (a * b) * 1 := by simp _ = (a * b) * (a * a) := by simp only [h a] _ = (a * (b * a)) * a := by simp only [mul_assoc] _ = (1 * (a * (b * a))) * a := by simp _ = ((b * b) * (a * (b * a))) * a := by simp only [h b] _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc] _ = (b * 1) * a := by simp only [h (b*a)] _ = b * a := by simp -- Lemas usados -- ============ -- variable (a b c : M) -- #check (mul_assoc a b c : (a * b) * c = a * (b * c)) -- #check (mul_one a : a * 1 = a) -- #check (one_mul a : 1 * a = a) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
1.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 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 |
theory Los_monoides_booleanos_son_conmutativos imports Main begin context monoid begin (* 1ª demostración *) lemma assumes "∀ x. x * x = 1" shows "∀ x y. x * y = y * x" proof (rule allI)+ fix a b have "a * b = (a * b) * 1" by (simp only: right_neutral) also have "… = (a * b) * (a * a)" by (simp only: assms) also have "… = ((a * b) * a) * a" by (simp only: assoc) also have "… = (a * (b * a)) * a" by (simp only: assoc) also have "… = (1 * (a * (b * a))) * a" by (simp only: left_neutral) also have "… = ((b * b) * (a * (b * a))) * a" by (simp only: assms) also have "… = (b * (b * (a * (b * a)))) * a" by (simp only: assoc) also have "… = (b * ((b * a) * (b * a))) * a" by (simp only: assoc) also have "… = (b * 1) * a" by (simp only: assms) also have "… = b * a" by (simp only: right_neutral) finally show "a * b = b * a" by this qed (* 2ª demostración *) lemma assumes "∀ x. x * x = 1" shows "∀ x y. x * y = y * x" proof (rule allI)+ fix a b have "a * b = (a * b) * 1" by simp also have "… = (a * b) * (a * a)" by (simp add: assms) also have "… = ((a * b) * a) * a" by (simp add: assoc) also have "… = (a * (b * a)) * a" by (simp add: assoc) also have "… = (1 * (a * (b * a))) * a" by simp also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms) also have "… = (b * (b * (a * (b * a)))) * a" by (simp add: assoc) also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc) also have "… = (b * 1) * a" by (simp add: assms) also have "… = b * a" by simp finally show "a * b = b * a" by this qed (* 3ª demostración *) lemma assumes "∀ x. x * x = 1" shows "∀ x y. x * y = y * x" proof (rule allI)+ fix a b have "a * b = (a * b) * (a * a)" by (simp add: assms) also have "… = (a * (b * a)) * a" by (simp add: assoc) also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms) also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc) also have "… = (b * 1) * a" by (simp add: assms) finally show "a * b = b * a" by simp qed (* 4ª demostración *) lemma assumes "∀ x. x * x = 1" shows "∀ x y. x * y = y * x" by (metis assms assoc right_neutral) end end |
2. 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 |
2.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.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.
2.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 |
3. Si una función es creciente e involutiva, entonces es la identidad
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 involutiva si para todo \(x\) se tiene que \(f(f(x)) = x\).
En Lean4 que \(f\) sea creciente se representa por Monotone f y que sea involutiva por Involutive f
Demostrar con Lean4 que si \(f\) es creciente e involutiva, entonces \(f\) es la identidad.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Data.Real.Basic open Function variable (f : ℝ → ℝ) example (hc : Monotone f) (hi : Involutive f) : f = id := by sorry |
3.1. Demostración en lenguaje natural
Tenemos que demostrar que para todo \(x ∈ ℝ\), \(f(x) = x\). Sea \(x ∈ ℝ\). Entonces, por ser \(f\) involutiva, se tiene que
\[ f(f(x)) = x \tag{1} \]
Además, por las propiedades del orden, se tiene que \(f(x) ≤ x\) ó \(x ≤ f(x)\). Demostraremos que \(f(x) = x\) en los dos casos.
Caso 1: Supongamos que
\[ f(x) ≤ x \tag{2} \]
Entonces, por ser \(f\) creciente, se tiene que
\[ f(f(x)) ≤ f(x) \tag{3} \]
Sustituyendo (1) en (3), se tiene
\[ x ≤ f(x) \]
que junto con (1) da
\[ f(x) = x \]
Caso 2: Supongamos que
\[ x ≤ f(x) \tag{4} \]
Entonces, por ser \(f\) creciente, se tiene que
\[ f(x) ≤ f(f(x)) \tag{5} \]
Sustituyendo (1) en (5), se tiene
\[ f(x) ≤ x \]
que junto con (4) da
\[ f(x) = x \]
3.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 |
import Mathlib.Data.Real.Basic open Function variable (f : ℝ → ℝ) -- 1ª demostración example (hc : Monotone f) (hi : Involutive f) : f = id := by funext x -- x : ℝ -- ⊢ f x = id x have h : f (f x) = x := hi x cases' (le_total (f x) x) with h1 h2 . -- h1 : f x ≤ x have h1a : f (f x) ≤ f x := hc h1 have h1b : x ≤ f x := by rwa [h] at h1a show f x = x exact antisymm h1 h1b . -- h2 : x ≤ f x have h2a : f x ≤ f (f x) := hc h2 have h2b : f x ≤ x := by rwa [h] at h2a show f x = x exact antisymm h2b h2 -- 2ª demostración example (hc : Monotone f) (hi : Involutive f) : f = id := by unfold Monotone Involutive at * -- hc : ∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b -- hi : ∀ (x : ℝ), f (f x) = x funext x -- x : ℝ -- ⊢ f x = id x unfold id -- ⊢ f x = x cases' (le_total (f x) x) with h1 h2 . -- h1 : f x ≤ x apply antisymm h1 -- ⊢ x ≤ f x have h3 : f (f x) ≤ f x := by apply hc -- ⊢ f x ≤ x exact h1 rwa [hi] at h3 . -- h2 : x ≤ f x apply antisymm _ h2 -- ⊢ f x ≤ x have h4 : f x ≤ f (f x) := by apply hc -- ⊢ x ≤ f x exact h2 rwa [hi] at h4 -- 3ª demostración example (hc : Monotone f) (hi : Involutive f) : f = id := by funext x -- x : ℝ -- ⊢ f x = id x cases' (le_total (f x) x) with h1 h2 . -- h1 : f x ≤ x apply antisymm h1 -- ⊢ x ≤ f x have h3 : f (f x) ≤ f x := hc h1 rwa [hi] at h3 . -- h2 : x ≤ f x apply antisymm _ h2 -- ⊢ f x ≤ x have h4 : f x ≤ f (f x) := hc h2 rwa [hi] at h4 -- 4ª demostración example (hc : Monotone f) (hi : Involutive f) : f = id := by funext x -- x : ℝ -- ⊢ f x = id x cases' (le_total (f x) x) with h1 h2 . -- h1 : f x ≤ x apply antisymm h1 -- ⊢ x ≤ f x calc x = f (f x) := (hi x).symm _ ≤ f x := hc h1 . -- h2 : x ≤ f x apply antisymm _ h2 -- ⊢ f x ≤ x calc f x ≤ f (f x) := hc h2 _ = x := hi x -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (le_total a b : a ≤ b ∨ b ≤ a) -- #check (antisymm : a ≤ b → b ≤ a → a = b) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3.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 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 |
theory Una_funcion_creciente_e_involutiva_es_la_identidad imports Main HOL.Real begin definition involutiva :: "(real ⇒ real) ⇒ bool" where "involutiva f ⟷ (∀x. f (f x) = x)" (* 1ª demostración *) lemma fixes f :: "real ⇒ real" assumes "mono f" "involutiva f" shows "f = id" proof (unfold fun_eq_iff; intro allI) fix x have "x ≤ f x ∨ f x ≤ x" by (rule linear) then have "f x = x" proof (rule disjE) assume "x ≤ f x" then have "f x ≤ f (f x)" using assms(1) by (simp only: monoD) also have "… = x" using assms(2) by (simp only: involutiva_def) finally have "f x ≤ x" by this show "f x = x" using ‹f x ≤ x› ‹x ≤ f x› by (simp only: antisym) next assume "f x ≤ x" have "x = f (f x)" using assms(2) by (simp only: involutiva_def) also have "... ≤ f x" using ‹f x ≤ x› assms(1) by (simp only: monoD) finally have "x ≤ f x" by this show "f x = x" using ‹f x ≤ x› ‹x ≤ f x› by (simp only: monoD) qed then show "f x = id x" by (simp only: id_apply) qed (* 2ª demostración *) lemma fixes f :: "real ⇒ real" assumes "mono f" "involutiva f" shows "f = id" proof fix x have "x ≤ f x ∨ f x ≤ x" by (rule linear) then have "f x = x" proof assume "x ≤ f x" then have "f x ≤ f (f x)" using assms(1) by (simp only: monoD) also have "… = x" using assms(2) by (simp only: involutiva_def) finally have "f x ≤ x" by this show "f x = x" using ‹f x ≤ x› ‹x ≤ f x› by auto next assume "f x ≤ x" have "x = f (f x)" using assms(2) by (simp only: involutiva_def) also have "... ≤ f x" by (simp add: ‹f x ≤ x› assms(1) monoD) finally have "x ≤ f x" by this show "f x = x" using ‹f x ≤ x› ‹x ≤ f x› by auto qed then show "f x = id x" by simp qed (* 3ª demostración *) lemma fixes f :: "real ⇒ real" assumes "mono f" "involutiva f" shows "f = id" proof fix x have "x ≤ f x ∨ f x ≤ x" by (rule linear) then have "f x = x" proof assume "x ≤ f x" then have "f x ≤ x" by (metis assms involutiva_def mono_def) then show "f x = x" using ‹x ≤ f x› by auto next assume "f x ≤ x" then have "x ≤ f x" by (metis assms involutiva_def mono_def) then show "f x = x" using ‹f x ≤ x› by auto qed then show "f x = id x" by simp qed end |
4. Si f(x) ≤ f(y) → x ≤ y, entonces f es inyectiva
Demostrar con Lean4 que si \(f\) una función de \(ℝ\) en \(ℝ\) tal que
\[ (∀ x, y)[f(x) ≤ f(y) → x ≤ y] \]
entonces \(f\) es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic open Function variable (f : ℝ → ℝ) example (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f := by sorry |
4.1. Demostración en lenguaje natural
Sean \(x, y ∈ ℝ\) tales que
\[ f(x) = f(y) \tag{1} \]
Tenemos que demostrar que \(x = y\).
De (1), tenemos que
\[ f(x) ≤ f(y) \]
y, por la hipótesis,
\[ x ≤ y \tag{2} \]
También de (1), tenemos que
\[ f(y) ≤ f(x) \]
y, por la hipótesis,
\[ y ≤ x \tag{3} \]
De (2) y (3), tenemos que
\[ x = y \]
4.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 |
import Mathlib.Data.Real.Basic open Function variable (f : ℝ → ℝ) -- 1ª demostración -- =============== example (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f := by intros x y hxy -- x y : ℝ -- hxy : f x = f y -- ⊢ x = y have h1 : f x ≤ f y := le_of_eq hxy have h2 : x ≤ y := h h1 have h3 : f y ≤ f x := ge_of_eq hxy have h4 : y ≤ x := h h3 show x = y exact le_antisymm h2 h4 -- 2ª demostración -- =============== example (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f := by intros x y hxy -- x y : ℝ -- hxy : f x = f y -- ⊢ x = y have h1 : x ≤ y := h (le_of_eq hxy) have h2 : y ≤ x := h (ge_of_eq hxy) show x = y exact le_antisymm h1 h2 -- 3ª demostración -- =============== example (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f := by intros x y hxy -- x y : ℝ -- hxy : f x = f y -- ⊢ x = y show x = y exact le_antisymm (h (le_of_eq hxy)) (h (ge_of_eq hxy)) -- 3ª demostración -- =============== example (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f := fun _ _ hxy ↦ le_antisymm (h hxy.le) (h hxy.ge) -- 4ª demostración -- =============== example (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f := by intros x y hxy -- x y : ℝ -- hxy : f x = f y -- ⊢ x = y apply le_antisymm . -- ⊢ x ≤ y apply h -- ⊢ f x ≤ f y exact le_of_eq hxy . -- ⊢ y ≤ x apply h -- ⊢ f y ≤ f x exact ge_of_eq hxy -- 5ª demostración -- =============== example (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f := by intros x y hxy -- x y : ℝ -- hxy : f x = f y -- ⊢ x = y apply le_antisymm . -- ⊢ x ≤ y exact h (le_of_eq hxy) . -- ⊢ y ≤ x exact h (ge_of_eq hxy) -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (ge_of_eq : a = b → a ≥ b) -- #check (le_antisymm : a ≤ b → b ≤ a → a = b) -- #check (le_of_eq : a = b → a ≤ b) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
4.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 |
theory "Si_f(x)_leq_f(y)_to_x_leq_y,_entonces_f_es_inyectiva" imports Main HOL.Real begin (* 1ª demostración *) lemma fixes f :: "real ⇒ real" assumes "∀ x y. f x ≤ f y ⟶ x ≤ y" shows "inj f" proof (rule injI) fix x y assume "f x = f y" show "x = y" proof (rule antisym) show "x ≤ y" by (simp only: assms ‹f x = f y›) next show "y ≤ x" by (simp only: assms ‹f x = f y›) qed qed (* 2ª demostración *) lemma fixes f :: "real ⇒ real" assumes "∀ x y. f x ≤ f y ⟶ x ≤ y" shows "inj f" proof (rule injI) fix x y assume "f x = f y" then show "x = y" using assms by (simp add: eq_iff) qed (* 3ª demostración *) lemma fixes f :: "real ⇒ real" assumes "∀ x y. f x ≤ f y ⟶ x ≤ y" shows "inj f" by (simp add: assms injI eq_iff) end |
5. Los supremos de las sucesiones crecientes son sus límites
Sea \(u\) una sucesión creciente. Demostrar con Lean4 que si \(S\) es un supremo de \(u\), entonces el límite de \(u\) es \(S\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 |
import Mathlib.Data.Real.Basic variable (u : ℕ → ℝ) variable (S : ℝ) -- (limite u c) expresa que el límite de u es c. def limite (u : ℕ → ℝ) (c : ℝ) := ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - c| ≤ ε -- (supremo u S) expresa que el supremo de u es S. def supremo (u : ℕ → ℝ) (S : ℝ) := (∀ n, u n ≤ S) ∧ ∀ ε > 0, ∃ k, u k ≥ S - ε example (hu : Monotone u) (hS : supremo u S) : limite u S := by sorry |
5.1. Demostración en lenguaje natural
Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Tenemos que demostrar que
\[ (∃ m ∈ ℕ)(∀ n ∈ ℕ)[n ≥ m → |u_n – S| ≤ ε] \tag{1} \]
Por ser \(S\) un supremo de u, existe un k ∈ ℕ tal que
\[ u_k ≥ S – ε \tag{2} \]
Vamos a demostrar que \(k\) verifica la condición de (1); es decir, que si \(n ∈ ℕ\) tal que \(n ≥ k\), entonces
\[ |u_n – S| ≤ ε \]
o, equivalentemente,
\[ -ε ≤ u_n – S ≤ ε \]
La primera desigualdad se tiene por la siguente cadena:
\begin{align}
-ε &= (S – ε) – S \\
&≤ u_k – S &&\text{[por (2)]} \\
&≤ u_n – S &&\text{[porque \(u\) es creciente y \(n ≥ k\)]}
\end{align}
La segunda desigualdad se tiene por la siguente cadena:
\begin{align}
u_n – S &≤ S – S &&\text{[porque \(S\) es un supremo de \(u\)]} \\
&= 0 \\
&≤ ε
\end{align}
5.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 |
import Mathlib.Data.Real.Basic variable (u : ℕ → ℝ) variable (S : ℝ) -- (limite u c) expresa que el límite de u es c. def limite (u : ℕ → ℝ) (c : ℝ) := ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - c| ≤ ε -- (supremo u S) expresa que el supremo de u es S. def supremo (u : ℕ → ℝ) (S : ℝ) := (∀ n, u n ≤ S) ∧ ∀ ε > 0, ∃ k, u k ≥ S - ε -- 1ª demostración -- =============== example (hu : Monotone u) (hS : supremo u S) : limite u S := by unfold limite -- ⊢ ∀ (ε : ℝ), ε > 0 → ∃ m, ∀ (n : ℕ), n ≥ m → |u n - S| ≤ ε intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ m, ∀ (n : ℕ), n ≥ m → |u n - S| ≤ ε unfold supremo at hS -- hS : (∀ (n : ℕ), u n ≤ S) ∧ ∀ (ε : ℝ), ε > 0 → ∃ k, u k ≥ S - ε cases' hS with hS₁ hS₂ -- hS₁ : ∀ (n : ℕ), u n ≤ S -- hS₂ : ∀ (ε : ℝ), ε > 0 → ∃ k, u k ≥ S - ε cases' hS₂ ε hε with k hk -- k : ℕ -- hk : u k ≥ S - ε use k -- ⊢ ∀ (n : ℕ), n ≥ k → |u n - S| ≤ ε intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |u n - S| ≤ ε rw [abs_le] -- ⊢ -ε ≤ u n - S ∧ u n - S ≤ ε constructor . -- ⊢ -ε ≤ u n - S unfold Monotone at hu -- hu : ∀ ⦃a b : ℕ⦄, a ≤ b → u a ≤ u b specialize hu hn -- hu : u k ≤ u n calc -ε = (S - ε) - S := by ring _ ≤ u k - S := sub_le_sub_right hk S _ ≤ u n - S := sub_le_sub_right hu S . calc u n - S ≤ S - S := sub_le_sub_right (hS₁ n) S _ = 0 := sub_self S _ ≤ ε := le_of_lt hε -- 2ª demostración -- =============== example (hu : Monotone u) (hS : supremo u S) : limite u S := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ m, ∀ (n : ℕ), n ≥ m → |u n - S| ≤ ε cases' hS with hS₁ hS₂ -- hS₁ : ∀ (n : ℕ), u n ≤ S -- hS₂ : ∀ (ε : ℝ), ε > 0 → ∃ k, u k ≥ S - ε cases' hS₂ ε hε with k hk -- k : ℕ -- hk : u k ≥ S - ε use k -- ⊢ ∀ (n : ℕ), n ≥ k → |u n - S| ≤ ε intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |u n - S| ≤ ε rw [abs_le] -- ⊢ -ε ≤ u n - S ∧ u n - S ≤ ε constructor . -- ⊢ -ε ≤ u n - S linarith [hu hn] . -- ⊢ u n - S ≤ ε linarith [hS₁ n] -- 3ª demostración -- =============== example (hu : Monotone u) (hS : supremo u S) : limite u S := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ m, ∀ (n : ℕ), n ≥ m → |u n - S| ≤ ε cases' hS with hS₁ hS₂ -- hS₁ : ∀ (n : ℕ), u n ≤ S -- hS₂ : ∀ (ε : ℝ), ε > 0 → ∃ k, u k ≥ S - ε cases' hS₂ ε hε with k hk -- k : ℕ -- hk : u k ≥ S - ε use k -- ⊢ ∀ (n : ℕ), n ≥ k → |u n - S| ≤ ε intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |u n - S| ≤ ε rw [abs_le] -- ⊢ -ε ≤ u n - S ∧ u n - S ≤ ε constructor <;> linarith [hu hn, hS₁ n] -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (abs_le : |a| ≤ b ↔ -b ≤ a ∧ a ≤ b) -- #check (le_of_lt : a < b → a ≤ b) -- #check (sub_le_sub_right : a ≤ b → ∀ (c : ℝ), a - c ≤ b - c) -- #check (sub_self a : a - a = 0) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
5.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 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 |
theory Los_supremos_de_las_sucesiones_crecientes_son_sus_limites imports Main HOL.Real begin (* (limite u c) expresa que el límite de u es c. *) definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)" (* (supremo u M) expresa que el supremo de u es M. *) definition supremo :: "(nat ⇒ real) ⇒ real ⇒ bool" where "supremo u M ⟷ ((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))" (* 1ª demostración *) lemma assumes "mono u" "supremo u M" shows "limite u M" proof (unfold limite_def; intro allI impI) fix ε :: real assume "0 < ε" have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))" using assms(2) by (simp add: supremo_def) then have "∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε" by (rule conjunct2) then have "∃k. ∀n≥k. u n ≥ M - ε" by (simp only: ‹0 < ε›) then obtain n0 where "∀n≥n0. u n ≥ M - ε" by (rule exE) have "∀n≥n0. ¦u n - M¦ ≤ ε" proof (intro allI impI) fix n assume "n ≥ n0" show "¦u n - M¦ ≤ ε" proof (rule abs_leI) have "∀n. u n ≤ M" using hM by (rule conjunct1) then have "u n - M ≤ M - M" by simp also have "… = 0" by (simp only: diff_self) also have "… ≤ ε" using ‹0 < ε› by (simp only: less_imp_le) finally show "u n - M ≤ ε" by this next have "-ε = (M - ε) - M" by simp also have "… ≤ u n - M" using ‹∀n≥n0. M - ε ≤ u n› ‹n0 ≤ n› by auto finally have "-ε ≤ u n - M" by this then show "- (u n - M) ≤ ε" by simp qed qed then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε" by (rule exI) qed (* 2ª demostración *) lemma assumes "mono u" "supremo u M" shows "limite u M" proof (unfold limite_def; intro allI impI) fix ε :: real assume "0 < ε" have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))" using assms(2) by (simp add: supremo_def) then have "∃k. ∀n≥k. u n ≥ M - ε" using ‹0 < ε› by presburger then obtain n0 where "∀n≥n0. u n ≥ M - ε" by (rule exE) then have "∀n≥n0. ¦u n - M¦ ≤ ε" using hM by auto then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε" by (rule exI) qed end |