8 junio 2021 – Calculemus

Subconjunto de la imagen inversa

PorJosé A. Alonso 8 junio 202112 junio 2021

Demostrar que

   f[s] ⊆ u ↔ s ⊆ f⁻¹[u]

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

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

import data.set.basic

open set

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

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=
sorry

import data.set.basic

open set

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

variable f : α → β

variable s : set α

variable u : set β

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic

open set

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

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

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=
begin
  split,
  { intros h x xs,
    apply mem_preimage.mpr,
    apply h,
    apply mem_image_of_mem,
    exact xs, },
  { intros h y hy,
    rcases hy with ⟨x, xs, fxy⟩,
    rw ← fxy,
    exact h xs, },
end

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

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=
begin
  split,
  { intros h x xs,
    apply h,
    apply mem_image_of_mem,
    exact xs, },
  { rintros h y ⟨x, xs, rfl⟩,
    exact h xs, },
end

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

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=
image_subset_iff

-- 4ª demostración
-- ===============

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=
by simp

import data.set.basic

open set

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

variable f : α → β

variable s : set α

variable u : set β

-- 1ª demostración

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

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=

begin

split,

{ intros h x xs,

apply mem_preimage.mpr,

apply h,

apply mem_image_of_mem,

exact xs, },

{ intros h y hy,

rcases hy with ⟨x, xs, fxy⟩,

rw ← fxy,

exact h xs, },

end

-- 2ª demostración

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

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=

begin

split,

{ intros h x xs,

apply h,

apply mem_image_of_mem,

exact xs, },

{ rintros h y ⟨x, xs, rfl⟩,

exact h xs, },

end

-- 3ª demostración

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

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=

image_subset_iff

-- 4ª demostración

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

example : f '' s ⊆ u ↔ s ⊆ f ⁻¹' u :=

by simp

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

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

theory Subconjunto_de_la_imagen_inversa
imports Main
begin

section ‹1ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"
proof (rule iffI)
  assume "f ` s ⊆ u"
  show "s ⊆ f -` u"
  proof (rule subsetI)
    fix x
    assume "x ∈ s"
    then have "f x ∈ f ` s"
      by (simp only: imageI)
    then have "f x ∈ u"
      using ‹f ` s ⊆ u› by (rule set_rev_mp)
    then show "x ∈ f -` u"
      by (simp only: vimageI)
  qed
next
  assume "s ⊆ f -` u"
  show "f ` s ⊆ u"
  proof (rule subsetI)
    fix y
    assume "y ∈ f ` s"
    then show "y ∈ u"
    proof
      fix x
      assume "y = f x"
      assume "x ∈ s"
      then have "x ∈ f -` u"
        using ‹s ⊆ f -` u› by (rule set_rev_mp)
      then have "f x ∈ u"
        by (rule vimageD)
      with ‹y = f x› show "y ∈ u"
        by (rule ssubst)
    qed
  qed
qed

section ‹2ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"
proof
  assume "f ` s ⊆ u"
  show "s ⊆ f -` u"
  proof
    fix x
    assume "x ∈ s"
    then have "f x ∈ f ` s"
      by simp
    then have "f x ∈ u"
      using ‹f ` s ⊆ u› by (simp add: set_rev_mp)
    then show "x ∈ f -` u"
      by simp
  qed
next
  assume "s ⊆ f -` u"
  show "f ` s ⊆ u"
  proof
    fix y
    assume "y ∈ f ` s"
    then show "y ∈ u"
    proof
      fix x
      assume "y = f x"
      assume "x ∈ s"
      then have "x ∈ f -` u"
        using ‹s ⊆ f -` u› by (simp only: set_rev_mp)
      then have "f x ∈ u"
        by simp
      with ‹y = f x› show "y ∈ u"
        by simp
    qed
  qed
qed

section ‹3ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"
  by (simp only: image_subset_iff_subset_vimage)

section ‹4ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"
  by auto

end

theory Subconjunto_de_la_imagen_inversa

imports Main

begin

section ‹1ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"

proof (rule iffI)

assume "f ` s ⊆ u"

show "s ⊆ f -` u"

proof (rule subsetI)

fix x

assume "x ∈ s"

then have "f x ∈ f ` s"

by (simp only: imageI)

then have "f x ∈ u"

using ‹f ` s ⊆ u› by (rule set_rev_mp)

then show "x ∈ f -` u"

by (simp only: vimageI)

qed

assume "s ⊆ f -` u"

show "f ` s ⊆ u"

proof (rule subsetI)

fix y

assume "y ∈ f ` s"

then show "y ∈ u"

proof

fix x

assume "y = f x"

assume "x ∈ s"

then have "x ∈ f -` u"

using ‹s ⊆ f -` u› by (rule set_rev_mp)

then have "f x ∈ u"

by (rule vimageD)

with ‹y = f x› show "y ∈ u"

by (rule ssubst)

qed

section ‹2ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"

proof

assume "f ` s ⊆ u"

show "s ⊆ f -` u"

proof

fix x

assume "x ∈ s"

then have "f x ∈ f ` s"

by simp

then have "f x ∈ u"

using ‹f ` s ⊆ u› by (simp add: set_rev_mp)

then show "x ∈ f -` u"

by simp

qed

assume "s ⊆ f -` u"

show "f ` s ⊆ u"

proof

fix y

assume "y ∈ f ` s"

then show "y ∈ u"

proof

fix x

assume "y = f x"

assume "x ∈ s"

then have "x ∈ f -` u"

using ‹s ⊆ f -` u› by (simp only: set_rev_mp)

then have "f x ∈ u"

by simp

with ‹y = f x› show "y ∈ u"

by simp

qed

section ‹3ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"

by (simp only: image_subset_iff_subset_vimage)

section ‹4ª demostración›

lemma "f ` s ⊆ u ⟷ s ⊆ f -` u"

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]