La semana en Calculemus (24 de febrero de 2024)
Estas 3 últimas semanas he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Si la sucesión u converge a a y la v a b, entonces u+v converge a a+b
- 2. Unicidad del límite de las sucesiones convergentes
- 3. Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de uₙ+c es a+c
- 4. Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de cuₙ es ca
- 5. El límite de uₙ es a syss el de uₙ-a es 0
- 6. Si uₙ y vₙ convergen a 0, entonces uₙvₙ converge a 0
- 7. Teorema del emparedado
- 8. Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u
- 9. s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)
- 10. (s \ t) \ u ⊆ s \ (t ∪ u)
- 11. (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)
A continuación se muestran las soluciones.
1. Si la sucesión u converge a a y la v a b, entonces u+v converge a a+b
Demostrar con Lean4 que si la sucesión \(u\) converge a \(a\) y la \(v\) a \(b\), entonces \(u+v\) converge a \(a+b\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Real.Basic variable {s t : ℕ → ℝ} {a b c : ℝ} def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by sorry |
1.1. Demostración en lenguaje natural
En la demostración usaremos los siguientes lemas
\begin{align}
&(∀ a ∈ ℝ)\left[a > 0 → \frac{a}{2} > 0\right] \tag{L1} \\
&(∀ a, b, c ∈ ℝ)[\max(a, b) ≤ c → a ≤ c] \tag{L2} \\
&(∀ a, b, c ∈ ℝ)[\max(a, b) ≤ c → b ≤ c] \tag{L3} \\
&(∀ a, b ∈ ℝ)[|a + b| ≤ |a| + |b|] \tag{L4} \\
&(∀ a ∈ ℝ)\left[\frac{a}{2} + \frac{a}{2} = a\right] \tag{L5}
\end{align}
Tenemos que probar que para todo \(ε ∈ ℝ\), si
\[ ε > 0 \tag{1} \]
entonces
\[ (∃N ∈ ℕ)(∀n ∈ ℕ)[n ≥ N → |(u + v)(n) – (a + b)| < ε] \tag{2} \]
Por (1) y el lema L1, se tiene que
\[ \frac{ε}{2} > 0 \tag{3} \]
Por (3) y porque el límite de \(u\) es \(a\), se tiene que
\[ (∃N ∈ ℕ)(∀n ∈ ℕ)\left[n ≥ N → |u(n) – a| < \frac{ε}{2}\right] \]
Sea \(N₁ ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ N₁ → |u(n) – a| < \frac{ε}{2}\right] \tag{4} \]
Por (3) y porque el límite de \(v\) es \(b\), se tiene que
\[ (∃N ∈ ℕ)(∀n ∈ ℕ)\left[n ≥ N → |v(n) – b| < \frac{ε}{2}\right] \]
Sea \(N₂ ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ N₂ → |v(n) – b| < \frac{ε}{2}\right] \tag{5} \]
Sea \(N = \max(N₁, N₂)\). Veamos que verifica la condición (1). Para ello, sea \(n ∈ ℕ\) tal que \(n ≥ N\). Entonces, \(n ≥ N₁\) (por L2) y \(n ≥ N₂\) (por L3). Por tanto, usando las propiedades (4) y (5) se tiene que
\begin{align}
|u(n) – a| &< \frac{ε}{2} \tag{6} \\
|v(n) – b| &< \frac{ε}{2} \tag{7}
\end{align}
Finalmente,
\begin{align}
|(u + v)(n) – (a + b)| &= |(u(n) + v(n)) – (a + b)| \\
&= |(u(n) – a) + (v(n) – b)| \\
&≤ |u(n) – a| + |v(n) – b| &&\text{[por L4]}\\
&< \frac{ε}{2} + \frac{ε}{2} &&\text{[por (6) y (7)]}\\
&= ε &&\text{[por L5]}
\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 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 175 176 177 178 |
import Mathlib.Data.Real.Basic variable {s t : ℕ → ℝ} {a b c : ℝ} def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε -- 1ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(u + v) n - (a + b)| < ε have hε2 : 0 < ε / 2 := half_pos hε cases' hu (ε / 2) hε2 with Nu hNu -- Nu : ℕ -- hNu : ∀ (n : ℕ), n ≥ Nu → |u n - a| < ε / 2 cases' hv (ε / 2) hε2 with Nv hNv -- Nv : ℕ -- hNv : ∀ (n : ℕ), n ≥ Nv → |v n - b| < ε / 2 clear hu hv hε2 hε let N := max Nu Nv use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(s + t) n - (a + b)| < ε intros n hn -- n : ℕ -- hn : n ≥ N have nNu : n ≥ Nu := le_of_max_le_left hn specialize hNu n nNu -- hNu : |u n - a| < ε / 2 have nNv : n ≥ Nv := le_of_max_le_right hn specialize hNv n nNv -- hNv : |v n - b| < ε / 2 clear hn nNu nNv calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| := rfl _ = |(u n - a) + (v n - b)| := by { congr; ring } _ ≤ |u n - a| + |v n - b| := by apply abs_add _ < ε / 2 + ε / 2 := by linarith [hNu, hNv] _ = ε := by apply add_halves -- 2ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε hε cases' hu (ε/2) (by linarith) with Nu hNu cases' hv (ε/2) (by linarith) with Nv hNv use max Nu Nv intros n hn have hn₁ : n ≥ Nu := le_of_max_le_left hn specialize hNu n hn₁ have hn₂ : n ≥ Nv := le_of_max_le_right hn specialize hNv n hn₂ calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| := by rfl _ = |(u n - a) + (v n - b)| := by {congr; ring} _ ≤ |u n - a| + |v n - b| := by apply abs_add _ < ε / 2 + ε / 2 := by linarith _ = ε := by apply add_halves -- 3ª demostración -- =============== lemma max_ge_iff {α : Type _} [LinearOrder α] {p q r : α} : r ≥ max p q ↔ r ≥ p ∧ r ≥ q := max_le_iff example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε hε cases' hu (ε/2) (by linarith) with Nu hNu cases' hv (ε/2) (by linarith) with Nv hNv use max Nu Nv intros n hn cases' max_ge_iff.mp hn with hn₁ hn₂ have cota₁ : |u n - a| < ε/2 := hNu n hn₁ have cota₂ : |v n - b| < ε/2 := hNv n hn₂ calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| := by rfl _ = |(u n - a) + (v n - b)| := by { congr; ring } _ ≤ |u n - a| + |v n - b| := by apply abs_add _ < ε := by linarith -- 4ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε hε cases' hu (ε/2) (by linarith) with Nu hNu cases' hv (ε/2) (by linarith) with Nv hNv use max Nu Nv intros n hn cases' max_ge_iff.mp hn with hn₁ hn₂ calc |(u + v) n - (a + b)| = |u n + v n - (a + b)| := by rfl _ = |(u n - a) + (v n - b)| := by { congr; ring } _ ≤ |u n - a| + |v n - b| := by apply abs_add _ < ε/2 + ε/2 := add_lt_add (hNu n hn₁) (hNv n hn₂) _ = ε := by simp -- 5ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε hε cases' hu (ε/2) (by linarith) with Nu hNu cases' hv (ε/2) (by linarith) with Nv hNv use max Nu Nv intros n hn rw [max_ge_iff] at hn calc |(u + v) n - (a + b)| = |u n + v n - (a + b)| := by rfl _ = |(u n - a) + (v n - b)| := by { congr; ring } _ ≤ |u n - a| + |v n - b| := by apply abs_add _ < ε := by linarith [hNu n (by linarith), hNv n (by linarith)] -- 6ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε Hε cases' hu (ε/2) (by linarith) with L HL cases' hv (ε/2) (by linarith) with M HM set N := max L M with _hN use N have HLN : N ≥ L := le_max_left _ _ have HMN : N ≥ M := le_max_right _ _ intros n Hn have H3 : |u n - a| < ε/2 := HL n (by linarith) have H4 : |v n - b| < ε/2 := HM n (by linarith) calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| := by rfl _ = |(u n - a) + (v n - b)| := by {congr; ring } _ ≤ |(u n - a)| + |(v n - b)| := by apply abs_add _ < ε/2 + ε/2 := by linarith _ = ε := by ring -- Lemas usados -- ============ -- variable (d : ℝ) -- #check (abs_add a b : |a + b| ≤ |a| + |b|) -- #check (add_halves a : a / 2 + a / 2 = a) -- #check (add_lt_add : a < b → c < d → a + c < b + d) -- #check (half_pos : a > 0 → a / 2 > 0) -- #check (le_max_left a b : a ≤ max a b) -- #check (le_max_right a b : b ≤ max a b) -- #check (le_of_max_le_left : max a b ≤ c → a ≤ c) -- #check (le_of_max_le_right : max a b ≤ c → b ≤ c) -- #check (max_le_iff : max a b ≤ c ↔ a ≤ c ∧ b ≤ c) |
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 |
theory Limite_de_sucesiones_constantes imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" (* 1ª demostración *) lemma "limite (λ n. c) c" proof (unfold limite_def) show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" have "∀n≥0::nat. ¦c - c¦ < ε" proof (intro allI impI) fix n :: nat assume "0 ≤ n" have "c - c = 0" by (simp only: diff_self) then have "¦c - c¦ = 0" by (simp only: abs_eq_0_iff) also have "… < ε" by (simp only: ‹0 < ε›) finally show "¦c - c¦ < ε" by this qed then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI) qed qed (* 2ª demostración *) lemma "limite (λ n. c) c" proof (unfold limite_def) show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" have "∀n≥0::nat. ¦c - c¦ < ε" by (simp add: ‹0 < ε›) then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI) qed qed (* 3ª demostración *) lemma "limite (λ n. c) c" unfolding limite_def by simp (* 4ª demostración *) lemma "limite (λ n. c) c" by (simp add: limite_def) end |
2. Unicidad del límite de las sucesiones convergentes
En Lean, una sucesión \(u₀, u₁, u₂, …\) se puede representar mediante una función \((u : ℕ → ℝ)\) de forma que \(u(n)\) es \(uₙ\).
Se define que \(a\) es el límite de la sucesión \(u\), por
|
1 2 |
def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε |
Demostrar con Lean4 que cada sucesión tiene como máximo un límite.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Real.Basic variable {u : ℕ → ℝ} variable {a b : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (ha : limite u a) (hb : limite u b) : a = b := by sorry |
2.1. Demostración en lenguaje natural
Tenemos que demostrar que si \(u\) es una sucesión y \(a\) y \(b\) son límites de \(u\), entonces \(a = b\). Para ello, basta demostrar que \(a ≤ b\) y \(b ≤ a\).
Demostraremos que \(b ≤ a\) por reducción al absurdo. Supongamos que \(b ≰ a\). Sea \(ε = b – a\). Entonces, ε/2 > 0 y, puesto que \(a\) es un límite de \(u\), existe un \(A ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ A → |u(n) – a| < \frac{ε}{2}\right] \tag{1} \]
y, puesto que \(b\) también es un límite de \(u\), existe un \(B ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ B → |u(n) – b| < \frac{ε}{2}\right] \tag{2} \]
Sea \(N = máx(A, B)\). Entonces, \(N ≥ A\) y \(N ≥ B\) y, por (2) y (3), se tiene
\begin{align}
|u(N) – a| &< \frac{ε}{2} \tag{3} \\
|u(N) – b| &< \frac{ε}{2} \tag{4}
\end{align}
Para obtener una contradicción basta probar que \(ε < ε\). Su prueba es
\begin{align}
ε &= b – a \\
&= |b – a| \\
&= |(b – a) + (u(N) – u(N))| \\
&= |(u(N) – a) + (b – u(N))| \\
&≤ |u(N) – a| + |b – u(N)| \\
&= |u(N) – a| + |u(N) – b| \\
&< \frac{ε}{2} + \frac{ε}{2} && \text{[por (3) y (4)]} \\
&= ε
\end{align}
La demostración de \(a ≤ b\) es análoga a la anterior.
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 |
import Mathlib.Data.Real.Basic variable {u : ℕ → ℝ} variable {a b : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración del lema auxiliar -- ================================= example (ha : limite u a) (hb : limite u b) : b ≤ a := by by_contra h -- h : ¬b ≤ a -- ⊢ False let ε := b - a have hε : ε > 0 := sub_pos.mpr (not_le.mp h) have hε2 : ε / 2 > 0 := half_pos hε cases' ha (ε/2) hε2 with A hA -- A : ℕ -- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2 cases' hb (ε/2) hε2 with B hB -- B : ℕ -- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2 let N := max A B have hAN : A ≤ N := le_max_left A B have hBN : B ≤ N := le_max_right A B specialize hA N hAN -- hA : |u N - a| < ε / 2 specialize hB N hBN -- hB : |u N - b| < ε / 2 have h2 : ε < ε := by calc ε = b - a := rfl _ = |b - a| := (abs_of_pos hε).symm _ = |(b - a) + 0| := by {congr ; exact (add_zero (b - a)).symm} _ = |(b - a) + (u N - u N)| := by {congr ; exact (sub_self (u N)).symm} _ = |(u N - a) + (b - u N)| := congrArg (fun x => |x|) (by ring) _ ≤ |u N - a| + |b - u N| := abs_add (u N - a) (b - u N) _ = |u N - a| + |u N - b| := congrArg (|u N - a| + .) (abs_sub_comm b (u N)) _ < ε / 2 + ε / 2 := add_lt_add hA hB _ = ε := add_halves ε have h3 : ¬(ε < ε) := lt_irrefl ε show False exact h3 h2 -- 2ª demostración del lema auxiliar -- ================================= lemma aux (ha : limite u a) (hb : limite u b) : b ≤ a := by by_contra h -- h : ¬b ≤ a -- ⊢ False let ε := b - a cases' ha (ε/2) (by linarith) with A hA -- A : ℕ -- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2 cases' hb (ε/2) (by linarith) with B hB -- B : ℕ -- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2 let N := max A B have hAN : A ≤ N := le_max_left A B have hBN : B ≤ N := le_max_right A B specialize hA N hAN -- hA : |u N - a| < ε / 2 specialize hB N hBN -- hB : |u N - b| < ε / 2 rw [abs_lt] at hA hB -- hA : -(ε / 2) < u N - a ∧ u N - a < ε / 2 -- hB : -(ε / 2) < u N - b ∧ u N - b < ε / 2 linarith -- 1ª demostración -- =============== example (ha : limite u a) (hb : limite u b) : a = b := le_antisymm (aux hb ha) (aux ha hb) -- Lemas usados -- ============ -- variable (c d : ℝ) -- #check (not_le : ¬a ≤ b ↔ b < a) -- #check (sub_pos : 0 < a - b ↔ b < a) -- #check (half_pos : a > 0 → a / 2 > 0) -- #check (le_max_left a b : a ≤ max a b) -- #check (le_max_right a b : b ≤ max a b) -- #check (abs_lt : |a| < b ↔ -b < a ∧ a < b) -- #check (abs_of_pos : 0 < a → |a| = a) -- #check (add_zero a : a + 0 = a) -- #check (sub_self a : a - a = 0) -- #check (abs_add a b : |a + b| ≤ |a| + |b|) -- #check (abs_sub_comm a b : |a - b| = |b - a|) -- #check (add_lt_add : a < b → c < d → a + c < b + d) -- #check (add_halves a : a / 2 + a / 2 = a) -- #check (lt_irrefl a : ¬a < a) -- #check (le_antisymm : a ≤ b → b ≤ a → a = b) |
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 |
theory Unicidad_del_limite_de_las_sucesiones_convergentes imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" lemma aux : assumes "limite u a" "limite u b" shows "b ≤ a" proof (rule ccontr) assume "¬ b ≤ a" let ?ε = "b - a" have "0 < ?ε/2" using ‹¬ b ≤ a› by auto obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2" using assms(1) limite_def ‹0 < ?ε/2› by blast obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2" using assms(2) limite_def ‹0 < ?ε/2› by blast let ?C = "max A B" have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2" using hA by simp have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2" using hB by simp have "∀n≥?C. ¦a - b¦ < ?ε" proof (intro allI impI) fix n assume "n ≥ ?C" have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp finally show "¦a - b¦ < b - a" using hCa hCb ‹n ≥ ?C› by fastforce qed then show False by fastforce qed theorem assumes "limite u a" "limite u b" shows "a = b" proof (rule antisym) show "a ≤ b" using assms(2) assms(1) by (rule aux) next show "b ≤ a" using assms(1) assms(2) by (rule aux) qed end |
3. Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de uₙ+c es a+c
Demostrar con Lean4 que si el límite de la sucesión \(uₙ\) es \(a\) y \(c ∈ ℝ\), entonces el límite de \(uₙ+c\) es \(a+c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} variable {a c : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (h : limite u a) : limite (fun i ↦ u i + c) (a + c) := by sorry |
3.1. Demostración en lenguaje natural
Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Tenemos que demostrar que
\[ (∃ N)(∀ n ≥ N)[|(u(n) + c) – (a + c)| < ε] \tag{1} \]
Puesto que el límite de la sucesión \(u\) es \(a\), existe un \(k\) tal que
\[ (∀ n ≥ k)[|u(n) – a| < ε] \tag{2} \]
Veamos que con k se verifica (1); es decir, que
\[ (∀ n ≥ k)[|(u(n) + c) – (a + c)| < ε] \]
Sea \(n ≥ k\). Entonces, por (2),
\[ |u(n) – a| < ε \tag{3} \]
y, por consiguiente,
\begin{align}
|(u(n) + c) – (a + c)| &= |u(n) – a| \\
&< ε &&\text{[por (3)]}
\end{align}
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 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} variable {a c : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración -- =============== example (h : limite u a) : limite (fun i ↦ u i + c) (a + c) := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun i => u i + c) n - (a + c)| < ε dsimp -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |u n + c - (a + c)| < ε cases' h ε hε with k hk -- k : ℕ -- hk : ∀ (n : ℕ), n ≥ k → |u n - a| < ε use k -- ⊢ ∀ (n : ℕ), n ≥ k → |u n + c - (a + c)| < ε intros n hn -- n : ℕ -- hn : n ≥ k calc |u n + c - (a + c)| = |u n - a| := by norm_num _ < ε := hk n hn -- 2ª demostración -- =============== example (h : limite u a) : limite (fun i ↦ u i + c) (a + c) := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun i => u i + c) n - (a + c)| < ε dsimp -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |u n + c - (a + c)| < ε cases' h ε hε with k hk -- k : ℕ -- hk : ∀ (n : ℕ), n ≥ k → |u n - a| < ε use k -- ⊢ ∀ (n : ℕ), n ≥ k → |u n + c - (a + c)| < ε intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |u n + c - (a + c)| < ε convert hk n hn using 2 -- ⊢ u n + c - (a + c) = u n - a ring -- 3ª demostración -- =============== example (h : limite u a) : limite (fun i ↦ u i + c) (a + c) := by intros ε hε dsimp convert h ε hε using 6 ring -- 4ª demostración -- =============== example (h : limite u a) : limite (fun i ↦ u i + c) (a + c) := fun ε hε ↦ (by convert h ε hε using 6; ring) |
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 |
theory Limite_cuando_se_suma_una_constante imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" (* 1ª demostración *) lemma assumes "limite u a" shows "limite (λ i. u i + c) (a + c)" proof (unfold limite_def) show "∀ε>0. ∃k. ∀n≥k. ¦(u n + c) - (a + c)¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" then have "∃k. ∀n≥k. ¦u n - a¦ < ε" using assms limite_def by simp then obtain k where "∀n≥k. ¦u n - a¦ < ε" by (rule exE) then have "∀n≥k. ¦(u n + c) - (a + c)¦ < ε" by simp then show "∃k. ∀n≥k. ¦(u n + c) - (a + c)¦ < ε" by (rule exI) qed qed (* 2ª demostración *) lemma assumes "limite u a" shows "limite (λ i. u i + c) (a + c)" using assms limite_def by simp end |
4. Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de cuₙ es ca
Demostrar con Lean4 que si el límite de la sucesión \(uₙ\) es \(a\) y \(c ∈ ℝ\), entonces el límite de \(cuₙ\) es \(ca\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (u v : ℕ → ℝ) variable (a c : ℝ) def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (h : limite u a) : limite (fun n ↦ c * (u n)) (c * a) := by |
4.1. Demostración en lenguaje natural
Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Tenemos que demostrar que
\[ (∃ N ∈ ℕ)(∀ n ≥ N)[|cuₙ – ca| < ε] \tag{1}\]
Distinguiremos dos casos según sea \(c = 0\) o no.
Primer caso: Supongamos que \(c = 0\). Entonces, (1) se reduce a
\[ (∃ N ∈ ℕ)(∀ n ≥ N)[|0·uₙ – 0·a| < ε] \]
es decir,
\[ (∃ N ∈ ℕ)(∀ n ≥ N)[0 < ε] \]
que se verifica para cualquier número \(N\), ya que \(ε > 0\).
Segundo caso: Supongamos que \(c ≠ 0\). Entonces, \(\dfrac{ε}{|c|}\) > 0 y, puesto que el límite de \(uₙ\) es \(a\), existe un \(k ∈ ℕ\) tal que
\[ (∀ n ≥ k)[|uₙ – a| < \frac{ε}{|c|}] \tag{2} \]
Veamos que con \(k\) se cumple (1). En efecto, sea \(n ≥ k\). Entonces,
\begin{align}
|cuₙ – ca| &= |c(uₙ – a)| \\
&= |c||uₙ – a| \\
&< |c|\frac{ε}{|c|} &&\text{[por (2)]} \\
&= ε
\end{align}
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 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 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (u v : ℕ → ℝ) variable (a c : ℝ) def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración -- =============== example (h : limite u a) : limite (fun n ↦ c * (u n)) (c * a) := by by_cases hc : c = 0 . -- hc : c = 0 subst hc -- ⊢ limite (fun n => 0 * u n) (0 * a) intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => 0 * u n) n - 0 * a| < ε aesop . -- hc : ¬c = 0 intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => c * u n) n - c * a| < ε have hc' : 0 < |c| := abs_pos.mpr hc have hεc : 0 < ε / |c| := div_pos hε hc' specialize h (ε/|c|) hεc -- h : ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε / |c| cases' h with N hN -- N : ℕ -- hN : ∀ (n : ℕ), n ≥ N → |u n - a| < ε / |c| use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(fun n => c * u n) n - c * a| < ε intros n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |(fun n => c * u n) n - c * a| < ε specialize hN n hn -- hN : |u n - a| < ε / |c| dsimp only calc |c * u n - c * a| = |c * (u n - a)| := congr_arg abs (mul_sub c (u n) a).symm _ = |c| * |u n - a| := abs_mul c (u n - a) _ < |c| * (ε / |c|) := (mul_lt_mul_left hc').mpr hN _ = ε := mul_div_cancel' ε (ne_of_gt hc') -- 2ª demostración -- =============== example (h : limite u a) : limite (fun n ↦ c * (u n)) (c * a) := by by_cases hc : c = 0 . -- hc : c = 0 subst hc -- ⊢ limite (fun n => 0 * u n) (0 * a) intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => 0 * u n) n - 0 * a| < ε aesop . -- hc : ¬c = 0 intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => c * u n) n - c * a| < ε have hc' : 0 < |c| := abs_pos.mpr hc have hεc : 0 < ε / |c| := div_pos hε hc' specialize h (ε/|c|) hεc -- h : ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε / |c| cases' h with N hN -- N : ℕ -- hN : ∀ (n : ℕ), n ≥ N → |u n - a| < ε / |c| use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(fun n => c * u n) n - c * a| < ε intros n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |(fun n => c * u n) n - c * a| < ε specialize hN n hn -- hN : |u n - a| < ε / |c| dsimp only -- ⊢ |c * u n - c * a| < ε rw [← mul_sub] -- ⊢ |c * (u n - a)| < ε rw [abs_mul] -- ⊢ |c| * |u n - a| < ε rw [← lt_div_iff' hc'] -- ⊢ |u n - a| < ε / |c| exact hN -- 3ª demostración -- =============== example (h : limite u a) : limite (fun n ↦ c * (u n)) (c * a) := by by_cases hc : c = 0 . subst hc intros ε hε aesop . intros ε hε have hc' : 0 < |c| := by aesop have hεc : 0 < ε / |c| := div_pos hε hc' cases' h (ε/|c|) hεc with N hN use N intros n hn specialize hN n hn dsimp only rw [← mul_sub, abs_mul, ← lt_div_iff' hc'] exact hN -- Lemas usados -- ============ -- variable (b c : ℝ) -- #check (abs_mul a b : |a * b| = |a| * |b|) -- #check (abs_pos.mpr : a ≠ 0 → 0 < |a|) -- #check (div_pos : 0 < a → 0 < b → 0 < a / b) -- #check (lt_div_iff' : 0 < c → (a < b / c ↔ c * a < b)) -- #check (mul_div_cancel' a : b ≠ 0 → b * (a / b) = a) -- #check (mul_lt_mul_left : 0 < a → (a * b < a * c ↔ b < c)) -- #check (mul_sub a b c : a * (b - c) = a * b - a * c) |
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 46 47 48 49 50 51 |
theory Limite_multiplicado_por_una_constante imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" lemma assumes "limite u a" shows "limite (λ n. c * u n) (c * a)" proof (unfold limite_def) show "∀ε>0. ∃k. ∀n≥k. ¦c * u n - c * a¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" show "∃k. ∀n≥k. ¦c * u n - c * a¦ < ε" proof (cases "c = 0") assume "c = 0" then show "∃k. ∀n≥k. ¦c * u n - c * a¦ < ε" by (simp add: ‹0 < ε›) next assume "c ≠ 0" then have "0 < ¦c¦" by simp then have "0 < ε/¦c¦" by (simp add: ‹0 < ε›) then obtain N where hN : "∀n≥N. ¦u n - a¦ < ε/¦c¦" using assms limite_def by auto have "∀n≥N. ¦c * u n - c * a¦ < ε" proof (intro allI impI) fix n assume "n ≥ N" have "¦c * u n - c * a¦ = ¦c * (u n - a)¦" by argo also have "… = ¦c¦ * ¦u n - a¦" by (simp only: abs_mult) also have "… < ¦c¦ * (ε/¦c¦)" using hN ‹n ≥ N› ‹0 < ¦c¦› by (simp only: mult_strict_left_mono) finally show "¦c * u n - c * a¦ < ε" using ‹0 < ¦c¦› by auto qed then show "∃k. ∀n≥k. ¦c * u n - c * a¦ < ε" by (rule exI) qed qed qed end |
5. El límite de uₙ es a syss el de uₙ-a es 0
Demostrar con Lean4 que el límite de \(uₙ\) es \(a\) si, y sólo si, el de \(uₙ-a\) es \(0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} variable {a c x : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example : limite u a ↔ limite (fun i ↦ u i - a) 0 := by sorry |
5.1. Demostración en lenguaje natural
Se prueba por la siguiente cadena de equivalencias
\begin{align}
&\text{el límite de \(uₙ\) es \(a\)} \\
&↔ (∀ε>0)(∃N)(∀n≥N)[|u(n) – a| < ε] \\
&↔ (∀ε>0)(∃N)(∀n≥N)[|(u(n) – a) – 0| < ε] \\
&↔ \text{el límite de \(uₙ-a\) es \(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 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} variable {a c x : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración -- =============== example : limite u a ↔ limite (fun i ↦ u i - a) 0 := by rw [iff_eq_eq] calc limite u a = ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε := rfl _ = ∀ ε > 0, ∃ N, ∀ n ≥ N, |(u n - a) - 0| < ε := by simp _ = limite (fun i ↦ u i - a) 0 := rfl -- 2ª demostración -- =============== example : limite u a ↔ limite (fun i ↦ u i - a) 0 := by constructor . -- ⊢ limite u a → limite (fun i => u i - a) 0 intros h ε hε -- h : limite u a -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun i => u i - a) n - 0| < ε convert h ε hε using 2 -- x : ℕ -- ⊢ (∀ (n : ℕ), n ≥ x → |(fun i => u i - a) n - 0| < ε) ↔ ∀ (n : ℕ), n ≥ x → |u n - a| < ε norm_num . -- ⊢ limite (fun i => u i - a) 0 → limite u a intros h ε hε -- h : limite (fun i => u i - a) 0 -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε convert h ε hε using 2 -- x : ℕ -- ⊢ (∀ (n : ℕ), n ≥ x → |u n - a| < ε) ↔ ∀ (n : ℕ), n ≥ x → |(fun i => u i - a) n - 0| < ε norm_num -- 3ª demostración -- =============== example : limite u a ↔ limite (fun i ↦ u i - a) 0 := by constructor <;> { intros h ε hε convert h ε hε using 2 norm_num } -- 4ª demostración -- =============== lemma limite_con_suma (c : ℝ) (h : limite u a) : limite (fun i ↦ u i + c) (a + c) := fun ε hε ↦ (by convert h ε hε using 2; norm_num) lemma CNS_limite_con_suma (c : ℝ) : limite u a ↔ limite (fun i ↦ u i + c) (a + c) := by constructor . -- ⊢ limite u a → limite (fun i => u i + c) (a + c) apply limite_con_suma . -- ⊢ limite (fun i => u i + c) (a + c) → limite u a intro h -- h : limite (fun i => u i + c) (a + c) -- ⊢ limite u a convert limite_con_suma (-c) h using 2 . -- ⊢ u x = u x + c + -c simp . -- ⊢ a = a + c + -c simp example (u : ℕ → ℝ) (a : ℝ) : limite u a ↔ limite (fun i ↦ u i - a) 0 := by convert CNS_limite_con_suma (-a) using 2 -- ⊢ 0 = a + -a simp -- Lemas usados -- ============ -- variable (p q : Prop) -- #check (iff_eq_eq : (p ↔ q) = (p = q)) |
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 |
theory "El_limite_de_u_es_a_syss_el_de_u-a_es_0" imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" (* 1ª demostración *) lemma "limite u a ⟷ limite (λ i. u i - a) 0" proof - have "limite u a ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - a¦ < ε)" by (rule limite_def) also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)" by simp also have "… ⟷ limite (λ i. u i - a) 0" by (rule limite_def[symmetric]) finally show "limite u a ⟷ limite (λ i. u i - a) 0" by this qed (* 2ª demostración *) lemma "limite u a ⟷ limite (λ i. u i - a) 0" proof - have "limite u a ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - a¦ < ε)" by (simp only: limite_def) also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)" by simp also have "… ⟷ limite (λ i. u i - a) 0" by (simp only: limite_def) finally show "limite u a ⟷ limite (λ i. u i - a) 0" by this qed (* 3ª demostración *) lemma "limite u a ⟷ limite (λ i. u i - a) 0" using limite_def by simp end |
6. Si uₙ y vₙ convergen a 0, entonces uₙvₙ converge a 0
Demostrar con Lean4 que si \(uₙ\) y \(vₙ\) convergen a \(0\), entonces \(uₙvₙ\) converge a \(0).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u v : ℕ → ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (hu : limite u 0) (hv : limite v 0) : limite (u * v) 0 := by sorry |
6.1. Demostración en lenguaje natural
Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Tenemos que demostrar que
\[ (∃N ∈ ℕ)(∀n ≥ N)[|(u·v)(n) – 0| < ε] \tag{1} \]
Puesto que el límite de \(uₙ\) es \(0\), existe un \(U ∈ ℕ\) tal que
\[ (∀n ≥ U)[|u(n) – 0| < ε] \tag{2} \]
y, puesto que el límite de \(vₙ\) es \(0\), existe un \(V ∈ ℕ\) tal que
\[ (∀n ≥ V)[|v(n) – 0| < 1] \tag{3} \]
Entonces, \(N = \text{máx}(U, V)\) cumple (1). En efecto, sea \(n ≥ N\). Entonces,
\(n ≥ U\) y \(n ≥ V\) y, aplicando (2) y (3), se tiene
\begin{align}
&|u(n) – 0| < ε \tag{4} \\
&|v(n) – 0| < 1 \tag{5}
\end{align}
Por tanto,
\begin{align}
|(u·v)(n) – 0| &= |u(n)·v(n)| \\
&= |u(n)|·|v n| \\
&< ε·1 &&\text{[por (4) y (5)]} \\
&= ε
\end{align}
6.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 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u v : ℕ → ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración -- =============== example (hu : limite u 0) (hv : limite v 0) : limite (u * v) 0 := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε cases' hu ε hε with U hU -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - 0| < ε cases' hv 1 zero_lt_one with V hV -- V : ℕ -- hV : ∀ (n : ℕ), n ≥ V → |v n - 0| < 1 let N := max U V use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε intros n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |(u * v) n - 0| < ε specialize hU n (le_of_max_le_left hn) -- hU : |u n - 0| < ε specialize hV n (le_of_max_le_right hn) -- hV : |v n - 0| < 1 rw [sub_zero] at * -- hU : |u n - 0| < ε -- hV : |v n - 0| < 1 -- ⊢ |(u * v) n - 0| < ε calc |(u * v) n| = |u n * v n| := rfl _ = |u n| * |v n| := abs_mul (u n) (v n) _ < ε * 1 := mul_lt_mul'' hU hV (abs_nonneg (u n)) (abs_nonneg (v n)) _ = ε := mul_one ε -- 2ª demostración -- =============== example (hu : limite u 0) (hv : limite v 0) : limite (u * v) 0 := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε cases' hu ε hε with U hU -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - 0| < ε cases' hv 1 (by linarith) with V hV -- V : ℕ -- hV : ∀ (n : ℕ), n ≥ V → |v n - 0| < 1 let N := max U V use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε intros n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |(u * v) n - 0| < ε specialize hU n (le_of_max_le_left hn) -- hU : |u n - 0| < ε specialize hV n (le_of_max_le_right hn) -- hV : |v n - 0| < 1 rw [sub_zero] at * -- hU : |u n| < ε -- hV : |v n| < 1 -- ⊢ |(u * v) n| < ε calc |(u * v) n| = |u n * v n| := rfl _ = |u n| * |v n| := abs_mul (u n) (v n) _ < ε * 1 := by { apply mul_lt_mul'' hU hV <;> simp [abs_nonneg] } _ = ε := mul_one ε -- 3ª demostración -- =============== example (hu : limite u 0) (hv : limite v 0) : limite (u * v) 0 := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε cases' hu ε hε with U hU -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - 0| < ε cases' hv 1 (by linarith) with V hV -- V : ℕ -- hV : ∀ (n : ℕ), n ≥ V → |v n - 0| < 1 let N := max U V use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε intros n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |(u * v) n - 0| < ε have hUN : U ≤ N := le_max_left U V have hVN : V ≤ N := le_max_right U V specialize hU n (by linarith) -- hU : |u n - 0| < ε specialize hV n (by linarith) -- hV : |v n - 0| < 1 rw [sub_zero] at * -- hU : |u n| < ε -- hV : |v n| < 1 -- ⊢ |(u * v) n| < ε rw [Pi.mul_apply] -- ⊢ |u n * v n| < ε rw [abs_mul] -- ⊢ |u n| * |v n| < ε convert mul_lt_mul'' hU hV _ _ using 2 <;> simp -- Lemas usados -- ============ -- variable (a b c d : ℝ) -- variable (I : Type _) -- variable (f : I → Type _) -- #check (zero_lt_one : 0 < 1) -- #check (le_of_max_le_left : max a b ≤ c → a ≤ c) -- #check (le_of_max_le_right : max a b ≤ c → b ≤ c) -- #check (sub_zero a : a - 0 = a) -- #check (abs_mul a b : |a * b| = |a| * |b|) -- #check (mul_lt_mul'' : a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d) -- #check (abs_nonneg a : 0 ≤ |a|) -- #check (mul_one a : a * 1 = a) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
6.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 |
theory Producto_de_sucesiones_convergentes_a_cero imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" lemma assumes "limite u 0" "limite v 0" shows "limite (λ n. u n * v n) 0" proof (unfold limite_def; intro allI impI) fix ε :: real assume hε : "0 < ε" then obtain U where hU : "∀n≥U. ¦u n - 0¦ < ε" using assms(1) limite_def by auto obtain V where hV : "∀n≥V. ¦v n - 0¦ < 1" using hε assms(2) limite_def by fastforce have "∀n≥max U V. ¦u n * v n - 0¦ < ε" proof (intro allI impI) fix n assume hn : "max U V ≤ n" then have "U ≤ n" by simp then have "¦u n - 0¦ < ε" using hU by blast have hnV : "V ≤ n" using hn by simp then have "¦v n - 0¦ < 1" using hV by blast have "¦u n * v n - 0¦ = ¦(u n - 0) * (v n - 0)¦" by simp also have "… = ¦u n - 0¦ * ¦v n - 0¦" by (simp add: abs_mult) also have "… < ε * 1" using ‹¦u n - 0¦ < ε› ‹¦v n - 0¦ < 1› by (rule abs_mult_less) also have "… = ε" by simp finally show "¦u n * v n - 0¦ < ε" by this qed then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε" by (rule exI) qed end |
7. Teorema del emparedado
Demostrar con Lean4 el teorema del emparedado.
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 (u v w : ℕ → ℝ) variable (a : ℝ) def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε example (hu : limite u a) (hw : limite w a) (h1 : ∀ n, u n ≤ v n) (h2 : ∀ n, v n ≤ w n) : limite v a := by sorry |
7.1. Demostración en lenguaje natural
Tenemos que demostrar que para cada \(ε > 0\), existe un \(N ∈ ℕ\) tal que
\[ (∀ n ≥ N)[|v(n) – a| ≤ ε] \tag{1} \]
Puesto que el límite de \(u\) es \(a\), existe un \(U ∈ ℕ\) tal que
\[ (∀ n ≥ U)[|u(n) – a| ≤ ε] \tag{2} \]
y, puesto que el límite de \(w\) es \(a\), existe un \(W ∈ ℕ\) tal que
\[ (∀ n ≥ W)[|w(n) – a| ≤ ε] \tag{3} \]
Sea \(N = \text{máx}(U, W)\). Veamos que se verifica (1). Para ello, sea \(n ≥ N\). Entonces, \(n ≥ U\), \(n ≥ W\) y, por (2) y (3), se tiene que
\begin{align}
|u(n) – a| &≤ ε \tag{4} \\
|w(n) – a| &≤ ε \tag{5}
\end{align}
Para demostrar que
\[ |v(n) – a| ≤ ε \]
basta demostrar las siguientes desigualdades
\begin{align}
&-ε ≤ v(n) – a \tag{6} \\
&v(n) – a ≤ ε \tag{7}
\end{align}
La demostración de (6) es
\begin{align}
-ε &≤ u(n) – a &&\text{[por (4)]} \\
&≤ v(n) – a &&\text{[por hipótesis]}
\end{align}
La demostración de (7) es
\begin{align}
v(n) – a &≤ w(n) – a &&\text{[por hipótesis]} \\
&≤ ε &&\text{[por (5)]}
\end{align}
7.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 145 146 |
import Mathlib.Data.Real.Basic variable (u v w : ℕ → ℝ) variable (a : ℝ) def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε -- Nota. En la demostración se usará el siguiente lema: lemma max_ge_iff {p q r : ℕ} : r ≥ max p q ↔ r ≥ p ∧ r ≥ q := max_le_iff -- 1ª demostración -- =============== example (hu : limite u a) (hw : limite w a) (h1 : ∀ n, u n ≤ v n) (h2 : ∀ n, v n ≤ w n) : limite v a := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v n - a| ≤ ε rcases hu ε hε with ⟨U, hU⟩ -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - a| ≤ ε clear hu rcases hw ε hε with ⟨W, hW⟩ -- W : ℕ -- hW : ∀ (n : ℕ), n ≥ W → |w n - a| ≤ ε clear hw hε use max U W intros n hn -- n : ℕ -- hn : n ≥ max U W -- ⊢ |v n - a| ≤ ε rw [max_ge_iff] at hn -- hn : n ≥ U ∧ n ≥ W specialize hU n hn.1 -- hU : |u n - a| ≤ ε specialize hW n hn.2 -- hW : |w n - a| ≤ ε specialize h1 n -- h1 : u n ≤ v n specialize h2 n -- h2 : v n ≤ w n clear hn rw [abs_le] at * -- ⊢ -ε ≤ v n - a ∧ v n - a ≤ ε constructor . -- ⊢ -ε ≤ v n - a calc -ε ≤ u n - a := hU.1 _ ≤ v n - a := by linarith . -- ⊢ v n - a ≤ ε calc v n - a ≤ w n - a := by linarith _ ≤ ε := hW.2 -- 2ª demostración example (hu : limite u a) (hw : limite w a) (h1 : ∀ n, u n ≤ v n) (h2 : ∀ n, v n ≤ w n) : limite v a := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v n - a| ≤ ε rcases hu ε hε with ⟨U, hU⟩ -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - a| ≤ ε clear hu rcases hw ε hε with ⟨W, hW⟩ -- W : ℕ -- hW : ∀ (n : ℕ), n ≥ W → |w n - a| ≤ ε clear hw hε use max U W intros n hn -- n : ℕ -- hn : n ≥ max U W rw [max_ge_iff] at hn -- hn : n ≥ U ∧ n ≥ W specialize hU n (by linarith) -- hU : |u n - a| ≤ ε specialize hW n (by linarith) -- hW : |w n - a| ≤ ε specialize h1 n -- h1 : u n ≤ v n specialize h2 n -- h2 : v n ≤ w n rw [abs_le] at * -- ⊢ -ε ≤ v n - a ∧ v n - a ≤ ε constructor . -- ⊢ -ε ≤ v n - a linarith . -- ⊢ v n - a ≤ ε linarith -- 3ª demostración example (hu : limite u a) (hw : limite w a) (h1 : ∀ n, u n ≤ v n) (h2 : ∀ n, v n ≤ w n) : limite v a := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v n - a| ≤ ε rcases hu ε hε with ⟨U, hU⟩ -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - a| ≤ ε clear hu rcases hw ε hε with ⟨W, hW⟩ -- W : ℕ -- hW : ∀ (n : ℕ), n ≥ W → |w n - a| ≤ ε clear hw hε use max U W intros n hn -- n : ℕ -- hn : n ≥ max U W -- ⊢ |v n - a| ≤ ε rw [max_ge_iff] at hn -- hn : n ≥ U ∧ n ≥ W specialize hU n (by linarith) -- hU : |u n - a| ≤ ε specialize hW n (by linarith) -- hW : |w n - a| ≤ ε specialize h1 n -- h1 : u n ≤ v n specialize h2 n -- h2 : v n ≤ w n rw [abs_le] at * -- hU : -ε ≤ u n - a ∧ u n - a ≤ ε -- hW : -ε ≤ w n - a ∧ w n - a ≤ ε -- ⊢ -ε ≤ v n - a ∧ v n - a ≤ ε constructor <;> linarith |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
7.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 |
theory Teorema_del_emparedado imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" lemma assumes "limite u a" "limite w a" "∀n. u n ≤ v n" "∀n. v n ≤ w n" shows "limite v a" proof (unfold limite_def; intro allI impI) fix ε :: real assume hε : "0 < ε" obtain N where hN : "∀n≥N. ¦u n - a¦ < ε" using assms(1) hε limite_def by auto obtain N' where hN' : "∀n≥N'. ¦w n - a¦ < ε" using assms(2) hε limite_def by auto have "∀n≥max N N'. ¦v n - a¦ < ε" proof (intro allI impI) fix n assume hn : "n≥max N N'" have "v n - a < ε" proof - have "v n - a ≤ w n - a" using assms(4) by simp also have "… ≤ ¦w n - a¦" by simp also have "… < ε" using hN' hn by auto finally show "v n - a < ε" . qed moreover have "-(v n - a) < ε" proof - have "-(v n - a) ≤ -(u n - a)" using assms(3) by auto also have "… ≤ ¦u n - a¦" by simp also have "… < ε" using hN hn by auto finally show "-(v n - a) < ε" . qed ultimately show "¦v n - a¦ < ε" by (simp only: abs_less_iff) qed then show "∃k. ∀n≥k. ¦v n - a¦ < ε" by (rule exI) qed end |
8. Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u
Demostrar con Lean4 que “Si \(s ⊆ t\), entonces \(s ∩ u ⊆ t ∩ u\)”.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α : Type} variable (s t u : Set α) example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by sorry |
8.1. Demostración en lenguaje natural
Sea \(x ∈ s ∩ u\). Entonces, se tiene que
\begin{align}
&x ∈ s \tag{1} \\
&x ∈ u \tag{2}
\end{align}
De (1) y \(s ⊆ t\), se tiene que
\[ x ∈ t \tag{3} \]
De (3) y (2) se tiene que
\[ x ∈ t ∩ u \]
que es lo que teníamos que demostrar.
8.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 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α : Type} variable (s t u : Set α) -- 1ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by rw [subset_def] -- ⊢ ∀ (x : α), x ∈ s ∩ u → x ∈ t ∩ u intros x h1 -- x : α -- h1 : x ∈ s ∩ u -- ⊢ x ∈ t ∩ u rcases h1 with ⟨xs, xu⟩ -- xs : x ∈ s -- xu : x ∈ u constructor . -- ⊢ x ∈ t rw [subset_def] at h -- h : ∀ (x : α), x ∈ s → x ∈ t apply h -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ u exact xu -- 2ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by rw [subset_def] -- ⊢ ∀ (x : α), x ∈ s ∩ u → x ∈ t ∩ u rintro x ⟨xs, xu⟩ -- x : α -- xs : x ∈ s -- xu : x ∈ u rw [subset_def] at h -- h : ∀ (x : α), x ∈ s → x ∈ t exact ⟨h x xs, xu⟩ -- 3ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by simp only [subset_def] -- ⊢ ∀ (x : α), x ∈ s ∩ u → x ∈ t ∩ u rintro x ⟨xs, xu⟩ -- x : α -- xs : x ∈ s -- xu : x ∈ u rw [subset_def] at h -- h : ∀ (x : α), x ∈ s → x ∈ t exact ⟨h _ xs, xu⟩ -- 4ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by intros x xsu -- x : α -- xsu : x ∈ s ∩ u -- ⊢ x ∈ t ∩ u exact ⟨h xsu.1, xsu.2⟩ -- 5ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by rintro x ⟨xs, xu⟩ -- xs : x ∈ s -- xu : x ∈ u -- ⊢ x ∈ t ∩ u exact ⟨h xs, xu⟩ -- 6ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := fun _ ⟨xs, xu⟩ ↦ ⟨h xs, xu⟩ -- 7ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := inter_subset_inter_left u h -- Lema usado -- ========== -- #check (inter_subset_inter_left u : s ⊆ t → s ∩ u ⊆ t ∩ u) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
8.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 |
theory Propiedad_de_monotonia_de_la_interseccion imports Main begin (* 1ª solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" proof (rule subsetI) fix x assume hx: "x ∈ s ∩ u" have xs: "x ∈ s" using hx by (simp only: IntD1) then have xt: "x ∈ t" using assms by (simp only: subset_eq) have xu: "x ∈ u" using hx by (simp only: IntD2) show "x ∈ t ∩ u" using xt xu by (simp only: Int_iff) qed (* 2 solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" proof fix x assume hx: "x ∈ s ∩ u" have xs: "x ∈ s" using hx by simp then have xt: "x ∈ t" using assms by auto have xu: "x ∈ u" using hx by simp show "x ∈ t ∩ u" using xt xu by simp qed (* 3ª solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" using assms by auto (* 4ª solución *) lemma "s ⊆ t ⟹ s ∩ u ⊆ t ∩ u" by auto end |
9. s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)
Demostrar con Lean4 que \(s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α : Type} variable (s t u : Set α) example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := by sorry |
9.1. Demostración en lenguaje natural
Sea \(x ∈ s ∩ (t ∪ u)\). Entonces se tiene que
\begin{align}
&x ∈ s \tag{1} \\
&x ∈ t ∪ u \tag{2}
\end{align}
La relación (2) da lugar a dos casos.
Caso 1: Supongamos que \(x ∈ t\). Entonces, por (1), \(x ∈ s ∩ t\) y, por tanto, \(x ∈ (s ∩ t) ∪ (s ∩ u)\).
Caso 2: Supongamos que \(x ∈ u\). Entonces, por (1), \(x ∈ s ∩ u\) y, por tanto, \(x ∈ (s ∩ t) ∪ (s ∩ u)\).
9.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 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α : Type} variable (s t u : Set α) -- 1ª demostración -- =============== example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := by intros x hx -- x : α -- hx : x ∈ s ∩ (t ∪ u) -- ⊢ x ∈ s ∩ t ∪ s ∩ u rcases hx with ⟨hxs, hxtu⟩ -- hxs : x ∈ s -- hxtu : x ∈ t ∪ u rcases hxtu with (hxt | hxu) . -- hxt : x ∈ t left -- ⊢ x ∈ s ∩ t constructor . -- ⊢ x ∈ s exact hxs . -- hxt : x ∈ t exact hxt . -- hxu : x ∈ u right -- ⊢ x ∈ s ∩ u constructor . -- ⊢ x ∈ s exact hxs . -- ⊢ x ∈ u exact hxu -- 2ª demostración -- =============== example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := by rintro x ⟨hxs, hxt | hxu⟩ -- x : α -- hxs : x ∈ s -- ⊢ x ∈ s ∩ t ∪ s ∩ u . -- hxt : x ∈ t left -- ⊢ x ∈ s ∩ t exact ⟨hxs, hxt⟩ . -- hxu : x ∈ u right -- ⊢ x ∈ s ∩ u exact ⟨hxs, hxu⟩ -- 3ª demostración -- =============== example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := by rintro x ⟨hxs, hxt | hxu⟩ -- x : α -- hxs : x ∈ s -- ⊢ x ∈ s ∩ t ∪ s ∩ u . -- hxt : x ∈ t exact Or.inl ⟨hxs, hxt⟩ . -- hxu : x ∈ u exact Or.inr ⟨hxs, hxu⟩ -- 4ª demostración -- =============== example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := by intro x hx -- x : α -- hx : x ∈ s ∩ (t ∪ u) -- ⊢ x ∈ s ∩ t ∪ s ∩ u aesop -- 5ª demostración -- =============== example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := by rw [inter_union_distrib_left] |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
9.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 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 |
theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union imports Main begin (* 1ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" proof (rule subsetI) fix x assume hx : "x ∈ s ∩ (t ∪ u)" then have xs : "x ∈ s" by (simp only: IntD1) have xtu: "x ∈ t ∪ u" using hx by (simp only: IntD2) then have "x ∈ t ∨ x ∈ u" by (simp only: Un_iff) then show " x ∈ s ∩ t ∪ s ∩ u" proof (rule disjE) assume xt : "x ∈ t" have xst : "x ∈ s ∩ t" using xs xt by (simp only: Int_iff) then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by (simp only: UnI1) next assume xu : "x ∈ u" have xst : "x ∈ s ∩ u" using xs xu by (simp only: Int_iff) then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by (simp only: UnI2) qed qed (* 2ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" proof fix x assume hx : "x ∈ s ∩ (t ∪ u)" then have xs : "x ∈ s" by simp have xtu: "x ∈ t ∪ u" using hx by simp then have "x ∈ t ∨ x ∈ u" by simp then show " x ∈ s ∩ t ∪ s ∩ u" proof assume xt : "x ∈ t" have xst : "x ∈ s ∩ t" using xs xt by simp then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by simp next assume xu : "x ∈ u" have xst : "x ∈ s ∩ u" using xs xu by simp then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by simp qed qed (* 3ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" proof (rule subsetI) fix x assume hx : "x ∈ s ∩ (t ∪ u)" then have xs : "x ∈ s" by (simp only: IntD1) have xtu: "x ∈ t ∪ u" using hx by (simp only: IntD2) then show " x ∈ s ∩ t ∪ s ∩ u" proof (rule UnE) assume xt : "x ∈ t" have xst : "x ∈ s ∩ t" using xs xt by (simp only: Int_iff) then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by (simp only: UnI1) next assume xu : "x ∈ u" have xst : "x ∈ s ∩ u" using xs xu by (simp only: Int_iff) then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by (simp only: UnI2) qed qed (* 4ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" proof fix x assume hx : "x ∈ s ∩ (t ∪ u)" then have xs : "x ∈ s" by simp have xtu: "x ∈ t ∪ u" using hx by simp then show " x ∈ s ∩ t ∪ s ∩ u" proof (rule UnE) assume xt : "x ∈ t" have xst : "x ∈ s ∩ t" using xs xt by simp then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by simp next assume xu : "x ∈ u" have xst : "x ∈ s ∩ u" using xs xu by simp then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by simp qed qed (* 5ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" by (simp only: Int_Un_distrib) (* 6ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" by auto end |
10. (s \ t) \ u ⊆ s \ (t ∪ u)
Demostrar con Lean4 que
\[ (s \setminus t) \setminus u ⊆ s \setminus (t ∪ u) \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t u : Set α) example : (s \ t) \ u ⊆ s \ (t ∪ u) := by sorry |
10.1. Demostración en lenguaje natural
Sea \(x ∈ (s \setminus t) \setminus u\). Entonces, se tiene que
\begin{align}
&x ∈ s \tag{1} \\
&x ∉ t \tag{2} \\
&x ∉ u \tag{3}
\end{align}
Tenemos que demostrar que
\[ x ∈ s \setminus (t ∪ u) \]
pero, por (1), se reduce a
\[ x ∉ t ∪ u \]
que se verifica por (2) y (3).
10.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 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t u : Set α) -- 1ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by intros x hx -- x : α -- hx : x ∈ (s \ t) \ u -- ⊢ x ∈ s \ (t ∪ u) rcases hx with ⟨hxst, hxnu⟩ -- hxst : x ∈ s \ t -- hxnu : ¬x ∈ u rcases hxst with ⟨hxs, hxnt⟩ -- hxs : x ∈ s -- hxnt : ¬x ∈ t constructor . -- ⊢ x ∈ s exact hxs . -- ⊢ ¬x ∈ t ∪ u by_contra hxtu -- hxtu : x ∈ t ∪ u -- ⊢ False rcases hxtu with (hxt | hxu) . -- hxt : x ∈ t apply hxnt -- ⊢ x ∈ t exact hxt . -- hxu : x ∈ u apply hxnu -- ⊢ x ∈ u exact hxu -- 2ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by rintro x ⟨⟨hxs, hxnt⟩, hxnu⟩ -- x : α -- hxnu : ¬x ∈ u -- hxs : x ∈ s -- hxnt : ¬x ∈ t -- ⊢ x ∈ s \ (t ∪ u) constructor . -- ⊢ x ∈ s exact hxs . -- ⊢ ¬x ∈ t ∪ u by_contra hxtu -- hxtu : x ∈ t ∪ u -- ⊢ False rcases hxtu with (hxt | hxu) . -- hxt : x ∈ t exact hxnt hxt . -- hxu : x ∈ u exact hxnu hxu -- 3ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by rintro x ⟨⟨xs, xnt⟩, xnu⟩ -- x : α -- xnu : ¬x ∈ u -- xs : x ∈ s -- xnt : ¬x ∈ t -- ⊢ x ∈ s \ (t ∪ u) use xs -- ⊢ ¬x ∈ t ∪ u rintro (xt | xu) . -- xt : x ∈ t -- ⊢ False contradiction . -- xu : x ∈ u -- ⊢ False contradiction -- 4ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by rintro x ⟨⟨xs, xnt⟩, xnu⟩ -- x : α -- xnu : ¬x ∈ u -- xs : x ∈ s -- xnt : ¬x ∈ t -- ⊢ x ∈ s \ (t ∪ u) use xs -- ⊢ ¬x ∈ t ∪ u rintro (xt | xu) <;> contradiction -- 5ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by intro x xstu -- x : α -- xstu : x ∈ (s \ t) \ u -- ⊢ x ∈ s \ (t ∪ u) simp at * -- ⊢ x ∈ s ∧ ¬(x ∈ t ∨ x ∈ u) aesop -- 6ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by intro x xstu -- x : α -- xstu : x ∈ (s \ t) \ u -- ⊢ x ∈ s \ (t ∪ u) aesop -- 7ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by rw [diff_diff] -- Lema usado -- ========== -- #check (diff_diff : (s \ t) \ u = s \ (t ∪ u)) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
10.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 |
theory Diferencia_de_diferencia_de_conjuntos imports Main begin |