La semana en Calculemus (21 de abril de 2024)
Desde el 18 de marzo, he publicado en Calculemus las demostraciones con Lean4 e Isabelle/HOL de las siguientes propiedades:
- 1. Si f es inyectiva, entonces f⁻¹(f(s)) ⊆ s
- 2. f(f⁻¹(u)) ⊆ u
- 3. Si f es suprayectiva, entonces u ⊆ f(f⁻¹(u))
- 4. Si s ⊆ t, entonces f(s) ⊆ f(t)
- 5. Si u ⊆ v, entonces f⁻¹(u) ⊆ f⁻¹(v)
- 6. f⁻¹(A ∪ B) = f⁻¹(A) ∪ f⁻¹(B)
- 7. f(s ∩ t) ⊆ f(s) ∩ f(t)
- 8. Si f es inyectiva, entonces f(s) ∩ f(t) ⊆ f(s ∩ t)
- 9. f(s) \ f(t) ⊆ f(s \ t)
- 10. f(s) ∩ t = f(s ∩ f⁻¹(t))
A continuación se muestran las soluciones.
1. Si f es inyectiva, entonces f⁻¹[f[s]] ⊆ s
Demostrar con Lean4 que si \(f\) es inyectiva, entonces \(f⁻¹[f[s]] ⊆ s\).
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Data.Set.Function open Set Function variable {α β : Type _} variable (f : α → β) variable (s : Set α) example (h : Injective f) : f ⁻¹' (f '' s) ⊆ s := by sorry |
1.1. Demostración en lenguaje natural
Sea \(x\) tal que
\[ x ∈ f⁻¹[f[s]] \]
Entonces,
\[ f(x) ∈ f[s] \]
y, por tanto, existe un
\[ y ∈ s \tag{1} \]
tal que
\[ f(y) = f(x) \tag{2} \]
De (2), puesto que \(f\) es inyectiva, se tiene que
\[ y = x \tag{3} \]
Finalmente, de (3) y (1), se tiene que
\[ x ∈ s \]
que es lo que teníamos que demostrar.
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 |
import Mathlib.Data.Set.Function open Set Function variable {α β : Type _} variable (f : α → β) variable (s : Set α) -- 1ª demostración -- =============== example (h : Injective f) : f ⁻¹' (f '' s) ⊆ s := by intros x hx -- x : α -- hx : x ∈ f ⁻¹' (f '' s) -- ⊢ x ∈ s have h1 : f x ∈ f '' s := mem_preimage.mp hx have h2 : ∃ y, y ∈ s ∧ f y = f x := (mem_image f s (f x)).mp h1 obtain ⟨y, hy : y ∈ s ∧ f y = f x⟩ := h2 obtain ⟨ys : y ∈ s, fyx : f y = f x⟩ := hy have h3 : y = x := h fyx show x ∈ s exact h3 ▸ ys -- 2ª demostración -- =============== example (h : Injective f) : f ⁻¹' (f '' s) ⊆ s := by intros x hx -- x : α -- hx : x ∈ f ⁻¹' (f '' s) -- ⊢ x ∈ s rw [mem_preimage] at hx -- hx : f x ∈ f '' s rw [mem_image] at hx -- hx : ∃ x_1, x_1 ∈ s ∧ f x_1 = f x rcases hx with ⟨y, hy⟩ -- y : α -- hy : y ∈ s ∧ f y = f x rcases hy with ⟨ys, fyx⟩ -- ys : y ∈ s -- fyx : f y = f x unfold Injective at h -- h : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂ have h1 : y = x := h fyx rw [←h1] -- ⊢ y ∈ s exact ys -- 3ª demostración -- =============== example (h : Injective f) : f ⁻¹' (f '' s) ⊆ s := by intros x hx -- x : α -- hx : x ∈ f ⁻¹' (f '' s) -- ⊢ x ∈ s rw [mem_preimage] at hx -- hx : f x ∈ f '' s rcases hx with ⟨y, ys, fyx⟩ -- y : α -- ys : y ∈ s -- fyx : f y = f x rw [←h fyx] -- ⊢ y ∈ s exact ys -- 4ª demostración -- =============== example (h : Injective f) : f ⁻¹' (f '' s) ⊆ s := by rintro x ⟨y, ys, hy⟩ -- x y : α -- ys : y ∈ s -- hy : f y = f x -- ⊢ x ∈ s rw [←h hy] -- ⊢ y ∈ s exact ys -- Lemas usados -- ============ -- variable (x : α) -- variable (y : β) -- variable (t : Set β) -- #check (mem_image f s y : y ∈ f '' s ↔ ∃ (x : α), x ∈ s ∧ f x = y) -- #check (mem_preimage : x ∈ f ⁻¹' t ↔ f x ∈ t) |
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 |
theory Imagen_inversa_de_la_imagen_de_aplicaciones_inyectivas imports Main begin (* 1ª demostración *) lemma assumes "inj f" shows "f -` (f ` s) ⊆ s" proof (rule subsetI) fix x assume "x ∈ f -` (f ` s)" then have "f x ∈ f ` s" by (rule vimageD) then show "x ∈ s" proof (rule imageE) fix y assume "f x = f y" assume "y ∈ s" have "x = y" using ‹inj f› ‹f x = f y› by (rule injD) then show "x ∈ s" using ‹y ∈ s› by (rule ssubst) qed qed (* 2ª demostración *) lemma assumes "inj f" shows "f -` (f ` s) ⊆ s" proof fix x assume "x ∈ f -` (f ` s)" then have "f x ∈ f ` s" by simp then show "x ∈ s" proof fix y assume "f x = f y" assume "y ∈ s" have "x = y" using ‹inj f› ‹f x = f y› by (rule injD) then show "x ∈ s" using ‹y ∈ s› by simp qed qed (* 3ª demostración *) lemma assumes "inj f" shows "f -` (f ` s) ⊆ s" using assms unfolding inj_def by auto (* 4ª demostración *) lemma assumes "inj f" shows "f -` (f ` s) ⊆ s" using assms by (simp only: inj_vimage_image_eq) end |
2. f[f⁻¹[u]] ⊆ u
Demostrar con Lean4 que
\[ f[f⁻¹[u]] ⊆ u \]
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (u : Set β) example : f '' (f⁻¹' u) ⊆ u := by sorry |
2.1. Demostración en lenguaje natural
Sea \(y ∈ f[f⁻¹[u]]\). Entonces existe un \(x\) tal que
\begin{align}
&x ∈ f⁻¹[u] \tag{1} \\
&f(x) = y \tag{2}
\end{align}
Por (1),
\[ f(x) ∈ u \]
y, por (2),
\[ y ∈ u \]
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 |
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (u : Set β) -- 1ª demostración -- =============== example : f '' (f⁻¹' u) ⊆ u := by intros y h -- y : β -- h : y ∈ f '' (f ⁻¹' u) -- ⊢ y ∈ u obtain ⟨x : α, h1 : x ∈ f ⁻¹' u ∧ f x = y⟩ := h obtain ⟨hx : x ∈ f ⁻¹' u, fxy : f x = y⟩ := h1 have h2 : f x ∈ u := mem_preimage.mp hx show y ∈ u exact fxy ▸ h2 -- 2ª demostración -- =============== example : f '' (f⁻¹' u) ⊆ u := by intros y h -- y : β -- h : y ∈ f '' (f ⁻¹' u) -- ⊢ y ∈ u rcases h with ⟨x, h2⟩ -- x : α -- h2 : x ∈ f ⁻¹' u ∧ f x = y rcases h2 with ⟨hx, fxy⟩ -- hx : x ∈ f ⁻¹' u -- fxy : f x = y rw [←fxy] -- ⊢ f x ∈ u exact hx -- 3ª demostración -- =============== example : f '' (f⁻¹' u) ⊆ u := by intros y h -- y : β -- h : y ∈ f '' (f ⁻¹' u) -- ⊢ y ∈ u rcases h with ⟨x, hx, fxy⟩ -- x : α -- hx : x ∈ f ⁻¹' u -- fxy : f x = y rw [←fxy] -- ⊢ f x ∈ u exact hx -- 4ª demostración -- =============== example : f '' (f⁻¹' u) ⊆ u := by rintro y ⟨x, hx, fxy⟩ -- y : β -- x : α -- hx : x ∈ f ⁻¹' u -- fxy : f x = y -- ⊢ y ∈ u rw [←fxy] -- ⊢ f x ∈ u exact hx -- 5ª demostración -- =============== example : f '' (f⁻¹' u) ⊆ u := by rintro y ⟨x, hx, rfl⟩ -- x : α -- hx : x ∈ f ⁻¹' u -- ⊢ f x ∈ u exact hx -- 6ª demostración -- =============== example : f '' (f⁻¹' u) ⊆ u := image_preimage_subset f u -- Lemas usados -- ============ -- #check (image_preimage_subset f u : f '' (f⁻¹' u) ⊆ u) |
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 |
theory Imagen_de_la_imagen_inversa imports Main begin (* 1ª demostración *) lemma "f ` (f -` u) ⊆ u" proof (rule subsetI) fix y assume "y ∈ f ` (f -` u)" then show "y ∈ u" proof (rule imageE) fix x assume "y = f x" assume "x ∈ f -` u" then have "f x ∈ u" by (rule vimageD) with ‹y = f x› show "y ∈ u" by (rule ssubst) qed qed (* 2ª demostración *) lemma "f ` (f -` u) ⊆ u" proof fix y assume "y ∈ f ` (f -` u)" then show "y ∈ u" proof fix x assume "y = f x" assume "x ∈ f -` u" then have "f x ∈ u" by simp with ‹y = f x› show "y ∈ u" by simp qed qed (* 3ª demostración *) lemma "f ` (f -` u) ⊆ u" by (simp only: image_vimage_subset) (* 4ª demostración *) lemma "f ` (f -` u) ⊆ u" by auto end |
3. Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]]
Demostrar con Lean4 que si \(f\) es suprayectiva, entonces
\[ u ⊆ f[f⁻¹[u]] \]
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Data.Set.Function open Set Function variable {α β : Type _} variable (f : α → β) variable (u : Set β) example (h : Surjective f) : u ⊆ f '' (f⁻¹' u) := by sorry |
3.1. Demostración en lenguaje natural
Sea \(y ∈ u\). Por ser \(f\) suprayectiva, exite un \(x\) tal que
\[ f(x) = y \tag{1} \]
Por tanto, \(x ∈ f⁻¹[u]\) y
\[ f(x) ∈ f[f⁻¹[u]] \tag{2} \]
Finalmente, por (1) y (2),
\[ y ∈ f[f⁻¹[u]] \]
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.Set.Function open Set Function variable {α β : Type _} variable (f : α → β) variable (u : Set β) -- 1ª demostración -- =============== example (h : Surjective f) : u ⊆ f '' (f⁻¹' u) := by intros y yu -- y : β -- yu : y ∈ u -- ⊢ y ∈ f '' (f ⁻¹' u) rcases h y with ⟨x, fxy⟩ -- x : α -- fxy : f x = y use x -- ⊢ x ∈ f ⁻¹' u ∧ f x = y constructor { -- ⊢ x ∈ f ⁻¹' u apply mem_preimage.mpr -- ⊢ f x ∈ u rw [fxy] -- ⊢ y ∈ u exact yu } { -- ⊢ f x = y exact fxy } -- 2ª demostración -- =============== example (h : Surjective f) : u ⊆ f '' (f⁻¹' u) := by intros y yu -- y : β -- yu : y ∈ u -- ⊢ y ∈ f '' (f ⁻¹' u) rcases h y with ⟨x, fxy⟩ -- x : α -- fxy : f x = y -- ⊢ y ∈ f '' (f ⁻¹' u) use x -- ⊢ x ∈ f ⁻¹' u ∧ f x = y constructor { show f x ∈ u rw [fxy] -- ⊢ y ∈ u exact yu } { show f x = y exact fxy } -- 3ª demostración -- =============== example (h : Surjective f) : u ⊆ f '' (f⁻¹' u) := by intros y yu -- y : β -- yu : y ∈ u -- ⊢ y ∈ f '' (f ⁻¹' u) rcases h y with ⟨x, fxy⟩ -- x : α -- fxy : f x = y aesop -- Lemas usados -- ============ -- variable (x : α) -- #check (mem_preimage : x ∈ f ⁻¹' u ↔ f x ∈ u) |
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 |
theory Imagen_de_imagen_inversa_de_aplicaciones_suprayectivas imports Main begin (* 1ª demostración *) lemma assumes "surj f" shows "u ⊆ f ` (f -` u)" proof (rule subsetI) fix y assume "y ∈ u" have "∃x. y = f x" using ‹surj f› by (rule surjD) then obtain x where "y = f x" by (rule exE) then have "f x ∈ u" using ‹y ∈ u› by (rule subst) then have "x ∈ f -` u" by (simp only: vimage_eq) then have "f x ∈ f ` (f -` u)" by (rule imageI) with ‹y = f x› show "y ∈ f ` (f -` u)" by (rule ssubst) qed (* 2ª demostración *) lemma assumes "surj f" shows "u ⊆ f ` (f -` u)" proof fix y assume "y ∈ u" have "∃x. y = f x" using ‹surj f› by (rule surjD) then obtain x where "y = f x" by (rule exE) then have "f x ∈ u" using ‹y ∈ u› by simp then have "x ∈ f -` u" by simp then have "f x ∈ f ` (f -` u)" by simp with ‹y = f x› show "y ∈ f ` (f -` u)" by simp qed (* 3ª demostración *) lemma assumes "surj f" shows "u ⊆ f ` (f -` u)" using assms by (simp only: surj_image_vimage_eq) (* 4ª demostración *) lemma assumes "surj f" shows "u ⊆ f ` (f -` u)" using assms unfolding surj_def by auto (* 5ª demostración *) lemma assumes "surj f" shows "u ⊆ f ` (f -` u)" using assms by auto end |
4. Si s ⊆ t, entonces f[s] ⊆ f[t]
Demostrar con Lean4 que si \(s ⊆ t\), entonces \(f[s] ⊆ f[t]\).
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.Set.Function import Mathlib.Tactic open Set variable {α β : Type _} variable (f : α → β) variable (s t : Set α) example (h : s ⊆ t) : f '' s ⊆ f '' t := by sorry |
4.1. Demostración en lenguaje natural
Sea \(y ∈ f[s]\). Entonces, existe un x tal que
\begin{align}
&x ∈ s \tag{1} \\
&f(x) = y \tag{2}
\end{align}
Por (1) y la hipótesis,
\[ x ∈ t \tag{3} \]
Por (3),
\[ f(x) ∈ f[t] \tag{4} \]
y, por (2) y (4),
\[ y ∈ f[t] \]
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 |
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable {α β : Type _} variable (f : α → β) variable (s t : Set α) -- 1ª demostración -- =============== example (h : s ⊆ t) : f '' s ⊆ f '' t := by intros y hy -- y : β -- hy : y ∈ f '' s -- ⊢ y ∈ f '' t rw [mem_image] at hy -- hy : ∃ x, x ∈ s ∧ f x = y rcases hy with ⟨x, hx⟩ -- x : α -- hx : x ∈ s ∧ f x = y rcases hx with ⟨xs, fxy⟩ -- xs : x ∈ s -- fxy : f x = y use x -- ⊢ x ∈ t ∧ f x = y constructor . -- ⊢ x ∈ t exact h xs . -- ⊢ f x = y exact fxy -- 2ª demostración -- =============== example (h : s ⊆ t) : f '' s ⊆ f '' t := by intros y hy -- y : β -- hy : y ∈ f '' s -- ⊢ y ∈ f '' t rcases hy with ⟨x, xs, fxy⟩ -- x : α -- xs : x ∈ s -- fxy : f x = y use x -- ⊢ x ∈ t ∧ f x = y exact ⟨h xs, fxy⟩ -- 3ª demostración -- =============== example (h : s ⊆ t) : f '' s ⊆ f '' t := image_subset f h -- Lemas usados -- ============ -- variable (y : β) -- #check (mem_image f s y : y ∈ f '' s ↔ ∃ x, x ∈ s ∧ f x = y) -- #check (image_subset f : s ⊆ t → f '' s ⊆ f '' t) |
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 |
theory Monotonia_de_la_imagen_de_conjuntos imports Main begin (* 1ª demostración *) lemma assumes "s ⊆ t" shows "f ` s ⊆ f ` t" proof (rule subsetI) fix y assume "y ∈ f ` s" then show "y ∈ f ` t" proof (rule imageE) fix x assume "y = f x" assume "x ∈ s" then have "x ∈ t" using ‹s ⊆ t› by (simp only: set_rev_mp) then have "f x ∈ f ` t" by (rule imageI) with ‹y = f x› show "y ∈ f ` t" by (rule ssubst) qed qed (* 2ª demostración *) lemma assumes "s ⊆ t" shows "f ` s ⊆ f ` t" proof fix y assume "y ∈ f ` s" then show "y ∈ f ` t" proof fix x assume "y = f x" assume "x ∈ s" then have "x ∈ t" using ‹s ⊆ t› by (simp only: set_rev_mp) then have "f x ∈ f ` t" by simp with ‹y = f x› show "y ∈ f ` t" by simp qed qed (* 3ª demostración *) lemma assumes "s ⊆ t" shows "f ` s ⊆ f ` t" using assms by blast (* 4ª demostración *) lemma assumes "s ⊆ t" shows "f ` s ⊆ f ` t" using assms by (simp only: image_mono) end |
5. Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]
Demostrar con Lean4 que si \(u ⊆ v\), entonces \(f⁻¹[u] ⊆ f⁻¹[v]\).
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (u v : Set β) example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by sorry |
5.1. Demostración en lenguaje natural
Por la siguiente cadena de implicaciones:
\begin{align}
x ∈ f⁻¹[u] &⟹ f(x) ∈ u \\
&⟹ f(x) ∈ v &&\text{[porque \(u ⊆ v\)]} \\
&⟹ x ∈ f⁻¹[v]
\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 101 102 103 104 105 106 107 108 |
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (u v : Set β) -- 1ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intros x hx -- x : α -- hx : x ∈ f ⁻¹' u -- ⊢ x ∈ f ⁻¹' v have h1 : f x ∈ u := mem_preimage.mp hx have h2 : f x ∈ v := h h1 show x ∈ f ⁻¹' v exact mem_preimage.mpr h2 -- 2ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intros x hx -- x : α -- hx : x ∈ f ⁻¹' u -- ⊢ x ∈ f ⁻¹' v apply mem_preimage.mpr -- ⊢ f x ∈ v apply h -- ⊢ f x ∈ u apply mem_preimage.mp -- ⊢ x ∈ f ⁻¹' u exact hx -- 3ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intros x hx -- x : α -- hx : x ∈ f ⁻¹' u -- ⊢ x ∈ f ⁻¹' v apply h -- ⊢ f x ∈ u exact hx -- 4ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intros x hx -- x : α -- hx : x ∈ f ⁻¹' u -- ⊢ x ∈ f ⁻¹' v exact h hx -- 5ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := fun _ hx ↦ h hx -- 6ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intro x; apply h -- 7ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := preimage_mono h -- 8ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by tauto -- Lemas usados -- ============ -- variable (a : α) -- #check (mem_preimage : a ∈ f ⁻¹' u ↔ f a ∈ u) -- #check (preimage_mono : u ⊆ v → f ⁻¹' u ⊆ f ⁻¹' v) |
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 Monotonia_de_la_imagen_inversa imports Main begin (* 1ª demostración *) lemma assumes "u ⊆ v" shows "f -` u ⊆ f -` v" proof (rule subsetI) fix x assume "x ∈ f -` u" then have "f x ∈ u" by (rule vimageD) then have "f x ∈ v" using ‹u ⊆ v› by (rule set_rev_mp) then show "x ∈ f -` v" by (simp only: vimage_eq) qed (* 2ª demostración *) lemma assumes "u ⊆ v" shows "f -` u ⊆ f -` v" proof fix x assume "x ∈ f -` u" then have "f x ∈ u" by simp then have "f x ∈ v" using ‹u ⊆ v› by (rule set_rev_mp) then show "x ∈ f -` v" by simp qed (* 3ª demostración *) lemma assumes "u ⊆ v" shows "f -` u ⊆ f -` v" using assms by (simp only: vimage_mono) (* 4ª demostración *) lemma assumes "u ⊆ v" shows "f -` u ⊆ f -` v" using assms by blast end |
6. f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]
Demostrar con Lean4 que \(f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]\).
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (A B : Set β) example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B := by sorry |
6.1. Demostración en lenguaje natural
Tenemos que demostrar que, para todo \(x\),
\[ x ∈ f⁻¹[A ∪ B] ↔ x ∈ f⁻¹[A] ∪ f⁻¹[B] \]
Lo haremos demostrando las dos implicaciones.
(⟹) Supongamos que \(x ∈ f⁻¹[A ∪ B]\). Entonces, \(f(x) ∈ A ∪ B\).
Distinguimos dos casos:
Caso 1: Supongamos que \(f(x) ∈ A\). Entonces, \(x ∈ f⁻¹[A]\) y, por tanto,
\(x ∈ f⁻¹[A] ∪ f⁻¹[B]\).
Caso 2: Supongamos que \(f(x) ∈ B\). Entonces, \(x ∈ f⁻¹[B]\) y, por tanto,
\(x ∈ f⁻¹[A] ∪ f⁻¹[B]\).
(⟸) Supongamos que \(x ∈ f⁻¹[A] ∪ f⁻¹[B]\). Distinguimos dos casos.
Caso 1: Supongamos que \(x ∈ f⁻¹[A]\). Entonces, \(f(x) ∈ A\) y, por tanto,
\(f(x) ∈ A ∪ B\). Luego, \(x ∈ f⁻¹[A ∪ B]\).
Caso 2: Supongamos que \(x ∈ f⁻¹[B]\). Entonces, \(f(x) ∈ B\) y, por tanto,
\(f(x) ∈ A ∪ B\). Luego, \(x ∈ f⁻¹[A ∪ B]\).
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 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 179 180 181 |
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (A B : Set β) -- 1ª demostración -- =============== example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B := by ext x -- x : α -- ⊢ x ∈ f ⁻¹' (A ∪ B) ↔ x ∈ f ⁻¹' A ∪ f ⁻¹' B constructor . -- ⊢ x ∈ f ⁻¹' (A ∪ B) → x ∈ f ⁻¹' A ∪ f ⁻¹' B intro h -- h : x ∈ f ⁻¹' (A ∪ B) -- ⊢ x ∈ f ⁻¹' A ∪ f ⁻¹' B rw [mem_preimage] at h -- h : f x ∈ A ∪ B rcases h with fxA | fxB . -- fxA : f x ∈ A left -- ⊢ x ∈ f ⁻¹' A apply mem_preimage.mpr -- ⊢ f x ∈ A exact fxA . -- fxB : f x ∈ B right -- ⊢ x ∈ f ⁻¹' B apply mem_preimage.mpr -- ⊢ f x ∈ B exact fxB . -- ⊢ x ∈ f ⁻¹' A ∪ f ⁻¹' B → x ∈ f ⁻¹' (A ∪ B) intro h -- h : x ∈ f ⁻¹' A ∪ f ⁻¹' B -- ⊢ x ∈ f ⁻¹' (A ∪ B) rw [mem_preimage] -- ⊢ f x ∈ A ∪ B rcases h with xfA | xfB . -- xfA : x ∈ f ⁻¹' A rw [mem_preimage] at xfA -- xfA : f x ∈ A left -- ⊢ f x ∈ A exact xfA . -- xfB : x ∈ f ⁻¹' B rw [mem_preimage] at xfB -- xfB : f x ∈ B right -- ⊢ f x ∈ B exact xfB -- 2ª demostración -- =============== example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B := by ext x -- x : α -- ⊢ x ∈ f ⁻¹' (A ∪ B) ↔ x ∈ f ⁻¹' A ∪ f ⁻¹' B constructor . -- ⊢ x ∈ f ⁻¹' (A ∪ B) → x ∈ f ⁻¹' A ∪ f ⁻¹' B intros h -- h : x ∈ f ⁻¹' (A ∪ B) -- ⊢ x ∈ f ⁻¹' A ∪ f ⁻¹' B rcases h with fxA | fxB . -- fxA : f x ∈ A left -- ⊢ x ∈ f ⁻¹' A exact fxA . -- fxB : f x ∈ B right -- ⊢ x ∈ f ⁻¹' B exact fxB . -- ⊢ x ∈ f ⁻¹' A ∪ f ⁻¹' B → x ∈ f ⁻¹' (A ∪ B) intro h -- h : x ∈ f ⁻¹' A ∪ f ⁻¹' B -- ⊢ x ∈ f ⁻¹' (A ∪ B) rcases h with xfA | xfB . -- xfA : x ∈ f ⁻¹' A left -- ⊢ f x ∈ A exact xfA . -- xfB : x ∈ f ⁻¹' B right -- ⊢ f x ∈ B exact xfB -- 3ª demostración -- =============== example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B := by ext x -- x : α -- ⊢ x ∈ f ⁻¹' (A ∪ B) ↔ x ∈ f ⁻¹' A ∪ f ⁻¹' B constructor . -- ⊢ x ∈ f ⁻¹' (A ∪ B) → x ∈ f ⁻¹' A ∪ f ⁻¹' B rintro (fxA | fxB) . -- fxA : f x ∈ A -- ⊢ x ∈ f ⁻¹' A ∪ f ⁻¹' B exact Or.inl fxA . -- fxB : f x ∈ B -- ⊢ x ∈ f ⁻¹' A ∪ f ⁻¹' B exact Or.inr fxB . -- ⊢ x ∈ f ⁻¹' A ∪ f ⁻¹' B → x ∈ f ⁻¹' (A ∪ B) rintro (xfA | xfB) . -- xfA : x ∈ f ⁻¹' A -- ⊢ x ∈ f ⁻¹' (A ∪ B) exact Or.inl xfA . -- xfB : x ∈ f ⁻¹' B -- ⊢ x ∈ f ⁻¹' (A ∪ B) exact Or.inr xfB -- 4ª demostración -- =============== example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B := by ext x -- x : α -- ⊢ x ∈ f ⁻¹' (A ∪ B) ↔ x ∈ f ⁻¹' A ∪ f ⁻¹' B constructor . -- ⊢ x ∈ f ⁻¹' (A ∪ B) → x ∈ f ⁻¹' A ∪ f ⁻¹' B aesop . -- ⊢ x ∈ f ⁻¹' A ∪ f ⁻¹' B → x ∈ f ⁻¹' (A ∪ B) aesop -- 5ª demostración -- =============== example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B := by ext x -- x : α -- ⊢ x ∈ f ⁻¹' (A ∪ B) ↔ x ∈ f ⁻¹' A ∪ f ⁻¹' B aesop -- 6ª demostración -- =============== example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B := by ext ; aesop -- 7ª demostración -- =============== example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B := by ext ; rfl -- 8ª demostración -- =============== example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B := rfl -- 9ª demostración -- =============== example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B := preimage_union -- 10ª demostración -- =============== example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B := by simp -- Lemas usados -- ============ -- variable (x : α) -- variable (p q : Prop) -- #check (Or.inl: p → p ∨ q) -- #check (Or.inr: q → p ∨ q) -- #check (mem_preimage : x ∈ f ⁻¹' A ↔ f x ∈ A) -- #check (preimage_union : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B) |
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 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 |
theory Imagen_inversa_de_la_union imports Main begin (* 1ª demostración *) lemma "f -` (u ∪ v) = f -` u ∪ f -` v" proof (rule equalityI) show "f -` (u ∪ v) ⊆ f -` u ∪ f -` v" proof (rule subsetI) fix x assume "x ∈ f -` (u ∪ v)" then have "f x ∈ u ∪ v" by (rule vimageD) then show "x ∈ f -` u ∪ f -` v" proof (rule UnE) assume "f x ∈ u" then have "x ∈ f -` u" by (rule vimageI2) then show "x ∈ f -` u ∪ f -` v" by (rule UnI1) next assume "f x ∈ v" then have "x ∈ f -` v" by (rule vimageI2) then show "x ∈ f -` u ∪ f -` v" by (rule UnI2) qed qed next show "f -` u ∪ f -` v ⊆ f -` (u ∪ v)" proof (rule subsetI) fix x assume "x ∈ f -` u ∪ f -` v" then show "x ∈ f -` (u ∪ v)" proof (rule UnE) assume "x ∈ f -` u" then have "f x ∈ u" by (rule vimageD) then have "f x ∈ u ∪ v" by (rule UnI1) then show "x ∈ f -` (u ∪ v)" by (rule vimageI2) next assume "x ∈ f -` v" then have "f x ∈ v" by (rule vimageD) then have "f x ∈ u ∪ v" by (rule UnI2) then show "x ∈ f -` (u ∪ v)" by (rule vimageI2) qed qed qed (* 2ª demostración *) lemma "f -` (u ∪ v) = f -` u ∪ f -` v" proof show "f -` (u ∪ v) ⊆ f -` u ∪ f -` v" proof fix x assume "x ∈ f -` (u ∪ v)" then have "f x ∈ u ∪ v" by simp then show "x ∈ f -` u ∪ f -` v" proof assume "f x ∈ u" then have "x ∈ f -` u" by simp then show "x ∈ f -` u ∪ f -` v" by simp next assume "f x ∈ v" then have "x ∈ f -` v" by simp then show "x ∈ f -` u ∪ f -` v" by simp qed qed next show "f -` u ∪ f -` v ⊆ f -` (u ∪ v)" proof fix x assume "x ∈ f -` u ∪ f -` v" then show "x ∈ f -` (u ∪ v)" proof assume "x ∈ f -` u" then have "f x ∈ u" by simp then have "f x ∈ u ∪ v" by simp then show "x ∈ f -` (u ∪ v)" by simp next assume "x ∈ f -` v" then have "f x ∈ v" by simp then have "f x ∈ u ∪ v" by simp then show "x ∈ f -` (u ∪ v)" by simp qed qed qed (* 3ª demostración *) lemma "f -` (u ∪ v) = f -` u ∪ f -` v" by (simp only: vimage_Un) (* 4ª demostración *) lemma "f -` (u ∪ v) = f -` u ∪ f -` v" by auto end |
7. f[s ∩ t] ⊆ f[s] ∩ f[t]
Demostrar con Lean4 que
\[ f[s ∩ t] ⊆ f[s] ∩ f[t] \]
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable {α β : Type _} variable (f : α → β) variable (s t : Set α) example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := by sorry |
7.1. Demostración en lenguaje natural
Sea tal que
\[ y ∈ f[s ∩ t] \]
Por tanto, existe un \(x\) tal que
\begin{align}
x ∈ s ∩ t \tag{1} \\
f(x) = y \tag{2}
\end{align}
Por (1), se tiene que
\begin{align}
x ∈ s \tag{3} \\
x ∈ t \tag{4}
\end{align}
Por (2) y (3), se tiene
\[ y ∈ f[s] \tag{5} \]
Por (2) y (4), se tiene
\[ y ∈ f[t] \tag{6} \]
Por (5) y (6), se tiene
\[ y ∈ f[s] ∩ f[t] \]
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 |
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable {α β : Type _} variable (f : α → β) variable (s t : Set α) -- 1ª demostración -- =============== example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := by intros y hy -- y : β -- hy : y ∈ f '' (s ∩ t) -- ⊢ y ∈ f '' s ∩ f '' t rcases hy with ⟨x, hx⟩ -- x : α -- hx : x ∈ s ∩ t ∧ f x = y rcases hx with ⟨xst, fxy⟩ -- xst : x ∈ s ∩ t -- fxy : f x = y constructor . -- ⊢ y ∈ f '' s use x -- ⊢ x ∈ s ∧ f x = y constructor . -- ⊢ x ∈ s exact xst.1 . -- ⊢ f x = y exact fxy . -- ⊢ y ∈ f '' t use x -- ⊢ x ∈ t ∧ f x = y constructor . -- ⊢ x ∈ t exact xst.2 . -- ⊢ f x = y exact fxy -- 2ª demostración -- =============== example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := by intros y hy -- y : β -- hy : y ∈ f '' (s ∩ t) -- ⊢ y ∈ f '' s ∩ f '' t rcases hy with ⟨x, ⟨xs, xt⟩, fxy⟩ -- x : α -- fxy : f x = y -- xs : x ∈ s -- xt : x ∈ t constructor . -- ⊢ y ∈ f '' s use x -- ⊢ x ∈ s ∧ f x = y exact ⟨xs, fxy⟩ . -- ⊢ y ∈ f '' t use x -- ⊢ x ∈ t ∧ f x = y exact ⟨xt, fxy⟩ -- 3ª demostración -- =============== example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := image_inter_subset f s t -- 4ª demostración -- =============== example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := by intro ; aesop -- Lemas usados -- ============ -- #check (image_inter_subset f s t : f '' (s ∩ t) ⊆ f '' s ∩ f '' t) |
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 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 |
theory Imagen_de_la_interseccion imports Main begin (* 1ª demostración *) lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t" proof (rule subsetI) fix y assume "y ∈ f ` (s ∩ t)" then have "y ∈ f ` s" proof (rule imageE) fix x assume "y = f x" assume "x ∈ s ∩ t" have "x ∈ s" using ‹x ∈ s ∩ t› by (rule IntD1) then have "f x ∈ f ` s" by (rule imageI) with ‹y = f x› show "y ∈ f ` s" by (rule ssubst) qed moreover note ‹y ∈ f ` (s ∩ t)› then have "y ∈ f ` t" proof (rule imageE) fix x assume "y = f x" assume "x ∈ s ∩ t" have "x ∈ t" using ‹x ∈ s ∩ t› by (rule IntD2) then have "f x ∈ f ` t" by (rule imageI) with ‹y = f x› show "y ∈ f ` t" by (rule ssubst) qed ultimately show "y ∈ f ` s ∩ f ` t" by (rule IntI) qed (* 2ª demostración *) lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t" proof fix y assume "y ∈ f ` (s ∩ t)" then have "y ∈ f ` s" proof fix x assume "y = f x" assume "x ∈ s ∩ t" have "x ∈ s" using ‹x ∈ s ∩ t› by simp then have "f x ∈ f ` s" by simp with ‹y = f x› show "y ∈ f ` s" by simp qed moreover note ‹y ∈ f ` (s ∩ t)› then have "y ∈ f ` t" proof fix x assume "y = f x" assume "x ∈ s ∩ t" have "x ∈ t" using ‹x ∈ s ∩ t› by simp then have "f x ∈ f ` t" by simp with ‹y = f x› show "y ∈ f ` t" by simp qed ultimately show "y ∈ f ` s ∩ f ` t" by simp qed (* 3ª demostración *) lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t" proof fix y assume "y ∈ f ` (s ∩ t)" then obtain x where hx : "y = f x ∧ x ∈ s ∩ t" by auto then have "y = f x" by simp have "x ∈ s" using hx by simp have "x ∈ t" using hx by simp have "y ∈ f ` s" using ‹y = f x› ‹x ∈ s› by simp moreover have "y ∈ f ` t" using ‹y = f x› ‹x ∈ t› by simp ultimately show "y ∈ f ` s ∩ f ` t" by simp qed (* 4ª demostración *) lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t" by (simp only: image_Int_subset) (* 5ª demostración *) lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t" by auto end |
8. Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]
Demostrar con Lean4 que si \(f\) es inyectiva, entonces
\[ f[s] ∩ f[t] ⊆ f[s ∩ t] \]
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Set.Function open Set Function variable {α β : Type _} variable (f : α → β) variable (s t : Set α) example (h : Injective f) : f '' s ∩ f '' t ⊆ f '' (s ∩ t) := by sorry |
8.1. Demostración en lenguaje natural
Sea \(y ∈ f[s] ∩ f[t]\). Entonces, existen \(x₁\) y \(x₂\) tales que
\begin{align}
&x₁ ∈ s \tag{1} \\
&f(x₁) = y \tag{2} \\
&x₂ ∈ t \tag{3} \\
&f(x₂) = y \tag{4}
\end{align}
De (2) y (4) se tiene que
\[ f(x₁) = f(x₂) \]
y, por ser \(f\) inyectiva, se tiene que
\[ x₁ = x₂ \]
y, por (1), se tiene que
\[ x₂ ∈ t \]
y, por (3), se tiene que
\[ x₂ ∈ s ∩ t \]
Por tanto,
\[ f(x₂) ∈ f[s ∩ t] \]
y, por (4),
\[ y ∈ f[s ∩ t] \]
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 115 116 117 118 119 |
import Mathlib.Data.Set.Function open Set Function variable {α β : Type _} variable (f : α → β) variable (s t : Set α) -- 1ª demostración -- =============== example (h : Injective f) : f '' s ∩ f '' t ⊆ f '' (s ∩ t) := by intros y hy -- y : β -- hy : y ∈ f '' s ∩ f '' t -- ⊢ y ∈ f '' (s ∩ t) rcases hy with ⟨hy1, hy2⟩ -- hy1 : y ∈ f '' s -- hy2 : y ∈ f '' t rcases hy1 with ⟨x1, hx1⟩ -- x1 : α -- hx1 : x1 ∈ s ∧ f x1 = y rcases hx1 with ⟨x1s, fx1y⟩ -- x1s : x1 ∈ s -- fx1y : f x1 = y rcases hy2 with ⟨x2, hx2⟩ -- x2 : α -- hx2 : x2 ∈ t ∧ f x2 = y rcases hx2 with ⟨x2t, fx2y⟩ -- x2t : x2 ∈ t -- fx2y : f x2 = y have h1 : f x1 = f x2 := Eq.trans fx1y fx2y.symm have h2 : x1 = x2 := h (congrArg f (h h1)) have h3 : x2 ∈ s := by rwa [h2] at x1s have h4 : x2 ∈ s ∩ t := by exact ⟨h3, x2t⟩ have h5 : f x2 ∈ f '' (s ∩ t) := mem_image_of_mem f h4 show y ∈ f '' (s ∩ t) rwa [fx2y] at h5 -- 2ª demostración -- =============== example (h : Injective f) : f '' s ∩ f '' t ⊆ f '' (s ∩ t) := by intros y hy -- y : β -- hy : y ∈ f '' s ∩ f '' t -- ⊢ y ∈ f '' (s ∩ t) rcases hy with ⟨hy1, hy2⟩ -- hy1 : y ∈ f '' s -- hy2 : y ∈ f '' t rcases hy1 with ⟨x1, hx1⟩ -- x1 : α -- hx1 : x1 ∈ s ∧ f x1 = y rcases hx1 with ⟨x1s, fx1y⟩ -- x1s : x1 ∈ s -- fx1y : f x1 = y rcases hy2 with ⟨x2, hx2⟩ -- x2 : α -- hx2 : x2 ∈ t ∧ f x2 = y rcases hx2 with ⟨x2t, fx2y⟩ -- x2t : x2 ∈ t -- fx2y : f x2 = y use x1 -- ⊢ x1 ∈ s ∩ t ∧ f x1 = y constructor . -- ⊢ x1 ∈ s ∩ t constructor . -- ⊢ x1 ∈ s exact x1s . -- ⊢ x1 ∈ t convert x2t -- ⊢ x1 = x2 apply h -- ⊢ f x1 = f x2 rw [← fx2y] at fx1y -- fx1y : f x1 = f x2 exact fx1y . -- ⊢ f x1 = y exact fx1y -- 3ª demostración -- =============== example (h : Injective f) : f '' s ∩ f '' t ⊆ f '' (s ∩ t) := by rintro y ⟨⟨x1, x1s, fx1y⟩, ⟨x2, x2t, fx2y⟩⟩ -- y : β -- x1 : α -- x1s : x1 ∈ s -- fx1y : f x1 = y -- x2 : α -- x2t : x2 ∈ t -- fx2y : f x2 = y -- ⊢ y ∈ f '' (s ∩ t) use x1 -- ⊢ x1 ∈ s ∩ t ∧ f x1 = y constructor . -- ⊢ x1 ∈ s ∩ t constructor . -- ⊢ x1 ∈ s exact x1s . -- ⊢ x1 ∈ t convert x2t -- ⊢ x1 = x2 apply h -- ⊢ f x1 = f x2 rw [← fx2y] at fx1y -- fx1y : f x1 = f x2 exact fx1y . -- ⊢ f x1 = y exact fx1y |
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 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 |
theory Imagen_de_la_interseccion_de_aplicaciones_inyectivas imports Main begin (* 1ª demostración *) lemma assumes "inj f" shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)" proof (rule subsetI) fix y assume "y ∈ f ` s ∩ f ` t" then have "y ∈ f ` s" by (rule IntD1) then show "y ∈ f ` (s ∩ t)" proof (rule imageE) fix x assume "y = f x" assume "x ∈ s" have "x ∈ t" proof - have "y ∈ f ` t" using ‹y ∈ f ` s ∩ f ` t› by (rule IntD2) then show "x ∈ t" proof (rule imageE) fix z assume "y = f z" assume "z ∈ t" have "f x = f z" using ‹y = f x› ‹y = f z› by (rule subst) with ‹inj f› have "x = z" by (simp only: inj_eq) then show "x ∈ t" using ‹z ∈ t› by (rule ssubst) qed qed with ‹x ∈ s› have "x ∈ s ∩ t" by (rule IntI) with ‹y = f x› show "y ∈ f ` (s ∩ t)" by (rule image_eqI) qed qed (* 2ª demostración *) lemma assumes "inj f" shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)" proof fix y assume "y ∈ f ` s ∩ f ` t" then have "y ∈ f ` s" by simp then show "y ∈ f ` (s ∩ t)" proof fix x assume "y = f x" assume "x ∈ s" have "x ∈ t" proof - have "y ∈ f ` t" using ‹y ∈ f ` s ∩ f ` t› by simp then show "x ∈ t" proof fix z assume "y = f z" assume "z ∈ t" have "f x = f z" using ‹y = f x› ‹y = f z› by simp with ‹inj f› have "x = z" by (simp only: inj_eq) then show "x ∈ t" using ‹z ∈ t› by simp qed qed with ‹x ∈ s› have "x ∈ s ∩ t" by simp with ‹y = f x› show "y ∈ f ` (s ∩ t)" by simp qed qed (* 3ª demostración *) lemma assumes "inj f" shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)" using assms by (simp only: image_Int) (* 4ª demostración *) lemma assumes "inj f" shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)" using assms unfolding inj_def by auto end |
9. f[s] \ f[t] ⊆ f[s \ t]
Demostrar con Lean4 que
\[f[s] \setminus f[t] ⊆ f[s \setminus t] \]
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable {α β : Type _} variable (f : α → β) variable (s t : Set α) example : f '' s \ f '' t ⊆ f '' (s \ t) := by sorry |
9.1. Demostración en lenguaje natural
Sea \(y ∈ f[s] \setminus f[t]\). Entonces,
\begin{align}
&y ∈ f[s] \tag{1} \\
&y ∉ f[t] \tag{2}
\end{align}
Por (1), existe un \(x\) tal que
\begin{align}
&x ∈ s \tag{3} \\
&f(x) = y \tag{4}
\end{align}
Por tanto, para demostrar que \(y ∈ f[s \setminus t]\), basta probar que \(x ∉ t\). Para ello, supongamos que \(x ∈ t\). Entonces, por (4), \(y ∈ f[t]\), en contradicción con (2).
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 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 |
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable {α β : Type _} variable (f : α → β) variable (s t : Set α) -- 1ª demostración -- =============== example : f '' s \ f '' t ⊆ f '' (s \ t) := by intros y hy -- y : β -- hy : y ∈ f '' s \ f '' t -- ⊢ y ∈ f '' (s \ t) rcases hy with ⟨yfs, ynft⟩ -- yfs : y ∈ f '' s -- ynft : ¬y ∈ f '' t rcases yfs with ⟨x, hx⟩ -- x : α -- hx : x ∈ s ∧ f x = y rcases hx with ⟨xs, fxy⟩ -- xs : x ∈ s -- fxy : f x = y have h1 : x ∉ t := by intro xt -- xt : x ∈ t -- ⊢ False have h2 : f x ∈ f '' t := mem_image_of_mem f xt have h3 : y ∈ f '' t := by rwa [fxy] at h2 show False exact ynft h3 have h4 : x ∈ s \ t := mem_diff_of_mem xs h1 have h5 : f x ∈ f '' (s \ t) := mem_image_of_mem f h4 show y ∈ f '' (s \ t) rwa [fxy] at h5 -- 2ª demostración -- =============== example : f '' s \ f '' t ⊆ f '' (s \ t) := by intros y hy -- y : β -- hy : y ∈ f '' s \ f '' t -- ⊢ y ∈ f '' (s \ t) rcases hy with ⟨yfs, ynft⟩ -- yfs : y ∈ f '' s -- ynft : ¬y ∈ f '' t rcases yfs with ⟨x, hx⟩ -- x : α -- hx : x ∈ s ∧ f x = y rcases hx with ⟨xs, fxy⟩ -- xs : x ∈ s -- fxy : f x = y use x -- ⊢ x ∈ s \ t ∧ f x = y constructor . -- ⊢ x ∈ s \ t constructor . -- ⊢ x ∈ s exact xs . -- ⊢ ¬x ∈ t intro xt -- xt : x ∈ t -- ⊢ False apply ynft -- ⊢ y ∈ f '' t rw [←fxy] -- ⊢ f x ∈ f '' t apply mem_image_of_mem -- ⊢ x ∈ t exact xt . -- ⊢ f x = y exact fxy -- 3ª demostración -- =============== example : f '' s \ f '' t ⊆ f '' (s \ t) := by rintro y ⟨⟨x, xs, fxy⟩, ynft⟩ -- y : β -- ynft : ¬y ∈ f '' t -- x : α -- xs : x ∈ s -- fxy : f x = y -- ⊢ y ∈ f '' (s \ t) use x -- ⊢ x ∈ s \ t ∧ f x = y aesop -- 4ª demostración -- =============== example : f '' s \ f '' t ⊆ f '' (s \ t) := fun y ⟨⟨x, xs, fxy⟩, ynft⟩ ↦ ⟨x, by aesop⟩ -- 5ª demostración -- =============== example : f '' s \ f '' t ⊆ f '' (s \ t) := subset_image_diff f s t -- Lemmas usados -- ============= -- variable (x : α) -- #check (mem_image_of_mem f : x ∈ s → f x ∈ f '' s) -- #check (subset_image_diff f s t : f '' s \ f '' t ⊆ f '' (s \ t)) |
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 |
theory Imagen_de_la_diferencia_de_conjuntos imports Main begin (* 1ª demostración *) lemma "f ` s - f ` t ⊆ f ` (s - t)" proof (rule subsetI) fix y assume hy : "y ∈ f ` s - f ` t" then show "y ∈ f ` (s - t)" proof (rule DiffE) assume "y ∈ f ` s" assume "y ∉ f ` t" note ‹y ∈ f ` s› then show "y ∈ f ` (s - t)" proof (rule imageE) fix x assume "y = f x" assume "x ∈ s" have ‹x ∉ t› proof (rule notI) assume "x ∈ t" then have "f x ∈ f ` t" by (rule imageI) with ‹y = f x› have "y ∈ f ` t" by (rule ssubst) with ‹y ∉ f ` t› show False by (rule notE) qed with ‹x ∈ s› have "x ∈ s - t" by (rule DiffI) then have "f x ∈ f ` (s - t)" by (rule imageI) with ‹y = f x› show "y ∈ f ` (s - t)" by (rule ssubst) qed qed qed (* 2ª demostración *) lemma "f ` s - f ` t ⊆ f ` (s - t)" proof fix y assume hy : "y ∈ f ` s - f ` t" then show "y ∈ f ` (s - t)" proof assume "y ∈ f ` s" assume "y ∉ f ` t" note ‹y ∈ f ` s› then show "y ∈ f ` (s - t)" proof fix x assume "y = f x" assume "x ∈ s" have ‹x ∉ t› proof assume "x ∈ t" then have "f x ∈ f ` t" by simp with ‹y = f x› have "y ∈ f ` t" by simp with ‹y ∉ f ` t› show False by simp qed with ‹x ∈ s› have "x ∈ s - t" by simp then have "f x ∈ f ` (s - t)" by simp with ‹y = f x› show "y ∈ f ` (s - t)" by simp qed qed qed (* 3ª demostración *) lemma "f ` s - f ` t ⊆ f ` (s - t)" by (simp only: image_diff_subset) (* 4ª demostración *) lemma "f ` s - f ` t ⊆ f ` (s - t)" by auto end |
10. f[s] ∩ t = f[s ∩ f⁻¹[t]]
Demostrar con Lean4 que
\[ f[s] ∩ t = f[s ∩ f⁻¹[t]] \]
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable {α β : Type _} variable (f : α → β) variable (s : Set α) variable (t : Set β) example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) := by sorry |
10.1. Demostración en lenguaje natural
Tenemos que demostrar que, para toda \(y\),
\[ y ∈ f[s] ∩ t ↔ y ∈ f[s ∩ f⁻¹[t]] \]
Lo haremos probando las dos implicaciones.
(⟹) Supongamos que \(y ∈ f[s] ∩ t\). Entonces, se tiene que
\begin{align}
&y ∈ f[s] \tag{1} \\
&y ∈ t \tag{2}
\end{align}
Por (1), existe un \(x\) tal que
\begin{align}
&x ∈ s \tag{3} \\
&f(x) = y \tag{4}
\end{align}
Por (2) y (4),
\[ f(x) ∈ t \]
y, por tanto,
\[ x ∈ f⁻¹[t] \]
que, junto con (3), da
\{ x ∈ s ∩ f⁻¹[t] \]
y, por tanto,
\[ f(x) ∈ f[s ∩ f⁻¹[t]] \]
que, junto con (4), da
\[ y ∈ f[s ∩ f⁻¹[t]] \]
(⟸) Supongamos que \(y ∈ f[s ∩ f⁻¹[t]]\). Entonces, existe un \(x\) tal que
\begin{align}
&x ∈ s ∩ f⁻¹[t] \tag{5} \\
&f(x) = y \tag{6}
\end{align}
Por (1), se tiene que
\begin{align}
&x ∈ s \tag{7} \\
&x ∈ f⁻¹[t] \tag{8}
\end{align}
Por (7) se tiene que
\[ f(x) ∈ f[s] \]
y, junto con (6), se tiene que
\[ y ∈ f[s] \tag{9} \]
Por (8), se tiene que
\[ f(x) ∈ t \]
y, junto con (6), se tiene que
\[ y ∈ t \tag{10} \]
Por (9) y (19), se tiene que
\[ y ∈ f[s] ∩ t \]
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 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 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 |
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable {α β : Type _} variable (f : α → β) variable (s : Set α) variable (t : Set β) -- 1ª demostración -- =============== example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) := by ext y -- y : β -- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t) have h1 : y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t) := by intro hy -- hy : y ∈ f '' s ∩ t -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) have h1a : y ∈ f '' s := hy.1 obtain ⟨x : α, hx: x ∈ s ∧ f x = y⟩ := h1a have h1b : x ∈ s := hx.1 have h1c : f x = y := hx.2 have h1d : y ∈ t := hy.2 have h1e : f x ∈ t := by rwa [←h1c] at h1d have h1f : x ∈ s ∩ f ⁻¹' t := mem_inter h1b h1e have h1g : f x ∈ f '' (s ∩ f ⁻¹' t) := mem_image_of_mem f h1f show y ∈ f '' (s ∩ f ⁻¹' t) rwa [h1c] at h1g have h2 : y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t := by intro hy -- hy : y ∈ f '' (s ∩ f ⁻¹' t) -- ⊢ y ∈ f '' s ∩ t obtain ⟨x : α, hx : x ∈ s ∩ f ⁻¹' t ∧ f x = y⟩ := hy have h2a : x ∈ s := hx.1.1 have h2b : f x ∈ f '' s := mem_image_of_mem f h2a have h2c : y ∈ f '' s := by rwa [hx.2] at h2b have h2d : x ∈ f ⁻¹' t := hx.1.2 have h2e : f x ∈ t := mem_preimage.mp h2d have h2f : y ∈ t := by rwa [hx.2] at h2e show y ∈ f '' s ∩ t exact mem_inter h2c h2f show y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t) exact ⟨h1, h2⟩ -- 2ª demostración -- =============== example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) := by ext y -- y : β -- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t) constructor . -- ⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t) intro hy -- hy : y ∈ f '' s ∩ t -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) cases' hy with hyfs yt -- hyfs : y ∈ f '' s -- yt : y ∈ t cases' hyfs with x hx -- x : α -- hx : x ∈ s ∧ f x = y cases' hx with xs fxy -- xs : x ∈ s -- fxy : f x = y use x -- ⊢ x ∈ s ∩ f ⁻¹' t ∧ f x = y constructor . -- ⊢ x ∈ s ∩ f ⁻¹' t constructor . -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ f ⁻¹' t rw [mem_preimage] -- ⊢ f x ∈ t rw [fxy] -- ⊢ y ∈ t exact yt . -- ⊢ f x = y exact fxy . -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t intro hy -- hy : y ∈ f '' (s ∩ f ⁻¹' t) -- ⊢ y ∈ f '' s ∩ t cases' hy with x hx -- x : α -- hx : x ∈ s ∩ f ⁻¹' t ∧ f x = y constructor . -- ⊢ y ∈ f '' s use x -- ⊢ x ∈ s ∧ f x = y constructor . -- ⊢ x ∈ s exact hx.1.1 . -- ⊢ f x = y exact hx.2 . -- ⊢ y ∈ t cases' hx with hx1 fxy -- hx1 : x ∈ s ∩ f ⁻¹' t -- fxy : f x = y rw [←fxy] -- ⊢ f x ∈ t rw [←mem_preimage] -- ⊢ x ∈ f ⁻¹' t exact hx1.2 -- 3ª demostración -- =============== example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) := by ext y -- y : β -- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t) constructor . -- ⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t) rintro ⟨⟨x, xs, fxy⟩, yt⟩ -- yt : y ∈ t -- x : α -- xs : x ∈ s -- fxy : f x = y -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) use x -- ⊢ x ∈ s ∩ f ⁻¹' t ∧ f x = y constructor . -- ⊢ x ∈ s ∩ f ⁻¹' t constructor . -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ f ⁻¹' t rw [mem_preimage] -- ⊢ f x ∈ t rw [fxy] -- ⊢ y ∈ t exact yt . -- ⊢ f x = y exact fxy . -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t rintro ⟨x, ⟨xs, xt⟩, fxy⟩ -- x : α -- fxy : f x = y -- xs : x ∈ s -- xt : x ∈ f ⁻¹' t -- ⊢ y ∈ f '' s ∩ t constructor . -- ⊢ y ∈ f '' s use x, xs -- ⊢ f x = y exact fxy . -- ⊢ y ∈ t rw [←fxy] -- ⊢ f x ∈ t rw [←mem_preimage] -- ⊢ x ∈ f ⁻¹' t exact xt -- 4ª demostración -- =============== example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) := by ext y -- y : β -- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t) constructor . -- ⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t) rintro ⟨⟨x, xs, fxy⟩, yt⟩ -- yt : y ∈ t -- x : α -- xs : x ∈ s -- fxy : f x = y -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) aesop . -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t rintro ⟨x, ⟨xs, xt⟩, fxy⟩ -- x : α -- fxy : f x = y -- xs : x ∈ s -- xt : x ∈ f ⁻¹' t -- ⊢ y ∈ f '' s ∩ t aesop -- 5ª demostración -- =============== example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) := by ext ; constructor <;> aesop -- 6ª demostración -- =============== example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) := (image_inter_preimage f s t).symm -- Lemas usados -- ============ -- variable (x : α) -- variable (v : Set α) -- #check (image_inter_preimage f s t : f '' (s ∩ f ⁻¹' t) = f '' s ∩ t) -- #check (mem_image_of_mem f : x ∈ s → f x ∈ f '' s) -- #check (mem_inter : x ∈ s → x ∈ v → x ∈ s ∩ v) -- #check (mem_preimage : x ∈ f ⁻¹' t ↔ f x ∈ t) |
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 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 |
theory Interseccion_con_la_imagen imports Main begin (* 1ª demostración *) lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)" proof (rule equalityI) show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)" proof (rule subsetI) fix y assume "y ∈ (f ` s) ∩ v" then show "y ∈ f ` (s ∩ f -` v)" proof (rule IntE) assume "y ∈ v" assume "y ∈ f ` s" then show "y ∈ f ` (s ∩ f -` v)" proof (rule imageE) fix x assume "x ∈ s" assume "y = f x" then have "f x ∈ v" using ‹y ∈ v› by (rule subst) then have "x ∈ f -` v" by (rule vimageI2) with ‹x ∈ s› have "x ∈ s ∩ f -` v" by (rule IntI) then have "f x ∈ f ` (s ∩ f -` v)" by (rule imageI) with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)" by (rule ssubst) qed qed qed next show "f ` (s ∩ f -` v) ⊆ (f ` s) ∩ v" proof (rule subsetI) fix y assume "y ∈ f ` (s ∩ f -` v)" then show "y ∈ (f ` s) ∩ v" proof (rule imageE) fix x assume "y = f x" assume hx : "x ∈ s ∩ f -` v" have "y ∈ f ` s" proof - have "x ∈ s" using hx by (rule IntD1) then have "f x ∈ f ` s" by (rule imageI) with ‹y = f x› show "y ∈ f ` s" by (rule ssubst) qed moreover have "y ∈ v" proof - have "x ∈ f -` v" using hx by (rule IntD2) then have "f x ∈ v" by (rule vimageD) with ‹y = f x› show "y ∈ v" by (rule ssubst) qed ultimately show "y ∈ (f ` s) ∩ v" by (rule IntI) qed qed qed (* 2ª demostración *) lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)" proof show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)" proof fix y assume "y ∈ (f ` s) ∩ v" then show "y ∈ f ` (s ∩ f -` v)" proof assume "y ∈ v" assume "y ∈ f ` s" then show "y ∈ f ` (s ∩ f -` v)" proof fix x assume "x ∈ s" assume "y = f x" then have "f x ∈ v" using ‹y ∈ v› by simp then have "x ∈ f -` v" by simp with ‹x ∈ s› have "x ∈ s ∩ f -` v" by simp then have "f x ∈ f ` (s ∩ f -` v)" by simp with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)" by simp qed qed qed next show "f ` (s ∩ f -` v) ⊆ (f ` s) ∩ v" proof fix y assume "y ∈ f ` (s ∩ f -` v)" then show "y ∈ (f ` s) ∩ v" proof fix x assume "y = f x" assume hx : "x ∈ s ∩ f -` v" have "y ∈ f ` s" proof - have "x ∈ s" using hx by simp then have "f x ∈ f ` s" by simp with ‹y = f x› show "y ∈ f ` s" by simp qed moreover have "y ∈ v" proof - have "x ∈ f -` v" using hx by simp then have "f x ∈ v" by simp with ‹y = f x› show "y ∈ v" by simp qed ultimately show "y ∈ (f ` s) ∩ v" by simp qed qed qed (* 3ª demostración *) lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)" proof show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)" proof fix y assume "y ∈ (f ` s) ∩ v" then show "y ∈ f ` (s ∩ f -` v)" proof assume "y ∈ v" assume "y ∈ f ` s" then show "y ∈ f ` (s ∩ f -` v)" proof fix x assume "x ∈ s" assume "y = f x" then show "y ∈ f ` (s ∩ f -` v)" using ‹x ∈ s› ‹y ∈ v› by simp qed qed qed next show "f ` (s ∩ f -` v) ⊆ (f ` s) ∩ v" proof fix y assume "y ∈ f ` (s ∩ f -` v)" then show "y ∈ (f ` s) ∩ v" proof fix x assume "y = f x" assume hx : "x ∈ s ∩ f -` v" then have "y ∈ f ` s" using ‹y = f x› by simp moreover have "y ∈ v" using hx ‹y = f x› by simp ultimately show "y ∈ (f ` s) ∩ v" by simp qed qed qed (* 4ª demostración *) lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)" by auto end |