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