Imagen de la intersección general
Demostrar con Lean4 que
\[ f\left[\bigcap_{i ∈ I} A_i\right] ⊆ \bigcap_{i ∈ I} f[A_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 (A : I → Set α) example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := by sorry |
1. Demostración en lenguaje natural
Sea \(y\) tal que
\[ y ∈ f\left[\bigcap_{i ∈ I} Aᵢ\right] \tag{1} \]
Tenemos que demostrar que
\[ y ∈ \bigcap_{i ∈ I} f[Aᵢ] \]
Para ello, sea \(i ∈ I\), tenemos que demostrar que \(y ∈ f[Aᵢ]\).
Por (1), existe un \(x\) tal que
\begin{align}
&x ∈ \bigcap_{i ∈ I} Aᵢ \tag{2} \\
&f(x) = y \tag{3}
\end{align}
Por (2),
\[ x ∈ Aᵢ \]
y, por tanto,
\[ f(x) ∈ f[Aᵢ] \]
que, junto con (3), da que
\[ y ∈ f[Aᵢ] \]
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 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α β I : Type _} variable (f : α → β) variable (A : I → Set α) -- 1ª demostración -- =============== example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := by intros y h -- y : β -- h : y ∈ f '' ⋂ (i : I), A i -- ⊢ y ∈ ⋂ (i : I), f '' A i have h1 : ∃ x, x ∈ ⋂ i, A i ∧ f x = y := (mem_image f (⋂ i, A i) y).mp h obtain ⟨x, hx : x ∈ ⋂ i, A i ∧ f x = y⟩ := h1 have h2 : x ∈ ⋂ i, A i := hx.1 have h3 : f x = y := hx.2 have h4 : ∀ i, y ∈ f '' A i := by intro i have h4a : x ∈ A i := mem_iInter.mp h2 i have h4b : f x ∈ f '' A i := mem_image_of_mem f h4a show y ∈ f '' A i rwa [h3] at h4b show y ∈ ⋂ i, f '' A i exact mem_iInter.mpr h4 -- 1ª demostración -- =============== example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := by intros y h -- y : β -- h : y ∈ f '' ⋂ (i : I), A i -- ⊢ y ∈ ⋂ (i : I), f '' A i apply mem_iInter_of_mem -- ⊢ ∀ (i : I), y ∈ f '' A i intro i -- i : I -- ⊢ y ∈ f '' A i cases' h with x hx -- x : α -- hx : x ∈ ⋂ (i : I), A i ∧ f x = y cases' hx with xIA fxy -- xIA : x ∈ ⋂ (i : I), A i -- fxy : f x = y rw [←fxy] -- ⊢ f x ∈ f '' A i apply mem_image_of_mem -- ⊢ x ∈ A i exact mem_iInter.mp xIA i -- 2ª demostración -- =============== example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := by intros y h -- y : β -- h : y ∈ f '' ⋂ (i : I), A i -- ⊢ y ∈ ⋂ (i : I), f '' A i apply mem_iInter_of_mem -- ⊢ ∀ (i : I), y ∈ f '' A i intro i -- i : I -- ⊢ y ∈ f '' A i rcases h with ⟨x, xIA, rfl⟩ -- x : α -- xIA : x ∈ ⋂ (i : I), A i -- ⊢ f x ∈ f '' A i exact mem_image_of_mem f (mem_iInter.mp xIA i) -- 3ª demostración -- =============== example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := by intro y -- y : β -- ⊢ y ∈ f '' ⋂ (i : I), A i → y ∈ ⋂ (i : I), f '' A i simp -- ⊢ ∀ (x : α), (∀ (i : I), x ∈ A i) → f x = y → ∀ (i : I), ∃ x, x ∈ A i ∧ f x = y intros x xIA fxy i -- x : α -- xIA : ∀ (i : I), x ∈ A i -- fxy : f x = y -- i : I -- ⊢ ∃ x, x ∈ A i ∧ f x = y use x, xIA i -- ⊢ f x = y exact fxy -- 4ª demostración -- =============== example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := image_iInter_subset A f -- Lemas usados -- ============ -- variable (x : α) -- variable (s : Set α) -- #check (image_iInter_subset A f : f '' ⋂ i, A i ⊆ ⋂ i, f '' A i) -- #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.
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 |
theory Imagen_de_la_interseccion_general imports Main begin (* 1ª demostración *) lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)" proof (rule subsetI) fix y assume "y ∈ f ` (⋂ i ∈ I. A i)" then show "y ∈ (⋂ i ∈ I. f ` A i)" proof (rule imageE) fix x assume "y = f x" assume xIA : "x ∈ (⋂ i ∈ I. A i)" have "f x ∈ (⋂ i ∈ I. f ` A i)" proof (rule INT_I) fix i assume "i ∈ I" with xIA have "x ∈ A i" by (rule INT_D) then show "f x ∈ f ` A i" by (rule imageI) qed with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)" by (rule ssubst) qed qed (* 2ª demostración *) lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)" proof fix y assume "y ∈ f ` (⋂ i ∈ I. A i)" then show "y ∈ (⋂ i ∈ I. f ` A i)" proof fix x assume "y = f x" assume xIA : "x ∈ (⋂ i ∈ I. A i)" have "f x ∈ (⋂ i ∈ I. f ` A i)" proof fix i assume "i ∈ I" with xIA have "x ∈ A i" by simp then show "f x ∈ f ` A i" by simp qed with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)" by simp qed qed (* 3ª demostración *) lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)" by blast end |
