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 |
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. 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.
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 |
