20 junio 2021 – Calculemus

Unión con la imagen

PorJosé A. Alonso 20 junio 202114 junio 2021

Demostrar que

   f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v

1	f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v

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

import data.set.basic
import tactic

open set

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

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=
sorry

import data.set.basic

import tactic

open set

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

variable f : α → β

variable s : set α

variable v : set β

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

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

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

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=
begin
  intros y hy,
  cases hy with x hx,
  cases hx with hx1 fxy,
  cases hx1 with xs xv,
  { left,
    use x,
    split,
    { exact xs, },
    { exact fxy, }},
  { right,
    rw ← fxy,
    exact xv, },
end

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

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=
begin
  rintros y ⟨x, xs | xv, fxy⟩,
  { left,
    use [x, xs, fxy], },
  { right,
    rw ← fxy,
    exact xv, },
end

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

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=
begin
  rintros y ⟨x, xs | xv, fxy⟩;
  finish,
end

import data.set.basic

import tactic

open set

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

variable f : α → β

variable s : set α

variable v : set β

-- 1ª demostración

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

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=

begin

intros y hy,

cases hy with x hx,

cases hx with hx1 fxy,

cases hx1 with xs xv,

{ left,

use x,

split,

{ exact xs, },

{ exact fxy, }},

{ right,

rw ← fxy,

exact xv, },

end

-- 2ª demostración

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

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=

begin

rintros y ⟨x, xs | xv, fxy⟩,

{ left,

use [x, xs, fxy], },

{ right,

rw ← fxy,

exact xv, },

end

-- 3ª demostración

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

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=

begin

rintros y ⟨x, xs | xv, fxy⟩;

finish,

end

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

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

theory Union_con_la_imagen
imports Main
begin

(* 1ª demostración *)

lemma "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 "x ∈ s ∪ f -` v"
    then show "y ∈ f ` s ∪ v"
    proof (rule UnE)
      assume "x ∈ s"
      then have "f x ∈ f ` s"
        by (rule imageI)
      with ‹y = f x› have "y ∈ f ` s"
        by (rule ssubst)
      then show "y ∈ f ` s ∪ v"
        by (rule UnI1)
    next
      assume "x ∈ f -` v"
      then have "f x ∈ v"
        by (rule vimageD)
      with ‹y = f x› have "y ∈ v"
        by (rule ssubst)
      then show "y ∈ f ` s ∪ v"
        by (rule UnI2)
    qed
  qed
qed

(* 2ª demostración *)

lemma "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 "x ∈ s ∪ f -` v"
    then show "y ∈ f ` s ∪ v"
    proof
      assume "x ∈ s"
      then have "f x ∈ f ` s" by simp
      with ‹y = f x› have "y ∈ f ` s" by simp
      then show "y ∈ f ` s ∪ v" by simp
    next
      assume "x ∈ f -` v"
      then have "f x ∈ v" by simp
      with ‹y = f x› have "y ∈ v" by simp
      then show "y ∈ f ` s ∪ v" by simp
    qed
  qed
qed

(* 3ª demostración *)

lemma "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 "x ∈ s ∪ f -` v"
    then show "y ∈ f ` s ∪ v"
    proof
      assume "x ∈ s"
      then show "y ∈ f ` s ∪ v" by (simp add: ‹y = f x›)
    next
      assume "x ∈ f -` v"
      then show "y ∈ f ` s ∪ v" by (simp add: ‹y = f x›)
    qed
  qed
qed

(* 4ª demostración *)

lemma "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 "x ∈ s ∪ f -` v"
    then show "y ∈ f ` s ∪ v" using ‹y = f x› by blast
  qed
qed

(* 5ª demostración *)

lemma "f ` (s ∪ f -` u) ⊆ f ` s ∪ u"
  by auto

end

100

101

102

103

104

105

theory Union_con_la_imagen

imports Main

begin

(* 1ª demostración *)

lemma "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 "x ∈ s ∪ f -` v"

then show "y ∈ f ` s ∪ v"

proof (rule UnE)

assume "x ∈ s"

then have "f x ∈ f ` s"

by (rule imageI)

with ‹y = f x› have "y ∈ f ` s"

by (rule ssubst)

then show "y ∈ f ` s ∪ v"

by (rule UnI1)

assume "x ∈ f -` v"

then have "f x ∈ v"

by (rule vimageD)

with ‹y = f x› have "y ∈ v"

by (rule ssubst)

then show "y ∈ f ` s ∪ v"

by (rule UnI2)

qed

(* 2ª demostración *)

lemma "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 "x ∈ s ∪ f -` v"

then show "y ∈ f ` s ∪ v"

proof

assume "x ∈ s"

then have "f x ∈ f ` s" by simp

with ‹y = f x› have "y ∈ f ` s" by simp

then show "y ∈ f ` s ∪ v" by simp

assume "x ∈ f -` v"

then have "f x ∈ v" by simp

with ‹y = f x› have "y ∈ v" by simp

then show "y ∈ f ` s ∪ v" by simp

qed

(* 3ª demostración *)

lemma "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 "x ∈ s ∪ f -` v"

then show "y ∈ f ` s ∪ v"

proof

assume "x ∈ s"

then show "y ∈ f ` s ∪ v" by (simp add: ‹y = f x›)

assume "x ∈ f -` v"

then show "y ∈ f ` s ∪ v" by (simp add: ‹y = f x›)

qed

(* 4ª demostración *)

lemma "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 "x ∈ s ∪ f -` v"

then show "y ∈ f ` s ∪ v" using ‹y = f x› by blast

qed

(* 5ª demostración *)

lemma "f ` (s ∪ f -` u) ⊆ f ` s ∪ u"

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]