La semana en Calculemus (6 de enero de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. f: ℝ → ℝ no es monótona syss (∃x,y)(x ≤ y ∧ f(x) > f(y))
- 2. La función x ↦ -x no es monótona creciente
- 3. En los órdenes parciales, a < b ↔ a ≤ b ∧ a ≠ b
- 4. Si ≤ es un preorden, entonces < es irreflexiva
- 5. Si ≤ es un preorden, entonces < es transitiva
A continuación se muestran las soluciones.
1. f: ℝ → ℝ no es monótona syss (∃x,y)[x ≤ y ∧ f(x) > f(y)]
Demostrar con Lean4 que \(f: ℝ → ℝ\) no es monótona syss \((∃x,y)[x ≤ y ∧ f(x) > f(y)]\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable {f : ℝ → ℝ} example : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := sorry |
Demostración en lenguaje natural
Por la siguiente cadena de equivalencias:
\begin{align}
f \text{ es no monótona } & ↔ ¬(∀ x, y)[x ≤ y → f(x) ≤ f(y)] \\
& ↔ (∃ x, y)[x ≤ y ∧ f(x) > f(y)]
\end{align}
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 |
import Mathlib.Data.Real.Basic variable {f : ℝ → ℝ} -- 1ª demostración -- =============== example : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := calc ¬Monotone f ↔ ¬∀ x y, x ≤ y → f x ≤ f y := by rw [Monotone] _ ↔ ∃ x y, x ≤ y ∧ f y < f x := by simp_all only [not_forall, not_le, exists_prop] _ ↔ ∃ x y, x ≤ y ∧ f x > f y := by rfl -- 2ª demostración -- =============== example : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := calc ¬Monotone f ↔ ¬∀ x y, x ≤ y → f x ≤ f y := by rw [Monotone] _ ↔ ∃ x y, x ≤ y ∧ f x > f y := by aesop -- 3ª demostración -- =============== example : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by rw [Monotone] -- ⊢ (¬∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b) ↔ ∃ x y, x ≤ y ∧ f x > f y push_neg -- ⊢ (Exists fun ⦃a⦄ => Exists fun ⦃b⦄ => a ≤ b ∧ f b < f a) ↔ ∃ x y, x ≤ y ∧ f x > f y rfl -- 4ª demostración -- =============== lemma not_Monotone_iff : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by rw [Monotone] -- ⊢ (¬∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b) ↔ ∃ x y, x ≤ y ∧ f x > f y aesop |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 37.
2. La función x ↦ -x no es monótona creciente
Demostrar con Lean4 que la función \(x ↦ -x\) no es monótona creciente.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic import src.CNS_de_no_monotona example : ¬Monotone fun x : ℝ ↦ -x := by sorry |
Demostración en lenguaje natural
Usando el lema del ejercicio anterior que afirma que una función f no es monótona syss existen x e y tales que x ≤ y y f(x) > f(y), basta demostrar que
\[ (∃ x, y)[x ≤ y ∧ -x > -y] \]
Basta elegir 2 y 3 ya que
\[ 2 ≤ 3 ∧ -2 > -3 \]
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Data.Real.Basic import src.CNS_de_no_monotona example : ¬Monotone fun x : ℝ ↦ -x := by apply not_Monotone_iff.mpr -- ⊢ ∃ x y, x ≤ y ∧ -x > -y use 2, 3 -- ⊢ 2 ≤ 3 ∧ -2 > -3 norm_num |
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 37.
3. En los órdenes parciales, a < b ↔ a ≤ b ∧ a ≠ b
Demostrar con Lean4 que en los órdenes parciales,
\[a < b ↔ a ≤ b ∧ a ≠ b\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable {α : Type _} [PartialOrder α] variable (a b : α) example : a < b ↔ a ≤ b ∧ a ≠ b := by sorry |
Demostración en lenguaje natural
Usaremos los siguientes lemas
\begin{align}
&(∀ a, b)[a < b ↔ a ≤ b ∧ b ≰ a] \tag{L1} \\
&(∀ a, b)[a ≤ b → b ≤ a → a = b] \tag{L2}
\end{align}
Por el lema L1, lo que tenemos que demostrar es
\[ a ≤ b ∧ b ≰ a ↔ a ≤ b ∧ a ≠ b \]
Lo haremos demostrando las dos implicaciones.
(⇒) Supongamos que \(a ≤ b\) y \(b ≰ a\). Tenemos que demostrar que \(a ≠ b\). Lo haremos por reducción al absurdo. Para ello, supongamos que \(a = b\). Entonces, \(b ≤ a\) que es una contradicicción con \(b ≰ a\).
(⇐) Supongamos que \(a ≤ b\) y \(a ≠ b\). Tenemos que demostrar que \(b ≰ a\). Lo haremos por reducción al absurdo. Para ello, supongamos que \(b ≤ a\). Entonces, junto con \(a ≤ b\), se tiene que \(a = b\) que es una contradicicción con \(a ≠ b\).
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 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 |
import Mathlib.Tactic variable {α : Type _} [PartialOrder α] variable (a b : α) -- 1ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b ∧ ¬b ≤ a → a ≤ b ∧ a ≠ b rintro ⟨h1 : a ≤ b, h2 : ¬b ≤ a⟩ -- ⊢ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b exact h1 . -- ⊢ a ≠ b rintro (h3 : a = b) -- ⊢ False have h4: b = a := h3.symm have h5: b ≤ a := le_of_eq h4 show False exact h2 h5 . -- ⊢ a ≤ b ∧ a ≠ b → a ≤ b ∧ ¬b ≤ a rintro ⟨h5 : a ≤ b , h6 : a ≠ b⟩ -- ⊢ a ≤ b ∧ ¬b ≤ a constructor . -- ⊢ a ≤ b exact h5 . -- ⊢ ¬b ≤ a rintro (h7 : b ≤ a) have h8 : a = b := le_antisymm h5 h7 show False exact h6 h8 -- 2ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b ∧ ¬b ≤ a → a ≤ b ∧ a ≠ b rintro ⟨h1 : a ≤ b, h2 : ¬b ≤ a⟩ -- ⊢ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b exact h1 . -- ⊢ a ≠ b rintro (h3 : a = b) -- ⊢ False exact h2 (le_of_eq h3.symm) . -- ⊢ a ≤ b ∧ a ≠ b → a ≤ b ∧ ¬b ≤ a rintro ⟨h4 : a ≤ b , h5 : a ≠ b⟩ -- ⊢ a ≤ b ∧ ¬b ≤ a constructor . -- ⊢ a ≤ b exact h4 . -- ⊢ ¬b ≤ a rintro (h6 : b ≤ a) exact h5 (le_antisymm h4 h6) -- 3ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b ∧ ¬b ≤ a → a ≤ b ∧ a ≠ b rintro ⟨h1 : a ≤ b, h2 : ¬b ≤ a⟩ -- ⊢ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b exact h1 . -- ⊢ a ≠ b exact fun h3 ↦ h2 (le_of_eq h3.symm) . -- ⊢ a ≤ b ∧ a ≠ b → a ≤ b ∧ ¬b ≤ a rintro ⟨h4 : a ≤ b , h5 : a ≠ b⟩ -- ⊢ a ≤ b ∧ ¬b ≤ a constructor . -- ⊢ a ≤ b exact h4 . -- ⊢ ¬b ≤ a exact fun h6 ↦ h5 (le_antisymm h4 h6) -- 4ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b ∧ ¬b ≤ a → a ≤ b ∧ a ≠ b rintro ⟨h1 : a ≤ b, h2 : ¬b ≤ a⟩ -- ⊢ a ≤ b ∧ a ≠ b exact ⟨h1, fun h3 ↦ h2 (le_of_eq h3.symm)⟩ . -- ⊢ a ≤ b ∧ a ≠ b → a ≤ b ∧ ¬b ≤ a rintro ⟨h4 : a ≤ b , h5 : a ≠ b⟩ -- ⊢ a ≤ b ∧ ¬b ≤ a exact ⟨h4, fun h6 ↦ h5 (le_antisymm h4 h6)⟩ -- 5ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b ∧ ¬b ≤ a → a ≤ b ∧ a ≠ b exact fun ⟨h1, h2⟩ ↦ ⟨h1, fun h3 ↦ h2 (le_of_eq h3.symm)⟩ . -- ⊢ a ≤ b ∧ a ≠ b → a ≤ b ∧ ¬b ≤ a exact fun ⟨h4, h5⟩ ↦ ⟨h4, fun h6 ↦ h5 (le_antisymm h4 h6)⟩ -- 6ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by rw [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ a ≠ b exact ⟨fun ⟨h1, h2⟩ ↦ ⟨h1, fun h3 ↦ h2 (le_of_eq h3.symm)⟩, fun ⟨h4, h5⟩ ↦ ⟨h4, fun h6 ↦ h5 (le_antisymm h4 h6)⟩⟩ -- 7ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := by constructor . -- ⊢ a < b → a ≤ b ∧ a ≠ b intro h -- h : a < b -- ⊢ a ≤ b ∧ a ≠ b constructor . -- ⊢ a ≤ b exact le_of_lt h . -- ⊢ a ≠ b exact ne_of_lt h . -- ⊢ a ≤ b ∧ a ≠ b → a < b rintro ⟨h1, h2⟩ -- h1 : a ≤ b -- h2 : a ≠ b -- ⊢ a < b exact lt_of_le_of_ne h1 h2 -- 8ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := ⟨fun h ↦ ⟨le_of_lt h, ne_of_lt h⟩, fun ⟨h1, h2⟩ ↦ lt_of_le_of_ne h1 h2⟩ -- 9ª demostración -- =============== example : a < b ↔ a ≤ b ∧ a ≠ b := lt_iff_le_and_ne -- Lemas usados -- ============ -- #check (le_antisymm : a ≤ b → b ≤ a → a = b) -- #check (le_of_eq : a = b → a ≤ b) -- #check (lt_iff_le_and_ne : a < b ↔ a ≤ b ∧ a ≠ b) -- #check (lt_iff_le_not_le : a < b ↔ a ≤ b ∧ ¬b ≤ a) -- #check (lt_of_le_of_ne : a ≤ b → a ≠ b → a < b) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 37.
4. Si ≤ es un preorden, entonces < es irreflexiva
Demostrar con Lean4 que si \(≤\) es un preorden, entonces \(<\) es irreflexiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable {α : Type _} [Preorder α] variable (a : α) example : ¬a < a := by sorry |
Demostración en lenguaje natural
Se usará la siguiente propiedad de lo preórdenes
\[ (∀ a, b)[a < b ↔ a ≤ b ∧ b ≰ a] \]
Con dicha propiedad, lo que tenemos que demostrar se transforma en
\[ ¬(a ≤ a ∧ a ≰ a) \]
Para demostrarla, supongamos que
\[ a ≤ a ∧ a ≰ a \]
lo que es una contradicción.
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 |
import Mathlib.Tactic variable {α : Type _} [Preorder α] variable (a : α) -- 1ª demostración -- =============== example : ¬a < a := by rw [lt_iff_le_not_le] -- ⊢ ¬(a ≤ a ∧ ¬a ≤ a) rintro ⟨h1, h2⟩ -- h1 : a ≤ a -- h2 : ¬a ≤ a -- ⊢ False exact h2 h1 -- 2ª demostración -- =============== example : ¬a < a := irrefl a -- Lemas usados -- ============ -- variable (b : α) -- #check (lt_iff_le_not_le : a < b ↔ a ≤ b ∧ ¬b ≤ a) -- #check (irrefl a : ¬a < a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 38.
5. Si ≤ es un preorden, entonces < es transitiva
Demostrar con Lean4 que si \(≤\) es un preorden, entonces \(<\) es transitiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable {α : Type _} [Preorder α] variable (a b c : α) example : a < b → b < c → a < c := by sorry |
Demostración en lenguaje natural
Se usará la siguiente propiedad de los preórdenes
\[ (∀ a, b)[a < b ↔ a ≤ b ∧ b ≰ a] \]
Con dicha propiedad, lo que tenemos que demostrar se transforma en
\[ a ≤ b ∧ b ≰ a → b ≤ c ∧ c ≰ b → a ≤ c ∧ c ≰ a \]
Para demostrarla, supongamos que
\begin{align}
&a ≤ b \tag{(1)} \\
&b ≰ a \tag{(2)} \\
&b ≤ c \tag{(3)} \\
&c ≰ b \tag{(4)}
\end{align}
y tenemos que demostrar las siguientes relaciones
\begin{align}
&a ≤ c \tag{(5)} \\
&c ≰ a \tag{(6)}
\end{align}
La (5) se tiene aplicando la propiedad transitiva a (1) y (3).
Para demostrar la (6), supongamos que
\[ c ≤ a \tag{(7)} \]
entonces, junto a la (1), por la propieda transitiva se tiene
\[ c ≤ b \]
que es una contradicción con la (4).
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 |
import Mathlib.Tactic variable {α : Type _} [Preorder α] variable (a b c : α) -- 1ª demostración -- =============== example : a < b → b < c → a < c := by simp only [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a → b ≤ c ∧ ¬c ≤ b → a ≤ c ∧ ¬c ≤ a rintro ⟨h1 : a ≤ b, _h2 : ¬b ≤ a⟩ ⟨h3 : b ≤ c, h4 : ¬c ≤ b⟩ -- ⊢ a ≤ c ∧ ¬c ≤ a constructor . -- ⊢ a ≤ c exact le_trans h1 h3 . -- ⊢ ¬c ≤ a contrapose! h4 -- h4 : c ≤ a -- ⊢ c ≤ b exact le_trans h4 h1 -- 2ª demostración -- =============== example : a < b → b < c → a < c := by simp only [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a → b ≤ c ∧ ¬c ≤ b → a ≤ c ∧ ¬c ≤ a rintro ⟨h1 : a ≤ b, _h2 : ¬b ≤ a⟩ ⟨h3 : b ≤ c, h4 : ¬c ≤ b⟩ -- ⊢ a ≤ c ∧ ¬c ≤ a constructor . -- ⊢ a ≤ c exact le_trans h1 h3 . -- ⊢ ¬c ≤ a rintro (h5 : c ≤ a) -- ⊢ False have h6 : c ≤ b := le_trans h5 h1 show False exact h4 h6 -- 3ª demostración -- =============== example : a < b → b < c → a < c := by simp only [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a → b ≤ c ∧ ¬c ≤ b → a ≤ c ∧ ¬c ≤ a rintro ⟨h1 : a ≤ b, _h2 : ¬b ≤ a⟩ ⟨h3 : b ≤ c, h4 : ¬c ≤ b⟩ -- ⊢ a ≤ c ∧ ¬c ≤ a constructor . -- ⊢ a ≤ c exact le_trans h1 h3 . -- ⊢ ¬c ≤ a exact fun h5 ↦ h4 (le_trans h5 h1) -- 4ª demostración -- =============== example : a < b → b < c → a < c := by simp only [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a → b ≤ c ∧ ¬c ≤ b → a ≤ c ∧ ¬c ≤ a rintro ⟨h1 : a ≤ b, _h2 : ¬b ≤ a⟩ ⟨h3 : b ≤ c, h4 : ¬c ≤ b⟩ -- ⊢ a ≤ c ∧ ¬c ≤ a exact ⟨le_trans h1 h3, fun h5 ↦ h4 (le_trans h5 h1)⟩ -- 5ª demostración -- =============== example : a < b → b < c → a < c := by simp only [lt_iff_le_not_le] -- ⊢ a ≤ b ∧ ¬b ≤ a → b ≤ c ∧ ¬c ≤ b → a ≤ c ∧ ¬c ≤ a exact fun ⟨h1, _h2⟩ ⟨h3, h4⟩ ↦ ⟨le_trans h1 h3, fun h5 ↦ h4 (le_trans h5 h1)⟩ -- 6ª demostración -- =============== example : a < b → b < c → a < c := lt_trans -- Lemas usados -- ============ -- #check (lt_iff_le_not_le : a < b ↔ a ≤ b ∧ ¬b ≤ a) -- #check (le_trans : a ≤ b → b ≤ c → a ≤ c) -- #check (lt_trans : a < b → b < c → a < c) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 38.