La semana en Calculemus (4 de mayo de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Imagen de la interseccion general mediante aplicaciones inyectivas
- 2. Imagen inversa de la unión general
- 3. Imagen inversa de la intersección general
- 4. Teorema de Cantor
- 5. En los monoides, los inversos a la izquierda y a la derecha son iguales
A continuación se muestran las soluciones.
1. Imagen de la interseccion general mediante aplicaciones inyectivas
Demostrar con Lean4 que si \(f\) es inyectiva, entonces
\[⋂ᵢf[Aᵢ] ⊆ f\left[⋂ᵢAᵢ\right] \]
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.Set.Basic import Mathlib.Tactic open Set Function variable {α β I : Type _} variable (f : α → β) variable (A : I → Set α) example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) := by sorry |
1.1. Demostración en lenguaje natural
Sea \(y ∈ ⋂ᵢf[Aᵢ]\). Entonces,
\begin{align}
& (∀i ∈ I)y ∈ f[Aᵢ] \tag{1} \\
& y ∈ f[Aᵢ]
\end{align}
Por tanto, existe un \(x ∈ Aᵢ\) tal que
\[ f(x) = y \tag{2} \]
Veamos que \(x ∈ ⋂ᵢAᵢ\). Para ello, sea \(j ∈ I\). Por (1),
\[ y ∈ f[Aⱼ] \]
Luego, existe un \(z\) tal que
\begin{align}
&z ∈ Aⱼ \tag{3} \\
&f(z) = y
\end{align}
Pot (2),
\[ f(x) = f(z) \]
y, por ser \(f\) inyectiva,
\[ x = z \]
y, por (3),
\[ x ∈ Aⱼ \]
Puesto que \(x ∈ ⋂ᵢAᵢ\) se tiene que \(f(x) ∈ f\left[⋂ᵢAᵢ\right]\) y, por (2), \(y ∈ f\left[⋂ᵢAᵢ\right]\).
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 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set Function variable {α β I : Type _} variable (f : α → β) variable (A : I → Set α) -- 1ª demostración -- =============== example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) := by intros y hy -- y : β -- hy : y ∈ ⋂ (i : I), f '' A i -- ⊢ y ∈ f '' ⋂ (i : I), A i have h1 : ∀ (i : I), y ∈ f '' A i := mem_iInter.mp hy have h2 : y ∈ f '' A i := h1 i obtain ⟨x : α, h3 : x ∈ A i ∧ f x = y⟩ := h2 have h4 : f x = y := h3.2 have h5 : ∀ i : I, x ∈ A i := by intro j have h5a : y ∈ f '' A j := h1 j obtain ⟨z : α, h5b : z ∈ A j ∧ f z = y⟩ := h5a have h5c : z ∈ A j := h5b.1 have h5d : f z = y := h5b.2 have h5e : f z = f x := by rwa [←h4] at h5d have h5f : z = x := injf h5e show x ∈ A j rwa [h5f] at h5c have h6 : x ∈ ⋂ i, A i := mem_iInter.mpr h5 have h7 : f x ∈ f '' (⋂ i, A i) := mem_image_of_mem f h6 show y ∈ f '' (⋂ i, A i) rwa [h4] at h7 -- 2ª demostración -- =============== example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) := by intros y hy -- y : β -- hy : y ∈ ⋂ (i : I), f '' A i -- ⊢ y ∈ f '' ⋂ (i : I), A i rw [mem_iInter] at hy -- hy : ∀ (i : I), y ∈ f '' A i rcases hy i with ⟨x, -, fxy⟩ -- x : α -- fxy : f x = y use x -- ⊢ x ∈ ⋂ (i : I), A i ∧ f x = y constructor . -- ⊢ x ∈ ⋂ (i : I), A i apply mem_iInter_of_mem -- ⊢ ∀ (i : I), x ∈ A i intro j -- j : I -- ⊢ x ∈ A j rcases hy j with ⟨z, zAj, fzy⟩ -- z : α -- zAj : z ∈ A j -- fzy : f z = y convert zAj -- ⊢ x = z apply injf -- ⊢ f x = f z rw [fxy] -- ⊢ y = f z rw [←fzy] . -- ⊢ f x = y exact fxy -- 3ª demostración -- =============== example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) := by intro y -- y : β -- ⊢ y ∈ ⋂ (i : I), f '' A i → y ∈ f '' ⋂ (i : I), A i simp -- ⊢ (∀ (i : I), ∃ x, x ∈ A i ∧ f x = y) → ∃ x, (∀ (i : I), x ∈ A i) ∧ f x = y intro h -- h : ∀ (i : I), ∃ x, x ∈ A i ∧ f x = y -- ⊢ ∃ x, (∀ (i : I), x ∈ A i) ∧ f x = y rcases h i with ⟨x, -, fxy⟩ -- x : α -- fxy : f x = y use x -- ⊢ (∀ (i : I), x ∈ A i) ∧ f x = y constructor . -- ⊢ ∀ (i : I), x ∈ A i intro j -- j : I -- ⊢ x ∈ A j rcases h j with ⟨z, zAi, fzy⟩ -- z : α -- zAi : z ∈ A j -- fzy : f z = y have : f x = f z := by rw [fxy, fzy] -- this : f x = f z have : x = z := injf this -- this : x = z rw [this] -- ⊢ z ∈ A j exact zAi . -- ⊢ f x = y exact fxy -- Lemas usados -- ============ -- variable (x : α) -- variable (s : Set α) -- #check (mem_iInter : x ∈ ⋂ i, A i ↔ ∀ i, x ∈ A i) -- #check (mem_iInter_of_mem : (∀ i, x ∈ A i) → x ∈ ⋂ i, A i) -- #check (mem_image_of_mem f : x ∈ s → f x ∈ f '' s) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
1.3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 |
theory Imagen_de_la_interseccion_general_mediante_inyectiva imports Main begin (* 1ª demostración *) lemma assumes "i ∈ I" "inj f" shows "(⋂ i ∈ I. f ` A i) ⊆ f ` (⋂ i ∈ I. A i)" proof (rule subsetI) fix y assume "y ∈ (⋂ i ∈ I. f ` A i)" then have "y ∈ f ` A i" using ‹i ∈ I› by (rule INT_D) then show "y ∈ f ` (⋂ i ∈ I. A i)" proof (rule imageE) fix x assume "y = f x" assume "x ∈ A i" have "x ∈ (⋂ i ∈ I. A i)" proof (rule INT_I) fix j assume "j ∈ I" show "x ∈ A j" proof - have "y ∈ f ` A j" using ‹y ∈ (⋂i∈I. f ` A i)› ‹j ∈ I› by (rule INT_D) then show "x ∈ A j" proof (rule imageE) fix z assume "y = f z" assume "z ∈ A j" have "f z = f x" using ‹y = f z› ‹y = f x› by (rule subst) with ‹inj f› have "z = x" by (rule injD) then show "x ∈ A j" using ‹z ∈ A j› by (rule subst) qed qed qed then have "f x ∈ f ` (⋂ i ∈ I. A i)" by (rule imageI) with ‹y = f x› show "y ∈ f ` (⋂ i ∈ I. A i)" by (rule ssubst) qed qed (* 2ª demostración *) lemma assumes "i ∈ I" "inj f" shows "(⋂ i ∈ I. f ` A i) ⊆ f ` (⋂ i ∈ I. A i)" proof fix y assume "y ∈ (⋂ i ∈ I. f ` A i)" then have "y ∈ f ` A i" using ‹i ∈ I› by simp then show "y ∈ f ` (⋂ i ∈ I. A i)" proof fix x assume "y = f x" assume "x ∈ A i" have "x ∈ (⋂ i ∈ I. A i)" proof fix j assume "j ∈ I" show "x ∈ A j" proof - have "y ∈ f ` A j" using ‹y ∈ (⋂i∈I. f ` A i)› ‹j ∈ I› by simp then show "x ∈ A j" proof fix z assume "y = f z" assume "z ∈ A j" have "f z = f x" using ‹y = f z› ‹y = f x› by simp with ‹inj f› have "z = x" by (rule injD) then show "x ∈ A j" using ‹z ∈ A j› by simp qed qed qed then have "f x ∈ f ` (⋂ i ∈ I. A i)" by simp with ‹y = f x› show "y ∈ f ` (⋂ i ∈ I. A i)" by simp qed qed (* 3ª demostración *) lemma assumes "i ∈ I" "inj f" shows "(⋂ i ∈ I. f ` A i) ⊆ f ` (⋂ i ∈ I. A i)" using assms by (simp add: image_INT) end |
2. Imagen inversa de la unión general
Demostrar con Lean4 que
\[ f⁻¹\left[⋃ᵢ Bᵢ\right] = ⋃ᵢ f⁻¹[Bᵢ] \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α β I : Type _} variable (f : α → β) variable (B : I → Set β) example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) := by sorry |
2.1. Demostración en lenguaje natural
Tenemos que demostrar que, para todo \(x\),
\[ x ∈ f⁻¹\left[⋃ᵢ Bᵢ\right] ↔ x ∈ ⋃ᵢ f⁻¹[Bᵢ] \]
y lo haremos demostrando las dos implicaciones.
(⟹) Supongamos que \(x ∈ f⁻¹\left[⋃ᵢ Bᵢ\right]\). Entonces, por la definición de la imagen inversa,
\[ f(x) ∈ ⋃ᵢ Bᵢ \]
y, por la definición de la unión, existe un \(i\) tal que
\[ f(x) ∈ Bᵢ \]
y, por la definición de la imagen inversa,
\[ x ∈ f⁻¹[Bᵢ] \]
y, por la definición de la unión,
\[ x ∈ ⋃ᵢ f⁻¹[Bᵢ] \]
(⟸) Supongamos que \(x ∈ ⋃ᵢ f⁻¹[Bᵢ]\). Entonces, por la definición de la unión, existe un \(i\) tal que
\[ x ∈ f⁻¹[Bᵢ] \]
y, por la definición de la imagen inversa,
\[ f(x) ∈ Bᵢ \]
y, por la definición de la unión,
\[ f(x) ∈ ⋃ᵢ Bᵢ \]
y, por la definición de la imagen inversa,
\[ x ∈ f⁻¹\left[⋃ᵢ Bᵢ\right] \]
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 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α β I : Type _} variable (f : α → β) variable (B : I → Set β) -- 1ª demostración -- =============== example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) := by ext x -- x : α -- ⊢ x ∈ f ⁻¹' ⋃ (i : I), B i ↔ x ∈ ⋃ (i : I), f ⁻¹' B i constructor . -- ⊢ x ∈ f ⁻¹' ⋃ (i : I), B i → x ∈ ⋃ (i : I), f ⁻¹' B i intro hx -- hx : x ∈ f ⁻¹' ⋃ (i : I), B i -- ⊢ x ∈ ⋃ (i : I), f ⁻¹' B i rw [mem_preimage] at hx -- hx : f x ∈ ⋃ (i : I), B i rw [mem_iUnion] at hx -- hx : ∃ i, f x ∈ B i cases' hx with i fxBi -- i : I -- fxBi : f x ∈ B i rw [mem_iUnion] -- ⊢ ∃ i, x ∈ f ⁻¹' B i use i -- ⊢ x ∈ f ⁻¹' B i apply mem_preimage.mpr -- ⊢ f x ∈ B i exact fxBi . -- ⊢ x ∈ ⋃ (i : I), f ⁻¹' B i → x ∈ f ⁻¹' ⋃ (i : I), B i intro hx -- hx : x ∈ ⋃ (i : I), f ⁻¹' B i -- ⊢ x ∈ f ⁻¹' ⋃ (i : I), B i rw [mem_preimage] -- ⊢ f x ∈ ⋃ (i : I), B i rw [mem_iUnion] -- ⊢ ∃ i, f x ∈ B i rw [mem_iUnion] at hx -- hx : ∃ i, x ∈ f ⁻¹' B i cases' hx with i xBi -- i : I -- xBi : x ∈ f ⁻¹' B i use i -- ⊢ f x ∈ B i rw [mem_preimage] at xBi -- xBi : f x ∈ B i exact xBi -- 2ª demostración -- =============== example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) := preimage_iUnion -- 3ª demostración -- =============== example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) := by simp -- Lemas usados -- ============ -- variable (x : α) -- variable (s : Set β) -- variable (A : I → Set α) -- #check (mem_iUnion : x ∈ ⋃ i, A i ↔ ∃ i, x ∈ A i) -- #check (mem_preimage : x ∈ f ⁻¹' s ↔ f x ∈ s) -- #check (preimage_iUnion : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i)) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
2.3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 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 |
theory Imagen_inversa_de_la_union_general imports Main begin (* 1ª demostración *) lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)" proof (rule equalityI) show "f -` (⋃ i ∈ I. B i) ⊆ (⋃ i ∈ I. f -` B i)" proof (rule subsetI) fix x assume "x ∈ f -` (⋃ i ∈ I. B i)" then have "f x ∈ (⋃ i ∈ I. B i)" by (rule vimageD) then show "x ∈ (⋃ i ∈ I. f -` B i)" proof (rule UN_E) fix i assume "i ∈ I" assume "f x ∈ B i" then have "x ∈ f -` B i" by (rule vimageI2) with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. f -` B i)" by (rule UN_I) qed qed next show "(⋃ i ∈ I. f -` B i) ⊆ f -` (⋃ i ∈ I. B i)" proof (rule subsetI) fix x assume "x ∈ (⋃ i ∈ I. f -` B i)" then show "x ∈ f -` (⋃ i ∈ I. B i)" proof (rule UN_E) fix i assume "i ∈ I" assume "x ∈ f -` B i" then have "f x ∈ B i" by (rule vimageD) with ‹i ∈ I› have "f x ∈ (⋃ i ∈ I. B i)" by (rule UN_I) then show "x ∈ f -` (⋃ i ∈ I. B i)" by (rule vimageI2) qed qed qed (* 2ª demostración *) lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)" proof show "f -` (⋃ i ∈ I. B i) ⊆ (⋃ i ∈ I. f -` B i)" proof fix x assume "x ∈ f -` (⋃ i ∈ I. B i)" then have "f x ∈ (⋃ i ∈ I. B i)" by simp then show "x ∈ (⋃ i ∈ I. f -` B i)" proof fix i assume "i ∈ I" assume "f x ∈ B i" then have "x ∈ f -` B i" by simp with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. f -` B i)" by (rule UN_I) qed qed next show "(⋃ i ∈ I. f -` B i) ⊆ f -` (⋃ i ∈ I. B i)" proof fix x assume "x ∈ (⋃ i ∈ I. f -` B i)" then show "x ∈ f -` (⋃ i ∈ I. B i)" proof fix i assume "i ∈ I" assume "x ∈ f -` B i" then have "f x ∈ B i" by simp with ‹i ∈ I› have "f x ∈ (⋃ i ∈ I. B i)" by (rule UN_I) then show "x ∈ f -` (⋃ i ∈ I. B i)" by simp qed qed qed (* 3ª demostración *) lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)" by (simp only: vimage_UN) (* 4ª demostración *) lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)" by auto end |
3. Imagen inversa de la intersección general
Demostrar con Lean4 que
\[ f⁻¹\left[\bigcap_{i \in I} B_i\right] = \bigcap_{i \in I} f⁻¹[B_i] \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α β I : Type _} variable (f : α → β) variable (B : I → Set β) example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) := by sorry |
3.1. Demostración en lenguaje natural
Se demuestra mediante la siguiente cadena de equivalencias
\begin{align}
x ∈ f⁻¹\left[\bigcap_{i \in I} B_i\right]
&↔ f(x) ∈ \bigcap_{i \in I} B_i \\
&↔ (∀ i) f(x) ∈ B_i \\
&↔ (∀ i) x ∈ f⁻¹[B_i] \\
&↔ x ∈ \bigcap_{i \in I} f⁻¹[B_i]
\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 79 80 81 82 83 84 85 86 87 88 89 90 91 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α β I : Type _} variable (f : α → β) variable (B : I → Set β) -- 1ª demostración -- =============== example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) := by ext x -- x : α -- ⊢ x ∈ f ⁻¹' ⋂ (i : I), B i ↔ x ∈ ⋂ (i : I), f ⁻¹' B i calc (x ∈ f ⁻¹' ⋂ i, B i) ↔ f x ∈ ⋂ i, B i := mem_preimage _ ↔ (∀ i, f x ∈ B i) := mem_iInter _ ↔ (∀ i, x ∈ f ⁻¹' B i) := iff_of_eq rfl _ ↔ x ∈ ⋂ i, f ⁻¹' B i := mem_iInter.symm -- 2ª demostración -- =============== example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) := by ext x -- x : α -- ⊢ x ∈ f ⁻¹' ⋂ (i : I), B i ↔ x ∈ ⋂ (i : I), f ⁻¹' B i constructor . -- ⊢ x ∈ f ⁻¹' ⋂ (i : I), B i → x ∈ ⋂ (i : I), f ⁻¹' B i intro hx -- hx : x ∈ f ⁻¹' ⋂ (i : I), B i -- ⊢ x ∈ ⋂ (i : I), f ⁻¹' B i apply mem_iInter_of_mem -- ⊢ ∀ (i : I), x ∈ f ⁻¹' B i intro i -- i : I -- ⊢ x ∈ f ⁻¹' B i rw [mem_preimage] -- ⊢ f x ∈ B i rw [mem_preimage] at hx -- hx : f x ∈ ⋂ (i : I), B i rw [mem_iInter] at hx -- hx : ∀ (i : I), f x ∈ B i exact hx i . -- ⊢ x ∈ ⋂ (i : I), f ⁻¹' B i → x ∈ f ⁻¹' ⋂ (i : I), B i intro hx -- hx : x ∈ ⋂ (i : I), f ⁻¹' B i -- ⊢ x ∈ f ⁻¹' ⋂ (i : I), B i rw [mem_preimage] -- ⊢ f x ∈ ⋂ (i : I), B i rw [mem_iInter] -- ⊢ ∀ (i : I), f x ∈ B i intro i -- i : I -- ⊢ f x ∈ B i rw [←mem_preimage] -- ⊢ x ∈ f ⁻¹' B i rw [mem_iInter] at hx -- hx : ∀ (i : I), x ∈ f ⁻¹' B i exact hx i -- 3ª demostración -- =============== example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) := by ext x -- ⊢ x ∈ f ⁻¹' ⋂ (i : I), B i ↔ x ∈ ⋂ (i : I), f ⁻¹' B i simp -- 4ª demostración -- =============== example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) := by { ext ; simp } -- Lemas usados -- ============ -- variable (x : α) -- variable (s : Set β) -- variable (A : I → Set α) -- variable (a b : Prop) -- #check (iff_of_eq : a = b → (a ↔ b)) -- #check (mem_iInter : x ∈ ⋂ i, A i ↔ ∀ i, x ∈ A i) -- #check (mem_iInter_of_mem : (∀ i, x ∈ A i) → x ∈ ⋂ i, A i) -- #check (mem_preimage : x ∈ f ⁻¹' s ↔ f x ∈ s) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3.3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 |
theory Imagen_inversa_de_la_interseccion_general imports Main begin (* 1ª demostración *) lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)" proof (rule equalityI) show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)" proof (rule subsetI) fix x assume "x ∈ f -` (⋂ i ∈ I. B i)" show "x ∈ (⋂ i ∈ I. f -` B i)" proof (rule INT_I) fix i assume "i ∈ I" have "f x ∈ (⋂ i ∈ I. B i)" using ‹x ∈ f -` (⋂ i ∈ I. B i)› by (rule vimageD) then have "f x ∈ B i" using ‹i ∈ I› by (rule INT_D) then show "x ∈ f -` B i" by (rule vimageI2) qed qed next show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)" proof (rule subsetI) fix x assume "x ∈ (⋂ i ∈ I. f -` B i)" have "f x ∈ (⋂ i ∈ I. B i)" proof (rule INT_I) fix i assume "i ∈ I" with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i" by (rule INT_D) then show "f x ∈ B i" by (rule vimageD) qed then show "x ∈ f -` (⋂ i ∈ I. B i)" by (rule vimageI2) qed qed (* 2ª demostración *) lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)" proof show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)" proof (rule subsetI) fix x assume hx : "x ∈ f -` (⋂ i ∈ I. B i)" show "x ∈ (⋂ i ∈ I. f -` B i)" proof fix i assume "i ∈ I" have "f x ∈ (⋂ i ∈ I. B i)" using hx by simp then have "f x ∈ B i" using ‹i ∈ I› by simp then show "x ∈ f -` B i" by simp qed qed next show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)" proof fix x assume "x ∈ (⋂ i ∈ I. f -` B i)" have "f x ∈ (⋂ i ∈ I. B i)" proof fix i assume "i ∈ I" with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i" by simp then show "f x ∈ B i" by simp qed then show "x ∈ f -` (⋂ i ∈ I. B i)" by simp qed qed (* 3 demostración *) lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)" by (simp only: vimage_INT) (* 4ª demostración *) lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)" by auto end |
4. Teorema de Cantor
Demostrar con Lean4 el teorema de Cantor; es decir, que no existe ninguna aplicación suprayectiva de un conjunto en el conjunto de sus subconjuntos.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Set.Basic open Function variable {α : Type} example : ∀ f : α → Set α, ¬Surjective f := by sorry |
4.1. Demostración en lenguaje natural
Sea \(f\) una función de \(A\) en el conjunto de los subconjuntos \(A\). Tenemos que demostrar que \(f\) no es suprayectiva. Lo haremos por reducción al absurdo. Para ello, supongamos que \(f\) es suprayectiva y consideremos el conjunto
\[ S := \{i ∈ A | i ∉ f(i)\} \tag{1} \]
Entonces, tiene que existir un \(j ∈ A\) tal que
\[ f(j) = S \tag{2} \]
Se pueden dar dos casos: \(j ∈ S\) ó \(j ∉ S\). Veamos que ambos son imposibles.
Caso 1: Supongamos que \(j ∈ S\). Entonces, por (1)
\[ j ∉ f(j) \]
y, por (2),
\[ j ∉ S \]
que es una contradicción.
Caso 2: Supongamos que \(j ∉ S\). Entonces, por (1)
\[ j ∈ f(j) \]
y, por (2),
\[ j ∈ S \]
que es una contradicción.
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 |
import Mathlib.Data.Set.Basic open Function variable {α : Type} -- 1ª demostración -- =============== example : ∀ f : α → Set α, ¬Surjective f := by intros f hf -- f : α → Set α -- hf : Surjective f -- ⊢ False let S := {i | i ∉ f i} unfold Surjective at hf -- hf : ∀ (b : Set α), ∃ a, f a = b cases' hf S with j hj -- j : α -- hj : f j = S by_cases j ∈ S . -- h : j ∈ S dsimp at h -- h : ¬j ∈ f j apply h -- ⊢ j ∈ f j rw [hj] -- ⊢ j ∈ S exact h . -- h : ¬j ∈ S apply h -- ⊢ j ∈ S rw [←hj] at h -- h : ¬j ∈ f j exact h -- 2ª demostración -- =============== example : ∀ f : α → Set α, ¬ Surjective f := by intros f hf -- f : α → Set α -- hf : Surjective f -- ⊢ False let S := {i | i ∉ f i} cases' hf S with j hj -- j : α -- hj : f j = S by_cases j ∈ S . -- h : j ∈ S apply h -- ⊢ j ∈ f j rwa [hj] . -- h : ¬j ∈ S apply h rwa [←hj] at h -- 3ª demostración -- =============== example : ∀ f : α → Set α, ¬ Surjective f := by intros f hf -- f : α → Set α -- hf : Surjective f -- ⊢ False let S := {i | i ∉ f i} cases' hf S with j hj -- j : α -- hj : f j = S have h : (j ∈ S) = (j ∉ S) := calc (j ∈ S) = (j ∉ f j) := Set.mem_setOf_eq _ = (j ∉ S) := congrArg (j ∉ .) hj exact iff_not_self (iff_of_eq h) -- 4ª demostración -- =============== example : ∀ f : α → Set α, ¬ Surjective f := cantor_surjective -- Lemas usados -- ============ -- variable (x : α) -- variable (p : α → Prop) -- variable (a b : Prop) -- #check (Set.mem_setOf_eq : (x ∈ {y : α | p y}) = p x) -- #check (iff_of_eq : a = b → (a ↔ b)) -- #check (iff_not_self : ¬(a ↔ ¬a)) -- #check (cantor_surjective : ∀ f : α → Set α, ¬ Surjective f) |
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 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 |
theory Teorema_de_Cantor imports Main begin (* 1ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" proof (rule notI) assume "surj f" let ?S = "{i. i ∉ f i}" have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD) then obtain j where "?S = f j" by (rule exE) show False proof (cases "j ∈ ?S") assume "j ∈ ?S" then have "j ∉ f j" by (rule CollectD) moreover have "j ∈ f j" using ‹?S = f j› ‹j ∈ ?S› by (rule subst) ultimately show False by (rule notE) next assume "j ∉ ?S" with ‹?S = f j› have "j ∉ f j" by (rule subst) then have "j ∈ ?S" by (rule CollectI) with ‹j ∉ ?S› show False by (rule notE) qed qed (* 2ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" proof (rule notI) assume "surj f" let ?S = "{i. i ∉ f i}" have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD) then obtain j where "?S = f j" by (rule exE) have "j ∉ ?S" proof (rule notI) assume "j ∈ ?S" then have "j ∉ f j" by (rule CollectD) with ‹?S = f j› have "j ∉ ?S" by (rule ssubst) then show False using ‹j ∈ ?S› by (rule notE) qed moreover have "j ∈ ?S" proof (rule CollectI) show "j ∉ f j" proof (rule notI) assume "j ∈ f j" with ‹?S = f j› have "j ∈ ?S" by (rule ssubst) then have "j ∉ f j" by (rule CollectD) then show False using ‹j ∈ f j› by (rule notE) qed qed ultimately show False by (rule notE) qed (* 3ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" proof assume "surj f" let ?S = "{i. i ∉ f i}" have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD) then obtain j where "?S = f j" by (rule exE) have "j ∉ ?S" proof assume "j ∈ ?S" then have "j ∉ f j" by simp with ‹?S = f j› have "j ∉ ?S" by simp then show False using ‹j ∈ ?S› by simp qed moreover have "j ∈ ?S" proof show "j ∉ f j" proof assume "j ∈ f j" with ‹?S = f j› have "j ∈ ?S" by simp then have "j ∉ f j" by simp then show False using ‹j ∈ f j› by simp qed qed ultimately show False by simp qed (* 4ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" proof (rule notI) assume "surj f" let ?S = "{i. i ∉ f i}" have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD) then obtain j where "?S = f j" by (rule exE) have "j ∈ ?S = (j ∉ f j)" by (rule mem_Collect_eq) also have "… = (j ∉ ?S)" by (simp only: ‹?S = f j›) finally show False by (simp only: simp_thms(10)) qed (* 5ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" proof assume "surj f" let ?S = "{i. i ∉ f i}" have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD) then obtain j where "?S = f j" by (rule exE) have "j ∈ ?S = (j ∉ f j)" by simp also have "… = (j ∉ ?S)" using ‹?S = f j› by simp finally show False by simp qed (* 6ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" unfolding surj_def by best end |
5. En los monoides, los inversos a la izquierda y a la derecha son iguales
Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.
En Lean4, está definida la clase de los monoides (como Monoid) y sus propiedades características son
|
1 2 3 |
mul_assoc : (a * b) * c = a * (b * c) one_mul : 1 * a = a mul_one : a * 1 = a |
Demostrar que si \(M\) es un monoide, \(a ∈ M\), \(b\) es un inverso de \(a\) por la izquierda y \(c\) es un inverso de \(a\) por la derecha, entonces \(b = c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Algebra.Group.Defs variable {M : Type} [Monoid M] variable {a b c : M} example (hba : b * a = 1) (hac : a * c = 1) : b = c := by sorry |
5.1. Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align}
b &= b * 1 &&\text{[por mul_one]} \\
&= b * (a * c) &&\text{[por hipótesis]} \\
&= (b * a) * c &&\text{[por mul_assoc]} \\
&= 1 * c &&\text{[por hipótesis]} \\
&= c &&\text{[por one_mul]} \\
\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 |
import Mathlib.Algebra.Group.Defs variable {M : Type} [Monoid M] variable {a b c : M} -- 1ª demostración -- =============== example (hba : b * a = 1) (hac : a * c = 1) : b = c := calc b = b * 1 := (mul_one b).symm _ = b * (a * c) := congrArg (b * .) hac.symm _ = (b * a) * c := (mul_assoc b a c).symm _ = 1 * c := congrArg (. * c) hba _ = c := one_mul c -- 2ª demostración -- =============== example (hba : b * a = 1) (hac : a * c = 1) : b = c := calc b = b * 1 := by aesop _ = b * (a * c) := by aesop _ = (b * a) * c := (mul_assoc b a c).symm _ = 1 * c := by aesop _ = c := by aesop -- 1ª demostración -- =============== example (hba : b * a = 1) (hac : a * c = 1) : b = c := by rw [←one_mul c] -- ⊢ b = 1 * c rw [←hba] -- ⊢ b = (b * a) * c rw [mul_assoc] -- ⊢ b = b * (a * c) rw [hac] -- ⊢ b = b * 1 rw [mul_one b] -- 2ª demostración -- =============== example (hba : b * a = 1) (hac : a * c = 1) : b = c := by rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b] -- 5ª demostración -- =============== example (hba : b * a = 1) (hac : a * c = 1) : b = c := left_inv_eq_right_inv hba hac -- Lemas usados -- ============ -- #check (left_inv_eq_right_inv : b * a = 1 → a * c = 1 → b = c) -- #check (mul_assoc a b c : (a * b) * c = a * (b * c)) -- #check (mul_one a : a * 1 = a) -- #check (one_mul a : 1 * a = a) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
5.3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 |
theory En_los_monoides_los_inversos_a_la_izquierda_y_a_la_derecha_son_iguales imports Main begin context monoid begin (* 1ª demostración *) lemma assumes "b * a = 1" "a * c = 1" shows "b = c" proof - have "b = b * 1" by (simp only: right_neutral) also have "… = b * (a * c)" by (simp only: ‹a * c = 1›) also have "… = (b * a) * c" by (simp only: assoc) also have "… = 1 * c" by (simp only: ‹b * a = 1›) also have "… = c" by (simp only: left_neutral) finally show "b = c" by this qed (* 2ª demostración *) lemma assumes "b * a = 1" "a * c = 1" shows "b = c" proof - have "b = b * 1" by simp also have "… = b * (a * c)" using ‹a * c = 1› by simp also have "… = (b * a) * c" by (simp add: assoc) also have "… = 1 * c" using ‹b * a = 1› by simp also have "… = c" by simp finally show "b = c" by this qed (* 3ª demostración *) lemma assumes "b * a = 1" "a * c = 1" shows "b = c" using assms by (metis assoc left_neutral right_neutral) end end |