11 junio 2021 – Calculemus

Imagen de imagen inversa de aplicaciones suprayectivas

PorJosé A. Alonso 11 junio 202112 junio 2021

Demostrar que si f es suprayectiva, entonces

   u ⊆ f[f⁻¹[u]]

1	u ⊆ f[f⁻¹[u]]

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

import data.set.basic
open set function

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  u : set β

example
  (h : surjective f)
  : u ⊆ f '' (f⁻¹' u) :=
sorry

import data.set.basic

open set function

variables {α : Type*} {β : Type*}

variable f : α → β

variable u : set β

example

(h : surjective f)

: u ⊆ f '' (f⁻¹' u) :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
open set function

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  u : set β

-- 1ª demostración
-- ===============

example
  (h : surjective f)
  : u ⊆ f '' (f⁻¹' u) :=
begin
  intros y yu,
  cases h y with x fxy,
  use x,
  split,
  { apply mem_preimage.mpr,
    rw fxy,
    exact yu },
  { exact fxy },
end

-- 2ª demostración
-- ===============

example
  (h : surjective f)
  : u ⊆ f '' (f⁻¹' u) :=
begin
  intros y yu,
  cases h y with x fxy,
  use x,
  split,
  { show f x ∈ u,
    rw fxy,
    exact yu },
  { exact fxy },
end

-- 3ª demostración
-- ===============

example
  (h : surjective f)
  : u ⊆ f '' (f⁻¹' u) :=
begin
  intros y yu,
  cases h y with x fxy,
  by finish,
end

import data.set.basic

open set function

variables {α : Type*} {β : Type*}

variable f : α → β

variable u : set β

-- 1ª demostración

-- ===============

example

(h : surjective f)

: u ⊆ f '' (f⁻¹' u) :=

begin

intros y yu,

cases h y with x fxy,

use x,

split,

{ apply mem_preimage.mpr,

rw fxy,

exact yu },

{ exact fxy },

end

-- 2ª demostración

-- ===============

example

(h : surjective f)

: u ⊆ f '' (f⁻¹' u) :=

begin

intros y yu,

cases h y with x fxy,

use x,

split,

{ show f x ∈ u,

rw fxy,

exact yu },

{ exact fxy },

end

-- 3ª demostración

-- ===============

example

(h : surjective f)

: u ⊆ f '' (f⁻¹' u) :=

begin

intros y yu,

cases h y with x fxy,

by finish,

end

Se puede interactuar con la prueba anterior en esta sesión con Lean,
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Imagen_de_imagen_inversa_de_aplicaciones_suprayectivas
imports Main
begin

section ‹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

section ‹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

section ‹3ª demostración›

lemma
  assumes "surj f"
  shows "u ⊆ f ` (f -` u)"
  using assms
  by (simp only: surj_image_vimage_eq)

section ‹4ª demostración›

lemma
  assumes "surj f"
  shows "u ⊆ f ` (f -` u)"
  using assms
  unfolding surj_def
  by auto

section ‹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

section ‹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

section ‹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

section ‹3ª demostración›

lemma

assumes "surj f"

shows "u ⊆ f ` (f -` u)"

using assms

by (simp only: surj_image_vimage_eq)

section ‹4ª demostración›

lemma

assumes "surj f"

shows "u ⊆ f ` (f -` u)"

using assms

unfolding surj_def

by auto

section ‹5ª demostración›

lemma

assumes "surj f"

shows "u ⊆ f ` (f -` u)"

using assms

by auto

end

[/expand]

[expand title=»Nuevas soluciones»]

En los comentarios se pueden escribir nuevas soluciones.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

[/expand]