La semana en Calculemus (11 de noviembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Transitividad de la divisibilidad
- 2. Si a divide a b y a c, entonces divide a b+c
- 3. La función (x ↦ x + c) es suprayectiva
- 4. Si c ≠ 0, entonces la función (x ↦ cx) es suprayectiva
- 5. Si c ≠ 0, entonces la función (x ↦ cx + d) es suprayectiva
A continuación se muestran las soluciones.
1. Transitividad de la divisibilidad
Demostrar con Lean4 la transitividad de la divisibilidad.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Tactic variable {a b c : ℕ} example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by sorry |
Demostración en lenguaje natural
Supongamos que \(a | b\) y \(b | c\). Entonces, existen \(d\) y \(e\) tales que
\begin{align}
b &= ad \tag{1} \\
c &= be \tag{2}
\end{align}
Por tanto,
\begin{align}
c &= be &&\text{[por (2)]} \\
&= (ad)e &&\text{[por (1)]} \\
&= a(de)
\end{align}
Por consiguiente, \(a | c\).
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 |
import Mathlib.Tactic variable {a b c : ℕ} -- 1ª demostración example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by rcases divab with ⟨d, beq : b = a * d⟩ rcases divbc with ⟨e, ceq : c = b * e⟩ have h1 : c = a * (d * e) := calc c = b * e := ceq _ = (a * d) * e := congrArg (. * e) beq _ = a * (d * e) := mul_assoc a d e show a ∣ c exact Dvd.intro (d * e) h1.symm -- 2ª demostración example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by rcases divab with ⟨d, beq : b = a * d⟩ rcases divbc with ⟨e, ceq : c = b * e⟩ use (d * e) -- ⊢ c = a * (d * e) rw [ceq, beq] -- ⊢ (a * d) * e = a * (d * e) exact mul_assoc a d e -- 3ª demostración example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by rcases divbc with ⟨e, rfl⟩ -- ⊢ a ∣ b * e rcases divab with ⟨d, rfl⟩ -- ⊢ a ∣ a * d * e use (d * e) -- ⊢ a * d * e = a * (d * e) ring -- 4ª demostración example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by cases' divab with d beq -- d : ℕ -- beq : b = a * d cases' divbc with e ceq -- e : ℕ -- ceq : c = b * e rw [ceq, beq] -- ⊢ a ∣ a * d * e use (d * e) -- ⊢ (a * d) * e = a * (d * e) exact mul_assoc a d e -- 5ª demostración example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by exact dvd_trans divab divbc -- Lemas usados -- ============ -- #check (mul_assoc a b c : (a * b) * c = a * (b * c)) -- #check (Dvd.intro c : a * c = b → a ∣ b) -- #check (dvd_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. 30.
2. Si a divide a b y a c, entonces divide a b+c
Demostrar con Lean4 que si \(a\) divide a \(b\) y a \(c\), entonces divide a \(b+c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Tactic variable {a b c : ℕ} example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by sorry |
Demostración en lenguaje natural
Puesto que \(a\) divide a \(b\) y a \(c\), existen \(d\) y \(e\) tales que
\begin{align}
b &= ad \tag{1} \\
c &= ae \tag{2}
\end{align}
Por tanto,
\begin{align}
b + c &= ad + c &&\text{[por (1)]} \\
&= ad + ae &&\text{[por (2)]} \\
&= a(d + e) &&\text{[por la distributiva]}
\end{align}
Por consiguiente, \(a\) divide a \(b + c\).
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 |
import Mathlib.Tactic variable {a b c : ℕ} -- 1ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by rcases h1 with ⟨d, beq : b = a * d⟩ rcases h2 with ⟨e, ceq: c = a * e⟩ have h1 : b + c = a * (d + e) := calc b + c = (a * d) + c := congrArg (. + c) beq _ = (a * d) + (a * e) := congrArg ((a * d) + .) ceq _ = a * (d + e) := by rw [← mul_add] show a ∣ (b + c) exact Dvd.intro (d + e) h1.symm -- 2ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by rcases h1 with ⟨d, beq : b = a * d⟩ rcases h2 with ⟨e, ceq: c = a * e⟩ have h1 : b + c = a * (d + e) := by linarith show a ∣ (b + c) exact Dvd.intro (d + e) h1.symm -- 3ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by rcases h1 with ⟨d, beq : b = a * d⟩ rcases h2 with ⟨e, ceq: c = a * e⟩ show a ∣ (b + c) exact Dvd.intro (d + e) (by linarith) -- 4ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by cases' h1 with d beq -- d : ℕ -- beq : b = a * d cases' h2 with e ceq -- e : ℕ -- ceq : c = a * e rw [ceq, beq] -- ⊢ a ∣ a * d + a * e use (d + e) -- ⊢ a * d + a * e = a * (d + e) ring -- 5ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by rcases h1 with ⟨d, rfl⟩ -- ⊢ a ∣ a * d + c rcases h2 with ⟨e, rfl⟩ -- ⊢ a ∣ a * d + a * e use (d + e) -- ⊢ a * d + a * e = a * (d + e) ring -- 6ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := dvd_add h1 h2 -- Lemas usados -- ============ -- #check (Dvd.intro c : a * c = b → a ∣ b) -- #check (dvd_add : a ∣ b → a ∣ c → a ∣ (b + c)) -- #check (mul_add a b c : a * (b + c) = a * b + 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. 30.
3. La función (x ↦ x + c) es suprayectiva
Demostrar con Lean4 que la función \(x ↦ x + c\) es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable {c : ℝ} open Function example : Surjective (fun x ↦ x + c) := by sorry |
Demostración en lenguaje natural
Tenemos que demostrar que
\[ (∀ x ∈ ℝ)(∃ y ∈ ℝ)[y+c = x] \]
Sea \(x ∈ ℝ\). Entonces, \(y = x-c ∈ ℝ\) y
\begin{align}
y + c &= (x – c) + c \\
&= x
\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 46 47 48 49 50 51 52 53 54 55 56 57 58 |
import Mathlib.Data.Real.Basic variable {c : ℝ} open Function -- 1ª demostración example : Surjective (fun x ↦ x + c) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => x + c) a = x use x - c -- ⊢ (fun x => x + c) (x - c) = x dsimp -- ⊢ (x - c) + c = x exact sub_add_cancel x c -- 2ª demostración example : Surjective (fun x ↦ x + c) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => x + c) a = x use x - c -- ⊢ (fun x => x + c) (x - c) = x change (x - c) + c = x -- ⊢ (x - c) + c = x exact sub_add_cancel x c -- 3ª demostración example : Surjective (fun x ↦ x + c) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => x + c) a = x use x - c -- ⊢ (fun x => x + c) (x - c) = x exact sub_add_cancel x c -- 4ª demostración example : Surjective (fun x ↦ x + c) := fun x ↦ ⟨x - c, sub_add_cancel x c⟩ -- 5ª demostración example : Surjective (fun x ↦ x + c) := fun x ↦ ⟨x - c, by ring⟩ -- 6ª demostración example : Surjective (fun x ↦ x + c) := add_right_surjective c -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (sub_add_cancel a b : (a - b) + b = a) -- #check (add_right_surjective c : Surjective (fun x ↦ x + c)) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 31.
4. Si c ≠ 0, entonces la función (x ↦ cx) es suprayectiva
Demostrar con Lean4 que si \(c ≠ 0\), entonces la función \(x ↦ cx\) es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic variable {c : ℝ} open Function example (h : c ≠ 0) : Surjective (fun x ↦ c * x) := by sorry |
Demostración en lenguaje natural
Hay que demostrar que
\[ (∀ x ∈ ℝ)(∃ y ∈ ℝ)[cy = x] \]
Sea \(x ∈ ℝ\). Entonces, \(y = x/c ∈ R\) y
\begin{align}
cy &= c(x/c) \\
&= 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 46 47 48 49 50 51 52 |
import Mathlib.Data.Real.Basic variable {c : ℝ} open Function -- 1ª demostración example (h : c ≠ 0) : Surjective (fun x ↦ c * x) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => c * x) a = x use (x / c) -- ⊢ (fun x => c * x) (x / c) = x dsimp -- ⊢ c * (x / c) = x rw [mul_comm] -- ⊢ (x / c) * c = x exact div_mul_cancel x h -- 2ª demostración example (h : c ≠ 0) : Surjective (fun x ↦ c * x) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => c * x) a = x use (x / c) -- ⊢ (fun x => c * x) (x / c) = x exact mul_div_cancel' x h -- 3ª demostración example (h : c ≠ 0) : Surjective (fun x ↦ c * x) := fun x ↦ ⟨x / c, mul_div_cancel' x h⟩ -- 4ª demostración example (h : c ≠ 0) : Surjective (fun x ↦ c * x) := mul_left_surjective₀ h -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (div_mul_cancel a : b ≠ 0 → (a / b) * b = a) -- #check (mul_comm a b : a * b = b * a) -- #check (mul_div_cancel' a : b ≠ 0 → b * (a / b) = a) -- #check (mul_left_surjective₀ : c ≠ 0 → Surjective (fun x ↦ c * x)) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 31.
5. Si c ≠ 0, entonces la función (x ↦ cx + d) es suprayectiva
Demostrar con Lean4 que si \(c ≠ 0\), entonces la función \(x ↦ cx + d\) es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic variable {c d : ℝ} open Function example (h : c ≠ 0) : Surjective (fun x ↦ c * x + d) := by sorry |
Demostración en lenguaje natural
Hay que demostrar que
\[ (∀x ∈ ℝ)(∃y ∈ ℝ)[cy+d = x] \]
Para \(x ∈ ℝ\), sea \(y = \dfrac{x-d}{c}\). Entonces,
\begin{align}
cy &= c\left(\frac{x-d}{c}\right)+d \\
&= (x-d)+d \\
&= x
\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 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 |
import Mathlib.Data.Real.Basic variable {c d : ℝ} open Function -- 1ª demostración -- =============== example (h : c ≠ 0) : Surjective (fun x ↦ c * x + d) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => c * x + d) a = x use ((x - d) / c) -- ⊢ (fun x => c * x + d) ((x - d) / c) = x dsimp -- ⊢ c * ((x - d) / c) + d = x show c * ((x - d) / c) + d = x calc c * ((x - d) / c) + d = (x - d) + d := congrArg (. + d) (mul_div_cancel' (x - d) h) _ = x := sub_add_cancel x d -- 2ª demostración -- =============== example (h : c ≠ 0) : Surjective (fun x ↦ c * x + d) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => c * x + d) a = x use ((x - d) / c) -- ⊢ (fun x => c * x + d) ((x - d) / c) = x dsimp -- ⊢ c * ((x - d) / c) + d = x simp [mul_div_cancel', h] -- 3ª demostración -- =============== example (h : c ≠ 0) : Surjective (fun x ↦ c * x + d) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => c * x + d) a = x use ((x - d) / c) -- ⊢ (fun x => c * x + d) ((x - d) / c) = x simp [mul_div_cancel', h] -- 4ª demostración -- =============== example (h : c ≠ 0) : Surjective (fun x ↦ c * x + d) := fun x ↦ ⟨(x - d) / c, by simp [mul_div_cancel', h]⟩ -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (mul_div_cancel' a : b ≠ 0 → b * (a / b) = a) -- #check (sub_add_cancel a b : a - b + b = a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.