La semana en Calculemus (30 de diciembre de 2023)
Estas 3 últimas semanas he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. {x ≤ y, y ≰ x} ⊢ x ≤ y ∧ x ≠ y
- 2. x ≤ y ∧ x ≠ y ⊢ y ≰ x
- 3. Si (m ∣ n ∧ m ≠ n), entonces (m ∣ n ∧ ¬(n ∣ m))
- 4. (∃x ∈ ℝ)(2 < x < 3)
- 5. Si (∃z ∈ ℝ)(x < z < y), entonces x < y
- 6. Existen números primos m y n tales que 4 < m < n < 10
- 7. En ℝ, x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x
- 8. En ℝ, si x ≤ y, entonces y ≰ x ↔ x ≠ y
- 9. En ℝ, x² + y² = 0 ↔ x = 0 ∧ y = 0
- 10. Si |x + 3| < 5, entonces -8 < x < 2
- 11. 3 divide al máximo común divisor de 6 y 15
A continuación se muestran las soluciones.
1. {x ≤ y, y ≰ x} ⊢ x ≤ y ∧ x ≠ y
Demostrar con Lean4 que
\[\{x ≤ y, y ≰ x\} ⊢ x ≤ y ∧ x ≠ y\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by sorry |
Demostración en lenguaje natural
Como la conclusión es una conjunción, tenemos que desmostrar sus partes. La primera parte (\(x ≤ y\)) coincide con la hipótesis. Para demostrar la segunda parte (\(x ≠ y\)), supongamos que \(x = y\); entonces \(y ≤ x\) en contradicción con la segunda hipótesis.
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 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by constructor . -- ⊢ x ≤ y exact h1 . -- ⊢ x ≠ y intro h3 -- h3 : x = y -- ⊢ False have h4 : y ≤ x := h3.symm.le show False exact h2 h4 -- 2ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by constructor . -- ⊢ x ≤ y exact h1 . -- ⊢ x ≠ y intro h3 -- h3 : x = y -- ⊢ False exact h2 (h3.symm.le) -- 3ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := ⟨h1, fun h3 ↦ h2 (h3.symm.le)⟩ -- 4ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by constructor . -- ⊢ x ≤ y exact h1 . -- ⊢ x ≠ y intro h3 -- h3 : x = y -- ⊢ False apply h2 -- ⊢ y ≤ x rw [h3] -- 5ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by constructor . -- ⊢ x ≤ y exact h1 . -- ⊢ x ≠ y intro h3 -- h3 : x = y -- ⊢ False exact h2 (by rw [h3]) -- 6ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬ y ≤ x) : x ≤ y ∧ x ≠ y := ⟨h1, fun h ↦ h2 (by rw [h])⟩ -- 7ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬ y ≤ x) : x ≤ y ∧ x ≠ y := by have h3 : x ≠ y . contrapose! h2 -- ⊢ y ≤ x rw [h2] exact ⟨h1, h3⟩ -- 8ª demostración -- =============== example (h1 : x ≤ y) (h2 : ¬ y ≤ x) : x ≤ y ∧ x ≠ y := by aesop |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 35.
2. x ≤ y ∧ x ≠ y ⊢ y ≰ x
Demostrar con Lean4 que
\[x ≤ y ∧ x ≠ y ⊢ y ≰ x\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by sorry |
Demostración en lenguaje natural
Supongamos que \(y ≤ x\). Entonces, por la antisimetría y la primera parte de la hipótesis, se tiene que \(x = y\) que contradice la segunda parte de la hipótesis.
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 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by intro h1 cases' h with h2 h3 -- h2 : x ≤ y -- h3 : x ≠ y have h4 : x = y := le_antisymm h2 h1 show False exact h3 h4 -- 2ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by intro h1 have h4 : x = y := le_antisymm h.1 h1 show False exact h.2 h4 -- 3ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by intro h1 show False exact h.2 (le_antisymm h.1 h1) -- 4ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := fun h1 ↦ h.2 (le_antisymm h.1 h1) -- 5ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by intro h' -- h' : y ≤ x -- ⊢ False apply h.right -- ⊢ x = y exact le_antisymm h.left h' -- 6ª demostración -- =============== example (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by cases' h with h1 h2 -- h1 : x ≤ y -- h2 : x ≠ y contrapose! h2 -- h2 : y ≤ x -- ⊢ x = y exact le_antisymm h1 h2 -- 7ª demostración -- =============== example : x ≤ y ∧ x ≠ y → ¬ y ≤ x := by rintro ⟨h1, h2⟩ h' -- h1 : x ≤ y -- h2 : x ≠ y -- h' : y ≤ x -- ⊢ False exact h2 (le_antisymm h1 h') -- 8ª demostración -- =============== example : x ≤ y ∧ x ≠ y → ¬ y ≤ x := fun ⟨h1, h2⟩ h' ↦ h2 (le_antisymm h1 h') -- Lemas usados -- ============ -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 35.
3. Si (m ∣ n ∧ m ≠ n), entonces (m ∣ n ∧ ¬(n ∣ m))
Demostrar con Lean4 que si (m ∣ n ∧ m ≠ n), entonces (m ∣ n ∧ ¬(n ∣ m)).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Nat.GCD.Basic variable {m n : ℕ} example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by sorry |
Demostración en lenguaje natural
La primera parte de la conclusión coincide con la primera de la hipótesis. Nos queda demostrar la segunda parte; es decir, que (¬(n | m)). Para ello, supongamos que (n | m). Entonces, por la propiedad antisimétrica de la divisibilidad y la primera parte de la hipótesis, se tiene que (m = n) en contradicción con la segunda parte de la hipótesis.
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 |
import Mathlib.Data.Nat.GCD.Basic variable {m n : ℕ} -- 1ª demostración -- =============== example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by constructor . show m ∣ n exact h.left . show ¬n ∣ m { intro (h1 : n ∣ m) have h2 : m = n := dvd_antisymm h.left h1 show False exact h.right h2 } -- 2ª demostración -- =============== example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by constructor . exact h.left . intro (h1 : n ∣ m) exact h.right (dvd_antisymm h.left h1) -- 3ª demostración -- =============== example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := ⟨h.left, fun h1 ↦ h.right (dvd_antisymm h.left h1)⟩ -- 4ª demostración -- =============== example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by cases' h with h1 h2 -- h1 : m ∣ n -- h2 : m ≠ n constructor . -- ⊢ m ∣ n exact h1 . -- ⊢ ¬n ∣ m contrapose! h2 -- h2 : n ∣ m -- ⊢ m = n apply dvd_antisymm h1 h2 -- 5ª demostración -- =============== example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by rcases h with ⟨h1 : m ∣ n, h2 : m ≠ n⟩ constructor . -- ⊢ m ∣ n exact h1 . -- ⊢ ¬n ∣ m contrapose! h2 -- h2 : n ∣ m -- ⊢ m = n apply dvd_antisymm h1 h2 -- Lemas usados -- ============ -- #check (dvd_antisymm : m ∣ n → n ∣ m → m = n) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 36.
4. (∃x ∈ ℝ)[2 < x < 3]
Demostrar con Lean4 que \((∃x ∈ ℝ)[2 < x < 3]\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 |
import Mathlib.Data.Real.Basic example : ∃ x : ℝ, 2 < x ∧ x < 3 := by sorry |
Demostración en lenguaje natural
Podemos usar el número \(\dfrac{5}{2}\) y comprobar que \(2 < \dfrac{5}{2} < 3\).
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 |
import Mathlib.Data.Real.Basic -- 1ª demostración -- =============== example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 show 2 < 5 / 2 ∧ 5 / 2 < 3 constructor . show 2 < 5 / 2 norm_num . show 5 / 2 < 3 norm_num -- 2ª demostración -- =============== example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 constructor . norm_num . norm_num -- 3ª demostración -- =============== example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 constructor <;> norm_num -- 4ª demostración -- =============== example : ∃ x : ℝ, 2 < x ∧ x < 3 := ⟨5/2, by norm_num⟩ |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 36.
5. Si (∃z ∈ ℝ)[x < z < y], entonces x < y
Demostrar con Lean4 que si \((∃z ∈ ℝ)[x < z < y]\), entonces \(x < y\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) example : (∃ z : ℝ, x < z ∧ z < y) → x < y := by sorry |
Demostración en lenguaje natural
Sea \(z\) tal que verifica las siguientes relaciones:
\begin{align}
x < z \tag{1} \\
z < y \tag{2}
\end{align}
Aplicando la propiedad transitiva a (1) y (2) se tiene que
\[ x < y \]
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 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) -- 1ª demostración -- =============== example : (∃ z : ℝ, x < z ∧ z < y) → x < y := by rintro ⟨z, h1 : x < z, h2 : z < y⟩ show x < y exact lt_trans h1 h2 -- 2ª demostración -- =============== example : (∃ z : ℝ, x < z ∧ z < y) → x < y := by rintro ⟨z, h1, h2⟩ exact lt_trans h1 h2 -- 3ª demostración -- =============== example : (∃ z : ℝ, x < z ∧ z < y) → x < y := fun ⟨_, h1, h2⟩ ↦ lt_trans h1 h2 -- Lemas usados -- ============ -- variable (a b 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. 36.
6. Existen números primos m y n tales que 4 < m < n < 10
Demostrar con Lean4 que existen números primos \(m\) y \(n\) tales que \(4 < m < n < 10\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Nat.Prime import Mathlib.Tactic example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by sorry |
Demostración en lenguaje natural
Basta considerar los números \(5\) y \(7\), ya que son primos y \(4 < 5 < 7 < 10\).
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Nat.Prime import Mathlib.Tactic example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by use 5, 7 norm_num |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 36.
7. En ℝ, x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x
Demostrar con Lean4 que. en \(ℝ\), \(x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by sorry |
Demostración en lenguaje natural
Supongamos que
\begin{align}
x ≤ y \tag{1} \\
x ≠ y \tag{2}
\end{align}
Entonces, se tiene \(x ≤ y\) (por (1)) y, para probar \(y ≰ x\), supongamos que
\[ y ≤ x \tag{3}\]
Aplicando la propiedad antimétrica a (1) y (3), se obtiene que \(x = y\), en contradicción con (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 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) -- 1ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1 : x ≤ y, h2 : x ≠ y⟩ constructor . show x ≤ y exact h1 . show ¬ y ≤ x rintro h3 : y ≤ x -- ⊢ False have h4 : x = y := le_antisymm h1 h3 show False exact h2 h4 -- 2ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1 : x ≤ y, h2 : x ≠ y⟩ -- ⊢ x ≤ y ∧ ¬y ≤ x constructor . show x ≤ y exact h1 . show ¬ y ≤ x rintro h3 : y ≤ x -- ⊢ False show False exact h2 (le_antisymm h1 h3) -- 3ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1 : x ≤ y, h2 : x ≠ y⟩ constructor . show x ≤ y exact h1 . show ¬ y ≤ x exact fun h3 ↦ h2 (le_antisymm h1 h3) -- 4ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1, h2⟩ exact ⟨h1, fun h3 ↦ h2 (le_antisymm h1 h3)⟩ -- 5ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := fun ⟨h1, h2⟩ ↦ ⟨h1, fun h3 ↦ h2 (le_antisymm h1 h3)⟩ -- 6ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1 : x ≤ y, h2 : x ≠ y⟩ use h1 exact fun h3 ↦ h2 (le_antisymm h1 h3) -- 7ª demostración -- =============== example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by rintro ⟨h1, h2⟩ -- h1 : x ≤ y -- h2 : x ≠ y -- ⊢ x ≤ y ∧ ¬y ≤ x use h1 -- ¬y ≤ x contrapose! h2 -- h2 : y ≤ x -- ⊢ x = y apply le_antisymm h1 h2 -- Lemas usados -- ============ -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 36.
8. En ℝ, si x ≤ y, entonces y ≰ x ↔ x ≠ y
Demostrar con Lean4 que si \(x\) e \(y\) son números reales tales que \(x ≤ y\), entonces \(y ≰ x ↔ x ≠ y\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by sorry |
Demostración en lenguaje natural
Para demostrar la equivalencia, demostraremos cada una de las implicaciones.
Para demostrar la primera, supongamos que \(y ≰ x\) y que \(x = y\). Entonces, \(y ≤ x\) que es una contradicción.
Para demostrar la segunda, supongamos que \(x ≠ y\) y que \(y ≤ x\). Entonces, por la hipótesis y la antisimetría, se tiene que \(x = y\) 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 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 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . show ¬y ≤ x → x ≠ y { intro h1 -- h1 : ¬y ≤ x -- ⊢ x ≠ y intro h2 -- h2 : x = y -- ⊢ False have h3 : y ≤ x := by rw [h2] show False exact h1 h3 } . show x ≠ y → ¬y ≤ x { intro h1 -- h1 : x ≠ y -- ⊢ ¬y ≤ x intro h2 -- h2 : y ≤ x -- ⊢ False have h3 : x = y := le_antisymm h h2 show False exact h1 h3 } -- 2ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . show ¬y ≤ x → x ≠ y { intro h1 -- h1 : ¬y ≤ x -- ⊢ x ≠ y intro h2 -- h2 : x = y -- ⊢ False show False exact h1 (by rw [h2]) } . show x ≠ y → ¬y ≤ x { intro h1 -- h1 : x ≠ y -- ⊢ ¬y ≤ x intro h2 -- h2 : y ≤ x -- ⊢ False show False exact h1 (le_antisymm h h2) } -- 3ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . show ¬y ≤ x → x ≠ y { intro h1 h2 exact h1 (by rw [h2]) } . show x ≠ y → ¬y ≤ x { intro h1 h2 exact h1 (le_antisymm h h2) } -- 4ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . intro h1 h2 exact h1 (by rw [h2]) . intro h1 h2 exact h1 (le_antisymm h h2) -- 5ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . exact fun h1 h2 ↦ h1 (by rw [h2]) . exact fun h1 h2 ↦ h1 (le_antisymm h h2) -- 6ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := ⟨fun h1 h2 ↦ h1 (by rw [h2]), fun h1 h2 ↦ h1 (le_antisymm h h2)⟩ -- 7ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor . show ¬y ≤ x → x ≠ y { intro h1 -- h1 : ¬y ≤ x -- ⊢ x ≠ y contrapose! h1 -- h1 : x = y -- ⊢ y ≤ x calc y = x := h1.symm _ ≤ x := by rfl } . show x ≠ y → ¬y ≤ x { intro h2 -- h2 : x ≠ y -- ⊢ ¬y ≤ x contrapose! h2 -- h2 : y ≤ x -- ⊢ x = y show x = y exact le_antisymm h h2 } -- 8ª demostración -- =============== example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by constructor · -- ⊢ ¬y ≤ x → x ≠ y contrapose! -- ⊢ x = y → y ≤ x rintro rfl -- ⊢ x ≤ x rfl . -- ⊢ x ≠ y → ¬y ≤ x contrapose! -- ⊢ y ≤ x → x = y exact le_antisymm h |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 36.
9. En ℝ, x² + y² = 0 ↔ x = 0 ∧ y = 0
Demostrar con Lean4 que si \(x, y ∈ ℝ\), entonces
\[ x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := by sorry |
Demostración en lenguaje natural
En la demostración usaremos el siguiente lema auxiliar
\[ (∀ x, y ∈ ℝ)[x² + y² = 0 → x = 0] \]
Para la primera implicación, supongamos que
\[ x² + y² = 0 \tag{1} \]
Entonces, por el lema auxiliar,
\[ x = 0 \tag{2} \]
Además, aplicando la conmutativa a (1), se tiene
\[ y² + x² = 0 \]
y, por el lema auxiliar,
\[ y = 0 \tag{3} \]
De (2) y (3) se tiene
\[ x = 0 ∧ y = 0 \]
Para la segunda implicación, supongamos que
\[ x = 0 ∧ y = 0 \]
Por tanto,
\begin{align}
x² + y² &= 0² + 0² \\
&= 0
\end{align}
En la demostración del lema auxiliar se usarán los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)(∀ n ∈ ℕ)[x^n = 0 → x = 0] \tag{L1} \\
&(∀ x, y ∈ ℝ)[x ≤ y → y ≤ x → x = y] \tag{L2} \\
&(∀ x, y ∈ ℝ)[0 ≤ y → x ≤ x + y] \tag{L3} \\
&(∀ x ∈ ℝ)[0 ≤ x²] \tag{L4}
\end{align}
Por el lema L1, para demostrar el lema auxiliar basta demostrar
\[ x² = 0 \tag{1} \]
y, por el lema L2, basta demostrar las siguientes desigualdades
\begin{align}
&x² ≤ 0 \tag{2} \\
&0 ≤ x² \tag{3}
\end{align}
La prueba de la (2) es
\begin{align}
x² &≤ x² + y² &&\text{[por L3 y L4]} \\
&= 0 &&\text{[por la hipótesis]}
\end{align}
La (3) se tiene por el lema L4.
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 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración del lema auxiliar -- ================================= example (h : x^2 + y^2 = 0) : x = 0 := by have h' : x^2 = 0 := by { apply le_antisymm . show x ^ 2 ≤ 0 calc x ^ 2 ≤ x^2 + y^2 := by simp [le_add_of_nonneg_right, pow_two_nonneg] _ = 0 := by exact h . show 0 ≤ x ^ 2 apply pow_two_nonneg } show x = 0 exact pow_eq_zero h' -- 2ª demostración lema auxiliar -- ============================= example (h : x^2 + y^2 = 0) : x = 0 := by have h' : x^2 = 0 := by { apply le_antisymm . -- ⊢ x ^ 2 ≤ 0 calc x ^ 2 ≤ x^2 + y^2 := by simp [le_add_of_nonneg_right, pow_two_nonneg] _ = 0 := by exact h . -- ⊢ 0 ≤ x ^ 2 apply pow_two_nonneg } exact pow_eq_zero h' -- 3ª demostración lema auxiliar -- ============================= lemma aux (h : x^2 + y^2 = 0) : x = 0 := have h' : x ^ 2 = 0 := by linarith [pow_two_nonneg x, pow_two_nonneg y] pow_eq_zero h' -- 1ª demostración -- =============== example : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := by constructor . -- ⊢ x ^ 2 + y ^ 2 = 0 → x = 0 ∧ y = 0 intro h -- h : x ^ 2 + y ^ 2 = 0 -- ⊢ x = 0 ∧ y = 0 constructor . -- ⊢ x = 0 exact aux h . -- ⊢ y = 0 rw [add_comm] at h -- h : x ^ 2 + y ^ 2 = 0 exact aux h . -- ⊢ x = 0 ∧ y = 0 → x ^ 2 + y ^ 2 = 0 intro h1 -- h1 : x = 0 ∧ y = 0 -- ⊢ x ^ 2 + y ^ 2 = 0 rcases h1 with ⟨h2, h3⟩ -- h2 : x = 0 -- h3 : y = 0 rw [h2, h3] -- ⊢ 0 ^ 2 + 0 ^ 2 = 0 norm_num -- 2ª demostración -- =============== example : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := by constructor . -- ⊢ x ^ 2 + y ^ 2 = 0 → x = 0 ∧ y = 0 intro h -- h : x ^ 2 + y ^ 2 = 0 -- ⊢ x = 0 ∧ y = 0 constructor . -- ⊢ x = 0 exact aux h . -- ⊢ y = 0 rw [add_comm] at h -- h : x ^ 2 + y ^ 2 = 0 exact aux h . -- ⊢ x = 0 ∧ y = 0 → x ^ 2 + y ^ 2 = 0 rintro ⟨h1, h2⟩ -- h1 : x = 0 -- h2 : y = 0 -- ⊢ x ^ 2 + y ^ 2 = 0 rw [h1, h2] -- ⊢ 0 ^ 2 + 0 ^ 2 = 0 norm_num -- 3ª demostración -- =============== example : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by constructor · -- ⊢ x ^ 2 + y ^ 2 = 0 → x = 0 ∧ y = 0 intro h -- h : x ^ 2 + y ^ 2 = 0 -- ⊢ x = 0 ∧ y = 0 constructor · -- x = 0 exact aux h . -- ⊢ y = 0 rw [add_comm] at h -- h : y ^ 2 + x ^ 2 = 0 exact aux h . -- ⊢ x = 0 ∧ y = 0 → x ^ 2 + y ^ 2 = 0 rintro ⟨rfl, rfl⟩ -- ⊢ 0 ^ 2 + 0 ^ 2 = 0 norm_num -- Lemas usados -- ============ -- #check (add_comm x y : x + y = y + x) -- #check (le_add_of_nonneg_right : 0 ≤ y → x ≤ x + y) -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) -- #check (pow_eq_zero : ∀ {n : ℕ}, x ^ n = 0 → x = 0) -- #check (pow_two_nonneg x : 0 ≤ x ^ 2) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 37.
10. Si |x + 3| < 5, entonces -8 < x < 2
Demostrar con Lean4 que si \(|x + 3| < 5\), entonces \(-8 < x < 2\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) example : |x + 3| < 5 → -8 < x ∧ x < 2 := by sorry |
Demostración en lenguaje natural
Supongamos que
\[ |x + 3| < 5 \]
entonces
\[ -5 < x + 3 < 5 \]
por tanto
\[ -8 < x < 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 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) -- 1ª demostración -- =============== example : |x + 3| < 5 → -8 < x ∧ x < 2 := by rw [abs_lt] -- ⊢ -5 < x + 3 ∧ x + 3 < 5 → -8 < x ∧ x < 2 intro h -- h : -5 < x + 3 ∧ x + 3 < 5 -- ⊢ -8 < x ∧ x < 2 constructor . -- ⊢ -8 < x linarith . -- x < 2 linarith -- 2ª demostración -- =============== example : |x + 3| < 5 → -8 < x ∧ x < 2 := by rw [abs_lt] intro h constructor <;> linarith -- Comentario: La composición (constructor <;> linarith) aplica constructor y a -- continuación le aplica linarith a cada subojetivo. -- 3ª demostración -- =============== example : |x + 3| < 5 → -8 < x ∧ x < 2 := by rw [abs_lt] exact fun _ ↦ ⟨by linarith, by linarith⟩ -- Lemas usados -- ============ -- #check (abs_lt: |x| < y ↔ -y < x ∧ x < y) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 37.
11. 3 divide al máximo común divisor de 6 y 15
Demostrar con Lean4 que 3 divide al máximo común divisor de 6 y 15.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic import Mathlib.Data.Nat.GCD.Basic open Nat example : 3 ∣ gcd 6 15 := by sorry |
Demostración en lenguaje natural
Se usará el siguiente lema
\[ (∀ k, m, n ∈ ℕ)[k ∣ \gcd(m, n) ↔ k ∣ m ∧ k ∣ n] \]
Por el lema,
\[ 3 ∣ \gcd(6, 15) \]
se reduce a
\[ 3 ∣ 6 ∧ 3 ∣ 15 \]
que se verifican fácilmente.
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 |
import Mathlib.Data.Real.Basic import Mathlib.Data.Nat.GCD.Basic open Nat -- 1ª demostración -- =============== example : 3 ∣ gcd 6 15 := by rw [dvd_gcd_iff] -- ⊢ 3 ∣ 6 ∧ 3 ∣ 15 constructor . -- 3 ∣ 6 norm_num . -- ⊢ 3 ∣ 15 norm_num -- 2ª demostración -- =============== example : 3 ∣ gcd 6 15 := by rw [dvd_gcd_iff] -- ⊢ 3 ∣ 6 ∧ 3 ∣ 15 constructor <;> norm_num -- Lemas usados -- ============ -- variable (k m n : ℕ) -- #check (dvd_gcd_iff : k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 37.