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:

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

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)

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) :=

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) :=

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) :=

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

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

1. Demostración en lenguaje natural

2. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL

Share this:

Escribe un comentarioCancel reply