Intersección con la imagen
Demostrar con Lean4 que \[ f[s] ∩ t = f[s ∩ f⁻¹[t]] \]
Para ello, completar la siguiente teoría de Lean4:
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
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 \]
2. Demostraciones con Lean4
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 . -- ⊢ 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.
3. Demostraciones con Isabelle/HOL
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