Imagen_de_imagen_inversa_de_aplicaciones_suprayectivas.md

Título	Autor
Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]].	José A. Alonso

[mathjax]

Demostrar con Lean4 que si \(f\) es suprayectiva, entonces \[ u ⊆ f[f⁻¹[u]] \]

Para ello, completar la siguiente teoría de Lean4:

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

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

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