junio 2021 – Página 2

Intersección con la imagen

PorJosé A. Alonso 19 junio 202113 junio 2021

Demostrar que

   f[s] ∩ v = f[s ∩ f⁻¹[v]]

1	f[s] ∩ v = f[s ∩ f⁻¹[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) ∩ v = f '' (s ∩ f ⁻¹' v) :=
sorry

import data.set.basic

import tactic

open set

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

variable f : α → β

variable s : set α

variable v : set β

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' 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) ∩ v = f '' (s ∩ f ⁻¹' v) :=
begin
  ext y,
  split,
  { intro hy,
    cases hy with hyfs yv,
    cases hyfs with x hx,
    cases hx with xs fxy,
    use x,
    split,
    { split,
      { exact xs, },
      { rw mem_preimage,
        rw fxy,
        exact yv, }},
    { exact fxy, }},
  { intro hy,
    cases hy with x hx,
    split,
    { use x,
      split,
      { exact hx.1.1, },
      { exact hx.2, }},
    { cases hx with hx1 fxy,
      rw ← fxy,
      rw ← mem_preimage,
      exact hx1.2, }},
end

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

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=
begin
  ext y,
  split,
  { rintros ⟨⟨x, xs, fxy⟩, yv⟩,
    use x,
    split,
    { split,
      { exact xs, },
      { rw mem_preimage,
        rw fxy,
        exact yv, }},
    { exact fxy, }},
  { rintros ⟨x, ⟨xs, xv⟩, fxy⟩,
    split,
    { use [x, xs, fxy], },
    { rw ← fxy,
      rw ← mem_preimage,
      exact xv, }},
end

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

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=
begin
  ext y,
  split,
  { rintros ⟨⟨x, xs, fxy⟩, yv⟩,
    finish, },
  { rintros ⟨x, ⟨xs, xv⟩, fxy⟩,
    finish, },
end

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

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=
by ext ; split ; finish

-- 5ª demostración
-- ===============

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=
by finish [ext_iff, iff_def]

-- 6ª demostración
-- ===============

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=
(image_inter_preimage f s v).symm

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) ∩ v = f '' (s ∩ f ⁻¹' v) :=

begin

ext y,

split,

{ intro hy,

cases hy with hyfs yv,

cases hyfs with x hx,

cases hx with xs fxy,

use x,

split,

{ split,

{ exact xs, },

{ rw mem_preimage,

rw fxy,

exact yv, }},

{ exact fxy, }},

{ intro hy,

cases hy with x hx,

split,

{ use x,

split,

{ exact hx.1.1, },

{ exact hx.2, }},

{ cases hx with hx1 fxy,

rw ← fxy,

rw ← mem_preimage,

exact hx1.2, }},

end

-- 2ª demostración

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

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=

begin

ext y,

split,

{ rintros ⟨⟨x, xs, fxy⟩, yv⟩,

use x,

split,

{ split,

{ exact xs, },

{ rw mem_preimage,

rw fxy,

exact yv, }},

{ exact fxy, }},

{ rintros ⟨x, ⟨xs, xv⟩, fxy⟩,

split,

{ use [x, xs, fxy], },

{ rw ← fxy,

rw ← mem_preimage,

exact xv, }},

end

-- 3ª demostración

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

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=

begin

ext y,

split,

{ rintros ⟨⟨x, xs, fxy⟩, yv⟩,

finish, },

{ rintros ⟨x, ⟨xs, xv⟩, fxy⟩,

finish, },

end

-- 4ª demostración

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

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=

by ext ; split ; finish

-- 5ª demostración

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

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=

by finish [ext_iff, iff_def]

-- 6ª demostración

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

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=

(image_inter_preimage f s v).symm

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 Interseccion_con_la_imagen
imports Main
begin

(* 1ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
proof (rule equalityI)
  show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)"
  proof (rule subsetI)
    fix y
    assume "y ∈ (f ` s) ∩ v"
    then show "y ∈ f ` (s ∩ f -` v)"
    proof (rule IntE)
      assume "y ∈ v"
      assume "y ∈ f ` s"
      then show "y ∈ f ` (s ∩ f -` v)"
      proof (rule imageE)
        fix x
        assume "x ∈ s"
        assume "y = f x"
        then have "f x ∈ v"
          using ‹y ∈ v› by (rule subst)
        then have "x ∈ f -` v"
          by (rule vimageI2)
        with ‹x ∈ s› have "x ∈ s ∩ f -` v"
          by (rule IntI)
        then have "f x ∈ f ` (s ∩ f -` v)"
          by (rule imageI)
        with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)"
          by (rule ssubst)
      qed
    qed
  qed
next
  show "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 hx : "x ∈ s ∩ f -` v"
      have "y ∈ f ` s"
      proof -
        have "x ∈ s"
          using hx by (rule IntD1)
        then have "f x ∈ f ` s"
          by (rule imageI)
        with ‹y = f x› show "y ∈ f ` s"
          by (rule ssubst)
      qed
      moreover
      have "y ∈ v"
      proof -
        have "x ∈ f -` v"
          using hx by (rule IntD2)
        then have "f x ∈ v"
          by (rule vimageD)
        with ‹y = f x› show "y ∈ v"
          by (rule ssubst)
      qed
      ultimately show "y ∈ (f ` s) ∩ v"
        by (rule IntI)
    qed
  qed
qed

(* 2ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
proof
  show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)"
  proof
    fix y
    assume "y ∈ (f ` s) ∩ v"
    then show "y ∈ f ` (s ∩ f -` v)"
    proof
      assume "y ∈ v"
      assume "y ∈ f ` s"
      then show "y ∈ f ` (s ∩ f -` v)"
      proof
        fix x
        assume "x ∈ s"
        assume "y = f x"
        then have "f x ∈ v" using ‹y ∈ v› by simp
        then have "x ∈ f -` v" by simp
        with ‹x ∈ s› have "x ∈ s ∩ f -` v" by simp
        then have "f x ∈ f ` (s ∩ f -` v)" by simp
        with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)" by simp
      qed
    qed
  qed
next
  show "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 hx : "x ∈ s ∩ f -` v"
      have "y ∈ f ` s"
      proof -
        have "x ∈ s" using hx by simp
        then have "f x ∈ f ` s" by simp
        with ‹y = f x› show "y ∈ f ` s" by simp
      qed
      moreover
      have "y ∈ v"
      proof -
        have "x ∈ f -` v" using hx by simp
        then have "f x ∈ v" by simp
        with ‹y = f x› show "y ∈ v" by simp
      qed
      ultimately show "y ∈ (f ` s) ∩ v" by simp
    qed
  qed
qed

(* 2ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
proof
  show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)"
  proof
    fix y
    assume "y ∈ (f ` s) ∩ v"
    then show "y ∈ f ` (s ∩ f -` v)"
    proof
      assume "y ∈ v"
      assume "y ∈ f ` s"
      then show "y ∈ f ` (s ∩ f -` v)"
      proof
        fix x
        assume "x ∈ s"
        assume "y = f x"
        then show "y ∈ f ` (s ∩ f -` v)"
          using ‹x ∈ s› ‹y ∈ v› by simp
      qed
    qed
  qed
next
  show "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 hx : "x ∈ s ∩ f -` v"
      then have "y ∈ f ` s" using ‹y = f x› by simp
      moreover
      have "y ∈ v" using hx ‹y = f x› by simp
      ultimately show "y ∈ (f ` s) ∩ v" by simp
    qed
  qed
qed

(* 4ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
  by auto

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

theory Interseccion_con_la_imagen

imports Main

begin

(* 1ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"

proof (rule equalityI)

show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)"

proof (rule subsetI)

fix y

assume "y ∈ (f ` s) ∩ v"

then show "y ∈ f ` (s ∩ f -` v)"

proof (rule IntE)

assume "y ∈ v"

assume "y ∈ f ` s"

then show "y ∈ f ` (s ∩ f -` v)"

proof (rule imageE)

fix x

assume "x ∈ s"

assume "y = f x"

then have "f x ∈ v"

using ‹y ∈ v› by (rule subst)

then have "x ∈ f -` v"

by (rule vimageI2)

with ‹x ∈ s› have "x ∈ s ∩ f -` v"

by (rule IntI)

then have "f x ∈ f ` (s ∩ f -` v)"

by (rule imageI)

with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)"

by (rule ssubst)

qed

show "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 hx : "x ∈ s ∩ f -` v"

have "y ∈ f ` s"

proof -

have "x ∈ s"

using hx by (rule IntD1)

then have "f x ∈ f ` s"

by (rule imageI)

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

by (rule ssubst)

qed

moreover

have "y ∈ v"

proof -

have "x ∈ f -` v"

using hx by (rule IntD2)

then have "f x ∈ v"

by (rule vimageD)

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

by (rule ssubst)

qed

ultimately show "y ∈ (f ` s) ∩ v"

by (rule IntI)

qed

(* 2ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"

proof

show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)"

proof

fix y

assume "y ∈ (f ` s) ∩ v"

then show "y ∈ f ` (s ∩ f -` v)"

proof

assume "y ∈ v"

assume "y ∈ f ` s"

then show "y ∈ f ` (s ∩ f -` v)"

proof

fix x

assume "x ∈ s"

assume "y = f x"

then have "f x ∈ v" using ‹y ∈ v› by simp

then have "x ∈ f -` v" by simp

with ‹x ∈ s› have "x ∈ s ∩ f -` v" by simp

then have "f x ∈ f ` (s ∩ f -` v)" by simp

with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)" by simp

qed

show "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 hx : "x ∈ s ∩ f -` v"

have "y ∈ f ` s"

proof -

have "x ∈ s" using hx by simp

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

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

qed

moreover

have "y ∈ v"

proof -

have "x ∈ f -` v" using hx by simp

then have "f x ∈ v" by simp

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

qed

ultimately show "y ∈ (f ` s) ∩ v" by simp

qed

(* 2ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"

proof

show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)"

proof

fix y

assume "y ∈ (f ` s) ∩ v"

then show "y ∈ f ` (s ∩ f -` v)"

proof

assume "y ∈ v"

assume "y ∈ f ` s"

then show "y ∈ f ` (s ∩ f -` v)"

proof

fix x

assume "x ∈ s"

assume "y = f x"

then show "y ∈ f ` (s ∩ f -` v)"

using ‹x ∈ s› ‹y ∈ v› by simp

qed

show "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 hx : "x ∈ s ∩ f -` v"

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

moreover

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

ultimately show "y ∈ (f ` s) ∩ v" by simp

qed

(* 4ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"

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]

Imagen inversa de la diferencia

PorJosé A. Alonso 18 junio 202112 junio 2021

Demostrar que

   f⁻¹[u] - f⁻¹[v] ⊆ f⁻¹[u - v]

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

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

import data.set.basic

open set

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

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=
sorry

import data.set.basic

open set

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

variable f : α → β

variables u v : set β

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic

open set

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

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

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=
begin
  intros x hx,
  rw mem_preimage,
  split,
  { rw ← mem_preimage,
    exact hx.1, },
  { dsimp,
    rw ← mem_preimage,
    exact hx.2, },
end

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

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=
begin
  intros x hx,
  split,
  { exact hx.1, },
  { exact hx.2, },
end

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

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=
begin
  intros x hx,
  exact ⟨hx.1, hx.2⟩,
end

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

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=
begin
  rintros x ⟨h1, h2⟩,
  exact ⟨h1, h2⟩,
end

-- 5ª demostración
-- ===============

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=
subset.rfl

-- 6ª demostración
-- ===============

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=
by finish

import data.set.basic

open set

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

variable f : α → β

variables u v : set β

-- 1ª demostración

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

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=

begin

intros x hx,

rw mem_preimage,

split,

{ rw ← mem_preimage,

exact hx.1, },

{ dsimp,

rw ← mem_preimage,

exact hx.2, },

end

-- 2ª demostración

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

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=

begin

intros x hx,

split,

{ exact hx.1, },

{ exact hx.2, },

end

-- 3ª demostración

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

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=

begin

intros x hx,

exact ⟨hx.1, hx.2⟩,

end

-- 4ª demostración

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

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=

begin

rintros x ⟨h1, h2⟩,

exact ⟨h1, h2⟩,

end

-- 5ª demostración

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

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=

subset.rfl

-- 6ª demostración

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

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=

by finish

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

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

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

theory Imagen_inversa_de_la_diferencia
imports Main
begin

(* 1ª demostración *)

lemma "f -` u - f -` v ⊆ f -` (u - v)"
proof (rule subsetI)
  fix x
  assume "x ∈ f -` u - f -` v"
  then have "f x ∈ u - v"
  proof (rule DiffE)
    assume "x ∈ f -` u"
    assume "x ∉ f -` v"
    have "f x ∈ u"
      using ‹x ∈ f -` u› by (rule vimageD)
    moreover
    have "f x ∉ v"
    proof (rule notI)
      assume "f x ∈ v"
      then have "x ∈ f -` v"
        by (rule vimageI2)
      with ‹x ∉ f -` v› show False
        by (rule notE)
    qed
    ultimately show "f x ∈ u - v"
      by (rule DiffI)
  qed
  then show "x ∈ f -` (u - v)"
    by (rule vimageI2)
qed

(* 2ª demostración *)

lemma "f -` u - f -` v ⊆ f -` (u - v)"
proof
  fix x
  assume "x ∈ f -` u - f -` v"
  then have "f x ∈ u - v"
  proof
    assume "x ∈ f -` u"
    assume "x ∉ f -` v"
    have "f x ∈ u" using ‹x ∈ f -` u› by simp
    moreover
    have "f x ∉ v"
    proof
      assume "f x ∈ v"
      then have "x ∈ f -` v" by simp
      with ‹x ∉ f -` v› show False by simp
    qed
    ultimately show "f x ∈ u - v" by simp
  qed
  then show "x ∈ f -` (u - v)" by simp
qed

(* 3ª demostración *)

lemma "f -` u - f -` v ⊆ f -` (u - v)"
  by (simp only: vimage_Diff)

(* 4ª demostración *)

lemma "f -` u - f -` v ⊆ f -` (u - v)"
  by auto

end

theory Imagen_inversa_de_la_diferencia

imports Main

begin

(* 1ª demostración *)

lemma "f -` u - f -` v ⊆ f -` (u - v)"

proof (rule subsetI)

fix x

assume "x ∈ f -` u - f -` v"

then have "f x ∈ u - v"

proof (rule DiffE)

assume "x ∈ f -` u"

assume "x ∉ f -` v"

have "f x ∈ u"

using ‹x ∈ f -` u› by (rule vimageD)

moreover

have "f x ∉ v"

proof (rule notI)

assume "f x ∈ v"

then have "x ∈ f -` v"

by (rule vimageI2)

with ‹x ∉ f -` v› show False

by (rule notE)

qed

ultimately show "f x ∈ u - v"

by (rule DiffI)

qed

then show "x ∈ f -` (u - v)"

by (rule vimageI2)

qed

(* 2ª demostración *)

lemma "f -` u - f -` v ⊆ f -` (u - v)"

proof

fix x

assume "x ∈ f -` u - f -` v"

then have "f x ∈ u - v"

proof

assume "x ∈ f -` u"

assume "x ∉ f -` v"

have "f x ∈ u" using ‹x ∈ f -` u› by simp

moreover

have "f x ∉ v"

proof

assume "f x ∈ v"

then have "x ∈ f -` v" by simp

with ‹x ∉ f -` v› show False by simp

qed

ultimately show "f x ∈ u - v" by simp

qed

then show "x ∈ f -` (u - v)" by simp

qed

(* 3ª demostración *)

lemma "f -` u - f -` v ⊆ f -` (u - v)"

by (simp only: vimage_Diff)

(* 4ª demostración *)

lemma "f -` u - f -` v ⊆ f -` (u - v)"

by auto

end

Otras 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]

Imagen de la diferencia de conjuntos

PorJosé A. Alonso 17 junio 202112 junio 2021

Demostrar que

   f[s] - f[t] ⊆ f[s - t]

1	f[s] - f[t] ⊆ f[s - t]

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

import data.set.basic
import tactic

open set

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

example : f '' s \ f '' t ⊆ f '' (s \ t) :=
sorry

import data.set.basic

import tactic

open set

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

variable f : α → β

variables s t : set α

example : f '' s \ f '' t ⊆ f '' (s \ t) :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

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

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

example : f '' s \ f '' t ⊆ f '' (s \ t) :=
begin
  intros y hy,
  cases hy with yfs ynft,
  cases yfs with x hx,
  cases hx with xs fxy,
  use x,
  split,
  { split,
    { exact xs, },
    { dsimp,
      intro xt,
      apply ynft,
      rw ← fxy,
      apply mem_image_of_mem,
      exact xt, }},
  { exact fxy, },
end

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

example : f '' s \ f '' t ⊆ f '' (s \ t) :=
begin
  rintros y ⟨⟨x, xs, fxy⟩, ynft⟩,
  use x,
  split,
  { split,
    { exact xs, },
    { intro xt,
      apply ynft,
      use [x, xt, fxy], }},
  { exact fxy, },
end

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

example : f '' s \ f '' t ⊆ f '' (s \ t) :=
begin
  rintros y ⟨⟨x, xs, fxy⟩, ynft⟩,
  use x,
  finish,
end

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

example : f '' s \ f '' t ⊆ f '' (s \ t) :=
subset_image_diff f s t

import data.set.basic

import tactic

open set

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

variable f : α → β

variables s t : set α

-- 1ª demostración

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

example : f '' s \ f '' t ⊆ f '' (s \ t) :=

begin

intros y hy,

cases hy with yfs ynft,

cases yfs with x hx,

cases hx with xs fxy,

use x,

split,

{ split,

{ exact xs, },

{ dsimp,

intro xt,

apply ynft,

rw ← fxy,

apply mem_image_of_mem,

exact xt, }},

{ exact fxy, },

end

-- 2ª demostración

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

example : f '' s \ f '' t ⊆ f '' (s \ t) :=

begin

rintros y ⟨⟨x, xs, fxy⟩, ynft⟩,

use x,

split,

{ split,

{ exact xs, },

{ intro xt,

apply ynft,

use [x, xt, fxy], }},

{ exact fxy, },

end

-- 3ª demostración

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

example : f '' s \ f '' t ⊆ f '' (s \ t) :=

begin

rintros y ⟨⟨x, xs, fxy⟩, ynft⟩,

use x,

finish,

end

-- 4ª demostración

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

example : f '' s \ f '' t ⊆ f '' (s \ t) :=

subset_image_diff f s t

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

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

theory Imagen_de_la_diferencia_de_conjuntos
imports Main
begin

(* 1ª demostración *)

lemma "f ` s - f ` t ⊆ f ` (s - t)"
proof (rule subsetI)
  fix y
  assume hy : "y ∈ f ` s - f ` t"
  then show "y ∈ f ` (s - t)"
  proof (rule DiffE)
    assume "y ∈ f ` s"
    assume "y ∉ f ` t"
    note ‹y ∈ f ` s›
    then show "y ∈ f ` (s - t)"
    proof (rule imageE)
      fix x
      assume "y = f x"
      assume "x ∈ s"
      have ‹x ∉ t›
      proof (rule notI)
        assume "x ∈ t"
        then have "f x ∈ f ` t"
          by (rule imageI)
        with ‹y = f x› have "y ∈ f ` t"
          by (rule ssubst)
      with ‹y ∉ f ` t› show False
        by (rule notE)
    qed
    with ‹x ∈ s› have "x ∈ s - t"
      by (rule DiffI)
    then have "f x ∈ f ` (s - t)"
      by (rule imageI)
    with ‹y = f x› show "y ∈ f ` (s - t)"
      by (rule ssubst)
    qed
  qed
qed

(* 2ª demostración *)

lemma "f ` s - f ` t ⊆ f ` (s - t)"
proof
  fix y
  assume hy : "y ∈ f ` s - f ` t"
  then show "y ∈ f ` (s - t)"
  proof
    assume "y ∈ f ` s"
    assume "y ∉ f ` t"
    note ‹y ∈ f ` s›
    then show "y ∈ f ` (s - t)"
    proof
      fix x
      assume "y = f x"
      assume "x ∈ s"
      have ‹x ∉ t›
      proof
        assume "x ∈ t"
        then have "f x ∈ f ` t" by simp
        with ‹y = f x› have "y ∈ f ` t" by simp
      with ‹y ∉ f ` t› show False by simp
    qed
    with ‹x ∈ s› have "x ∈ s - t" by simp
    then have "f x ∈ f ` (s - t)" by simp
    with ‹y = f x› show "y ∈ f ` (s - t)" by simp
    qed
  qed
qed

(* 3ª demostración *)

lemma "f ` s - f ` t ⊆ f ` (s - t)"
  by (simp only: image_diff_subset)

(* 4ª demostración *)

lemma "f ` s - f ` t ⊆ f ` (s - t)"
  by auto

end

theory Imagen_de_la_diferencia_de_conjuntos

imports Main

begin

(* 1ª demostración *)

lemma "f ` s - f ` t ⊆ f ` (s - t)"

proof (rule subsetI)

fix y

assume hy : "y ∈ f ` s - f ` t"

then show "y ∈ f ` (s - t)"

proof (rule DiffE)

assume "y ∈ f ` s"

assume "y ∉ f ` t"

note ‹y ∈ f ` s›

then show "y ∈ f ` (s - t)"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ s"

have ‹x ∉ t›

proof (rule notI)

assume "x ∈ t"

then have "f x ∈ f ` t"

by (rule imageI)

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

by (rule ssubst)

with ‹y ∉ f ` t› show False

by (rule notE)

qed

with ‹x ∈ s› have "x ∈ s - t"

by (rule DiffI)

then have "f x ∈ f ` (s - t)"

by (rule imageI)

with ‹y = f x› show "y ∈ f ` (s - t)"

by (rule ssubst)

qed

(* 2ª demostración *)

lemma "f ` s - f ` t ⊆ f ` (s - t)"

proof

fix y

assume hy : "y ∈ f ` s - f ` t"

then show "y ∈ f ` (s - t)"

proof

assume "y ∈ f ` s"

assume "y ∉ f ` t"

note ‹y ∈ f ` s›

then show "y ∈ f ` (s - t)"

proof

fix x

assume "y = f x"

assume "x ∈ s"

have ‹x ∉ t›

proof

assume "x ∈ t"

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

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

with ‹y ∉ f ` t› show False by simp

qed

with ‹x ∈ s› have "x ∈ s - t" by simp

then have "f x ∈ f ` (s - t)" by simp

with ‹y = f x› show "y ∈ f ` (s - t)" by simp

qed

(* 3ª demostración *)

lemma "f ` s - f ` t ⊆ f ` (s - t)"

by (simp only: image_diff_subset)

(* 4ª demostración *)

lemma "f ` s - f ` t ⊆ f ` (s - t)"

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="lean"> (o <pre lang="isar">) y otra con </pre>

[/expand]

Imagen de la intersección mediante aplicaciones inyectivas

PorJosé A. Alonso 16 junio 202112 junio 2021

Demostrar que si f es inyectiva, entonces

   f[s] ∩ f[t] ⊆ f[s ∩ t]

1	f[s] ∩ f[t] ⊆ f[s ∩ t]

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

import data.set.basic

open set function

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

example
  (h : injective f)
  : f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=
sorry

import data.set.basic

open set function

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

variable f : α → β

variables s t : set α

example

(h : injective f)

: f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic

open set function

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

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

example
  (h : injective f)
  : f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=
begin
  intros y hy,
  cases hy  with hy1 hy2,
  cases hy1 with x1 hx1,
  cases hx1 with x1s fx1y,
  cases hy2 with x2 hx2,
  cases hx2 with x2t fx2y,
  use x1,
  split,
  { split,
    { exact x1s, },
    { convert x2t,
      apply h,
      rw ← fx2y at fx1y,
      exact fx1y, }},
  { exact fx1y, },
end

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

example
  (h : injective f)
  : f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=
begin
  rintros y ⟨⟨x1, x1s, fx1y⟩, ⟨x2, x2t, fx2y⟩⟩,
  use x1,
  split,
  { split,
    { exact x1s, },
    { convert x2t,
      apply h,
      rw ← fx2y at fx1y,
      exact fx1y, }},
  { exact fx1y, },
end

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

example
  (h : injective f)
  : f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=
begin
  rintros y ⟨⟨x1, x1s, fx1y⟩, ⟨x2, x2t, fx2y⟩⟩,
  unfold injective at h,
  finish,
end

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

example
  (h : injective f)
  : f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=
by intro ; unfold injective at *  ; finish

import data.set.basic

open set function

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

variable f : α → β

variables s t : set α

-- 1ª demostración

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

example

(h : injective f)

: f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=

begin

intros y hy,

cases hy with hy1 hy2,

cases hy1 with x1 hx1,

cases hx1 with x1s fx1y,

cases hy2 with x2 hx2,

cases hx2 with x2t fx2y,

use x1,

split,

{ split,

{ exact x1s, },

{ convert x2t,

apply h,

rw ← fx2y at fx1y,

exact fx1y, }},

{ exact fx1y, },

end

-- 2ª demostración

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

example

(h : injective f)

: f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=

begin

rintros y ⟨⟨x1, x1s, fx1y⟩, ⟨x2, x2t, fx2y⟩⟩,

use x1,

split,

{ split,

{ exact x1s, },

{ convert x2t,

apply h,

rw ← fx2y at fx1y,

exact fx1y, }},

{ exact fx1y, },

end

-- 3ª demostración

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

example

(h : injective f)

: f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=

begin

rintros y ⟨⟨x1, x1s, fx1y⟩, ⟨x2, x2t, fx2y⟩⟩,

unfold injective at h,

finish,

end

-- 4ª demostración

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

example

(h : injective f)

: f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=

by intro ; unfold injective at * ; finish

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

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

theory Imagen_de_la_interseccion_de_aplicaciones_inyectivas
imports Main
begin

(* 1ª demostración *)

lemma
  assumes "inj f"
  shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"
proof (rule subsetI)
  fix y
  assume "y ∈ f ` s ∩ f ` t"
  then have "y ∈ f ` s"
    by (rule IntD1)
  then show "y ∈ f ` (s ∩ t)"
  proof (rule imageE)
    fix x
    assume "y = f x"
    assume "x ∈ s"
    have "x ∈ t"
    proof -
      have "y ∈ f ` t"
        using ‹y ∈ f ` s ∩ f ` t› by (rule IntD2)
      then show "x ∈ t"
      proof (rule imageE)
        fix z
        assume "y = f z"
        assume "z ∈ t"
        have "f x = f z"
          using ‹y = f x› ‹y = f z› by (rule subst)
        with ‹inj f› have "x = z"
          by (simp only: inj_eq)
        then show "x ∈ t"
          using ‹z ∈ t› by (rule ssubst)
      qed
    qed
    with ‹x ∈ s› have "x ∈ s ∩ t"
      by (rule IntI)
    with ‹y = f x› show "y ∈ f ` (s ∩ t)"
      by (rule image_eqI)
  qed
qed

(* 2ª demostración *)

lemma
  assumes "inj f"
  shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"
proof
  fix y
  assume "y ∈ f ` s ∩ f ` t"
  then have "y ∈ f ` s" by simp
  then show "y ∈ f ` (s ∩ t)"
  proof
    fix x
    assume "y = f x"
    assume "x ∈ s"
    have "x ∈ t"
    proof -
      have "y ∈ f ` t" using ‹y ∈ f ` s ∩ f ` t› by simp
      then show "x ∈ t"
      proof
        fix z
        assume "y = f z"
        assume "z ∈ t"
        have "f x = f z" using ‹y = f x› ‹y = f z› by simp
        with ‹inj f› have "x = z" by (simp only: inj_eq)
        then show "x ∈ t" using ‹z ∈ t› by simp
      qed
    qed
    with ‹x ∈ s› have "x ∈ s ∩ t" by simp
    with ‹y = f x› show "y ∈ f ` (s ∩ t)" by simp
  qed
qed

(* 3ª demostración *)

lemma
  assumes "inj f"
  shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"
  using assms
  by (simp only: image_Int)

(* 4ª demostración *)

lemma
  assumes "inj f"
  shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"
  using assms
  unfolding inj_def
  by auto

end

theory Imagen_de_la_interseccion_de_aplicaciones_inyectivas

imports Main

begin

(* 1ª demostración *)

lemma

assumes "inj f"

shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"

proof (rule subsetI)

fix y

assume "y ∈ f ` s ∩ f ` t"

then have "y ∈ f ` s"

by (rule IntD1)

then show "y ∈ f ` (s ∩ t)"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ s"

have "x ∈ t"

proof -

have "y ∈ f ` t"

using ‹y ∈ f ` s ∩ f ` t› by (rule IntD2)

then show "x ∈ t"

proof (rule imageE)

fix z

assume "y = f z"

assume "z ∈ t"

have "f x = f z"

using ‹y = f x› ‹y = f z› by (rule subst)

with ‹inj f› have "x = z"

by (simp only: inj_eq)

then show "x ∈ t"

using ‹z ∈ t› by (rule ssubst)

qed

with ‹x ∈ s› have "x ∈ s ∩ t"

by (rule IntI)

with ‹y = f x› show "y ∈ f ` (s ∩ t)"

by (rule image_eqI)

qed

(* 2ª demostración *)

lemma

assumes "inj f"

shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"

proof

fix y

assume "y ∈ f ` s ∩ f ` t"

then have "y ∈ f ` s" by simp

then show "y ∈ f ` (s ∩ t)"

proof

fix x

assume "y = f x"

assume "x ∈ s"

have "x ∈ t"

proof -

have "y ∈ f ` t" using ‹y ∈ f ` s ∩ f ` t› by simp

then show "x ∈ t"

proof

fix z

assume "y = f z"

assume "z ∈ t"

have "f x = f z" using ‹y = f x› ‹y = f z› by simp

with ‹inj f› have "x = z" by (simp only: inj_eq)

then show "x ∈ t" using ‹z ∈ t› by simp

qed

with ‹x ∈ s› have "x ∈ s ∩ t" by simp

with ‹y = f x› show "y ∈ f ` (s ∩ t)" by simp

qed

(* 3ª demostración *)

lemma

assumes "inj f"

shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"

using assms

by (simp only: image_Int)

(* 4ª demostración *)

lemma

assumes "inj f"

shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"

using assms

unfolding inj_def

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="lean"> (o <pre lang="isar">) y otra con </pre>

[/expand]

Imagen de la intersección

PorJosé A. Alonso 15 junio 202112 junio 2021

Demostrar que

   f[s ∩ t] ⊆ f[s] ∩ f[t]

1	f[s ∩ t] ⊆ f[s] ∩ f[t]

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

import data.set.basic
import tactic

open set

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

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=
sorry

import data.set.basic

import tactic

open set

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

variable f : α → β

variables s t : set α

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

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

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

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=
begin
  intros y hy,
  cases hy with x hx,
  cases hx with xst fxy,
  split,
  { use x,
    split,
    { exact xst.1, },
    { exact fxy, }},
  { use x,
    split,
    { exact xst.2, },
    { exact fxy, }},
end

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

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=
begin
  intros y hy,
  rcases hy with ⟨x, ⟨xs, xt⟩, fxy⟩,
  split,
  { use x,
    exact ⟨xs, fxy⟩, },
  { use x,
    exact ⟨xt, fxy⟩, },
end

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

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=
begin
  rintros y ⟨x, ⟨xs, xt⟩, fxy⟩,
  split,
  { use [x, xs, fxy], },
  { use [x, xt, fxy], },
end

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

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=
image_inter_subset f s t

-- 5ª demostración
-- ===============

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=
by intro ; finish

import data.set.basic

import tactic

open set

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

variable f : α → β

variables s t : set α

-- 1ª demostración

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

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=

begin

intros y hy,

cases hy with x hx,

cases hx with xst fxy,

split,

{ use x,

split,

{ exact xst.1, },

{ exact fxy, }},

{ use x,

split,

{ exact xst.2, },

{ exact fxy, }},

end

-- 2ª demostración

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

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=

begin

intros y hy,

rcases hy with ⟨x, ⟨xs, xt⟩, fxy⟩,

split,

{ use x,

exact ⟨xs, fxy⟩, },

{ use x,

exact ⟨xt, fxy⟩, },

end

-- 3ª demostración

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

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=

begin

rintros y ⟨x, ⟨xs, xt⟩, fxy⟩,

split,

{ use [x, xs, fxy], },

{ use [x, xt, fxy], },

end

-- 4ª demostración

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

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=

image_inter_subset f s t

-- 5ª demostración

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

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=

by intro ; finish

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

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

theory Imagen_de_la_interseccion
imports Main
begin

section ‹1ª demostración›

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"
proof (rule subsetI)
  fix y
  assume "y ∈ f ` (s ∩ t)"
  then have "y ∈ f ` s"
  proof (rule imageE)
    fix x
    assume "y = f x"
    assume "x ∈ s ∩ t"
    have "x ∈ s"
      using ‹x ∈ s ∩ t› by (rule IntD1)
    then have "f x ∈ f ` s"
      by (rule imageI)
    with ‹y = f x› show "y ∈ f ` s"
      by (rule ssubst)
  qed
  moreover
  note ‹y ∈ f ` (s ∩ t)›
  then have "y ∈ f ` t"
  proof (rule imageE)
    fix x
    assume "y = f x"
    assume "x ∈ s ∩ t"
    have "x ∈ t"
      using ‹x ∈ s ∩ t› by (rule IntD2)
    then have "f x ∈ f ` t"
      by (rule imageI)
    with ‹y = f x› show "y ∈ f ` t"
      by (rule ssubst)
  qed
  ultimately show "y ∈ f ` s ∩ f ` t"
    by (rule IntI)
qed

section ‹2ª demostración›

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"
proof
  fix y
  assume "y ∈ f ` (s ∩ t)"
  then have "y ∈ f ` s"
  proof
    fix x
    assume "y = f x"
    assume "x ∈ s ∩ t"
    have "x ∈ s"
      using ‹x ∈ s ∩ t› by simp
    then have "f x ∈ f ` s"
      by simp
    with ‹y = f x› show "y ∈ f ` s"
      by simp
  qed
  moreover
  note ‹y ∈ f ` (s ∩ t)›
  then have "y ∈ f ` t"
  proof
    fix x
    assume "y = f x"
    assume "x ∈ s ∩ t"
    have "x ∈ t"
      using ‹x ∈ s ∩ t› by simp
    then have "f x ∈ f ` t"
      by simp
    with ‹y = f x› show "y ∈ f ` t"
      by simp
  qed
  ultimately show "y ∈ f ` s ∩ f ` t"
    by simp
qed

section ‹3ª demostración›

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"
proof
  fix y
  assume "y ∈ f ` (s ∩ t)"
  then obtain x where hx : "y = f x ∧ x ∈ s ∩ t" by auto
  then have "y = f x" by simp
  have "x ∈ s" using hx by simp
  have "x ∈ t" using hx by simp
  have "y ∈  f ` s" using ‹y = f x› ‹x ∈ s› by simp
  moreover
  have "y ∈  f ` t" using ‹y = f x› ‹x ∈ t› by simp
  ultimately show "y ∈ f ` s ∩ f ` t"
    by simp
qed

section ‹4ª demostración›

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"
  by (simp only: image_Int_subset)

section ‹5ª demostración›

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"
  by auto

end

100

101

102

103

104

theory Imagen_de_la_interseccion

imports Main

begin

section ‹1ª demostración›

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"

proof (rule subsetI)

fix y

assume "y ∈ f ` (s ∩ t)"

then have "y ∈ f ` s"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ s ∩ t"

have "x ∈ s"

using ‹x ∈ s ∩ t› by (rule IntD1)

then have "f x ∈ f ` s"

by (rule imageI)

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

by (rule ssubst)

qed

moreover

note ‹y ∈ f ` (s ∩ t)›

then have "y ∈ f ` t"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ s ∩ t"

have "x ∈ t"

using ‹x ∈ s ∩ t› by (rule IntD2)

then have "f x ∈ f ` t"

by (rule imageI)

with ‹y = f x› show "y ∈ f ` t"

by (rule ssubst)

qed

ultimately show "y ∈ f ` s ∩ f ` t"

by (rule IntI)

qed

section ‹2ª demostración›

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"

proof

fix y

assume "y ∈ f ` (s ∩ t)"

then have "y ∈ f ` s"

proof

fix x

assume "y = f x"

assume "x ∈ s ∩ t"

have "x ∈ s"

using ‹x ∈ s ∩ t› by simp

then have "f x ∈ f ` s"

by simp

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

by simp

qed

moreover

note ‹y ∈ f ` (s ∩ t)›

then have "y ∈ f ` t"

proof

fix x

assume "y = f x"

assume "x ∈ s ∩ t"

have "x ∈ t"

using ‹x ∈ s ∩ t› by simp

then have "f x ∈ f ` t"

by simp

with ‹y = f x› show "y ∈ f ` t"

by simp

qed

ultimately show "y ∈ f ` s ∩ f ` t"

by simp

qed

section ‹3ª demostración›

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"

proof

fix y

assume "y ∈ f ` (s ∩ t)"

then obtain x where hx : "y = f x ∧ x ∈ s ∩ t" by auto

then have "y = f x" by simp

have "x ∈ s" using hx by simp

have "x ∈ t" using hx by simp

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

moreover

have "y ∈ f ` t" using ‹y = f x› ‹x ∈ t› by simp

ultimately show "y ∈ f ` s ∩ f ` t"

by simp

qed

section ‹4ª demostración›

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"

by (simp only: image_Int_subset)

section ‹5ª demostración›

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"

by auto

end

[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="lean"> (o <pre lang="isar">) y otra con </pre>

[/expand]

Imagen inversa de la unión

PorJosé A. Alonso 14 junio 202112 junio 2021

Demostrar que

   f⁻¹[u ∪ v] = f⁻¹[u] ∪ f⁻¹[v]

1	f⁻¹[u ∪ v] = f⁻¹[u] ∪ f⁻¹[v]

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

import data.set.basic

open set

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

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

import data.set.basic

open set

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

variable f : α → β

variables u v : set β

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic

open set

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

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
begin
  ext x,
  split,
  { intros h,
    rw mem_preimage at h,
    cases h with fxu fxv,
    { left,
      apply mem_preimage.mpr,
      exact fxu, },
    { right,
      apply mem_preimage.mpr,
      exact fxv, }},
  { intro h,
    rw mem_preimage,
    cases h with xfu xfv,
    { rw mem_preimage at xfu,
      left,
      exact xfu, },
    { rw mem_preimage at xfv,
      right,
      exact xfv, }},
end

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
begin
  ext x,
  split,
  { intros h,
    cases h with fxu fxv,
    { left,
      exact fxu, },
    { right,
      exact fxv, }},
  { intro h,
    cases h with xfu xfv,
    { left,
      exact xfu, },
    { right,
      exact xfv, }},
end

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
begin
  ext x,
  split,
  { rintro (fxu | fxv),
    { exact or.inl fxu, },
    { exact or.inr fxv, }},
  { rintro (xfu | xfv),
    { exact or.inl xfu, },
    { exact or.inr xfv, }},
end

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
begin
  ext x,
  split,
  { finish, },
  { finish, } ,
end

-- 5ª demostración
-- ===============

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
begin
  ext x,
  finish,
end

-- 6ª demostración
-- ===============

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
by ext; finish

-- 7ª demostración
-- ===============

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
by ext; refl

-- 8ª demostración
-- ===============

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
rfl

-- 9ª demostración
-- ===============

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
preimage_union

-- 10ª demostración
-- ===============

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
by simp

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

import data.set.basic

open set

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

variable f : α → β

variables u v : set β

-- 1ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

begin

ext x,

split,

{ intros h,

rw mem_preimage at h,

cases h with fxu fxv,

{ left,

apply mem_preimage.mpr,

exact fxu, },

{ right,

apply mem_preimage.mpr,

exact fxv, }},

{ intro h,

rw mem_preimage,

cases h with xfu xfv,

{ rw mem_preimage at xfu,

left,

exact xfu, },

{ rw mem_preimage at xfv,

right,

exact xfv, }},

end

-- 2ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

begin

ext x,

split,

{ intros h,

cases h with fxu fxv,

{ left,

exact fxu, },

{ right,

exact fxv, }},

{ intro h,

cases h with xfu xfv,

{ left,

exact xfu, },

{ right,

exact xfv, }},

end

-- 3ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

begin

ext x,

split,

{ rintro (fxu | fxv),

{ exact or.inl fxu, },

{ exact or.inr fxv, }},

{ rintro (xfu | xfv),

{ exact or.inl xfu, },

{ exact or.inr xfv, }},

end

-- 4ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

begin

ext x,

split,

{ finish, },

{ finish, } ,

end

-- 5ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

begin

ext x,

finish,

end

-- 6ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

by ext; finish

-- 7ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

by ext; refl

-- 8ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

rfl

-- 9ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

preimage_union

-- 10ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

by simp

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

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

theory Imagen_inversa_de_la_union
imports Main
begin

(* 1ª demostración *)

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"
proof (rule equalityI)
  show "f -` (u ∪ v) ⊆ f -` u ∪ f -` v"
  proof (rule subsetI)
    fix x
    assume "x ∈ f -` (u ∪ v)"
    then have "f x ∈ u ∪ v"
      by (rule vimageD)
    then show "x ∈ f -` u ∪ f -` v"
    proof (rule UnE)
      assume "f x ∈ u"
      then have "x ∈ f -` u"
        by (rule vimageI2)
      then show "x ∈ f -` u ∪ f -` v"
        by (rule UnI1)
    next
      assume "f x ∈ v"
      then have "x ∈ f -` v"
        by (rule vimageI2)
      then show "x ∈ f -` u ∪ f -` v"
        by (rule UnI2)
    qed
  qed
next
  show "f -` u ∪ f -` v ⊆ f -` (u ∪ v)"
  proof (rule subsetI)
    fix x
    assume "x ∈ f -` u ∪ f -` v"
    then show "x ∈ f -` (u ∪ v)"
    proof (rule UnE)
      assume "x ∈ f -` u"
      then have "f x ∈ u"
        by (rule vimageD)
      then have "f x ∈ u ∪ v"
        by (rule UnI1)
      then show "x ∈ f -` (u ∪ v)"
        by (rule vimageI2)
    next
      assume "x ∈ f -` v"
      then have "f x ∈ v"
        by (rule vimageD)
      then have "f x ∈ u ∪ v"
        by (rule UnI2)
      then show "x ∈ f -` (u ∪ v)"
        by (rule vimageI2)
    qed
  qed
qed

(* 2ª demostración *)

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"
proof
  show "f -` (u ∪ v) ⊆ f -` u ∪ f -` v"
  proof
    fix x
    assume "x ∈ f -` (u ∪ v)"
    then have "f x ∈ u ∪ v" by simp
    then show "x ∈ f -` u ∪ f -` v"
    proof
      assume "f x ∈ u"
      then have "x ∈ f -` u" by simp
      then show "x ∈ f -` u ∪ f -` v" by simp
    next
      assume "f x ∈ v"
      then have "x ∈ f -` v" by simp
      then show "x ∈ f -` u ∪ f -` v" by simp
    qed
  qed
next
  show "f -` u ∪ f -` v ⊆ f -` (u ∪ v)"
  proof
    fix x
    assume "x ∈ f -` u ∪ f -` v"
    then show "x ∈ f -` (u ∪ v)"
    proof
      assume "x ∈ f -` u"
      then have "f x ∈ u" by simp
      then have "f x ∈ u ∪ v" by simp
      then show "x ∈ f -` (u ∪ v)" by simp
    next
      assume "x ∈ f -` v"
      then have "f x ∈ v" by simp
      then have "f x ∈ u ∪ v" by simp
      then show "x ∈ f -` (u ∪ v)" by simp
    qed
  qed
qed

(* 3ª demostración *)

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"
  by (simp only: vimage_Un)

(* 4ª demostración *)

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"
  by auto

end

100

101

102

103

104

105

106

theory Imagen_inversa_de_la_union

imports Main

begin

(* 1ª demostración *)

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"

proof (rule equalityI)

show "f -` (u ∪ v) ⊆ f -` u ∪ f -` v"

proof (rule subsetI)

fix x

assume "x ∈ f -` (u ∪ v)"

then have "f x ∈ u ∪ v"

by (rule vimageD)

then show "x ∈ f -` u ∪ f -` v"

proof (rule UnE)

assume "f x ∈ u"

then have "x ∈ f -` u"

by (rule vimageI2)

then show "x ∈ f -` u ∪ f -` v"

by (rule UnI1)

assume "f x ∈ v"

then have "x ∈ f -` v"

by (rule vimageI2)

then show "x ∈ f -` u ∪ f -` v"

by (rule UnI2)

qed

show "f -` u ∪ f -` v ⊆ f -` (u ∪ v)"

proof (rule subsetI)

fix x

assume "x ∈ f -` u ∪ f -` v"

then show "x ∈ f -` (u ∪ v)"

proof (rule UnE)

assume "x ∈ f -` u"

then have "f x ∈ u"

by (rule vimageD)

then have "f x ∈ u ∪ v"

by (rule UnI1)

then show "x ∈ f -` (u ∪ v)"

by (rule vimageI2)

assume "x ∈ f -` v"

then have "f x ∈ v"

by (rule vimageD)

then have "f x ∈ u ∪ v"

by (rule UnI2)

then show "x ∈ f -` (u ∪ v)"

by (rule vimageI2)

qed

(* 2ª demostración *)

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"

proof

show "f -` (u ∪ v) ⊆ f -` u ∪ f -` v"

proof

fix x

assume "x ∈ f -` (u ∪ v)"

then have "f x ∈ u ∪ v" by simp

then show "x ∈ f -` u ∪ f -` v"

proof

assume "f x ∈ u"

then have "x ∈ f -` u" by simp

then show "x ∈ f -` u ∪ f -` v" by simp

assume "f x ∈ v"

then have "x ∈ f -` v" by simp

then show "x ∈ f -` u ∪ f -` v" by simp

qed

show "f -` u ∪ f -` v ⊆ f -` (u ∪ v)"

proof

fix x

assume "x ∈ f -` u ∪ f -` v"

then show "x ∈ f -` (u ∪ v)"

proof

assume "x ∈ f -` u"

then have "f x ∈ u" by simp

then have "f x ∈ u ∪ v" by simp

then show "x ∈ f -` (u ∪ v)" by simp

assume "x ∈ f -` v"

then have "f x ∈ v" by simp

then have "f x ∈ u ∪ v" by simp

then show "x ∈ f -` (u ∪ v)" by simp

qed

(* 3ª demostración *)

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"

by (simp only: vimage_Un)

(* 4ª demostración *)

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"

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="lean"> (o <pre lang="isar">) y otra con </pre>

[/expand]

Monotonía de la imagen inversa

PorJosé A. Alonso 13 junio 202112 junio 2021

Demostrar que si u ⊆ v, entonces

    f⁻¹[u] ⊆ f⁻¹[v]

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

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

import data.set.basic
open set

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

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

import data.set.basic

open set

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

variable f : α → β

variables u v : set β

example

(h : u ⊆ v)

: f ⁻¹' u ⊆ f ⁻¹' v :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
open set

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

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

example
  (h : u ⊆ v)
  : f ⁻¹' u ⊆ f ⁻¹' v :=
begin
  intros x hx,
  apply mem_preimage.mpr,
  apply h,
  apply mem_preimage.mp,
  exact hx,
end

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

example
  (h : u ⊆ v)
  : f ⁻¹' u ⊆ f ⁻¹' v :=
begin
  intros x hx,
  apply h,
  exact hx,
end

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

example
  (h : u ⊆ v)
  : f ⁻¹' u ⊆ f ⁻¹' v :=
begin
  intros x hx,
  exact h hx,
end

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

example
  (h : u ⊆ v)
  : f ⁻¹' u ⊆ f ⁻¹' v :=
λ x hx, h hx

-- 5ª demostración
-- ===============

example
  (h : u ⊆ v)
  : f ⁻¹' u ⊆ f ⁻¹' v :=
by intro x; apply h

-- 6ª demostración
-- ===============

example
  (h : u ⊆ v)
  : f ⁻¹' u ⊆ f ⁻¹' v :=
preimage_mono h

-- 7ª demostración
-- ===============

example
  (h : u ⊆ v)
  : f ⁻¹' u ⊆ f ⁻¹' v :=
by tauto

import data.set.basic

open set

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

variable f : α → β

variables u v : set β

-- 1ª demostración

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

example

(h : u ⊆ v)

: f ⁻¹' u ⊆ f ⁻¹' v :=

begin

intros x hx,

apply mem_preimage.mpr,

apply h,

apply mem_preimage.mp,

exact hx,

end

-- 2ª demostración

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

example

(h : u ⊆ v)

: f ⁻¹' u ⊆ f ⁻¹' v :=

begin

intros x hx,

apply h,

exact hx,

end

-- 3ª demostración

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

example

(h : u ⊆ v)

: f ⁻¹' u ⊆ f ⁻¹' v :=

begin

intros x hx,

exact h hx,

end

-- 4ª demostración

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

example

(h : u ⊆ v)

: f ⁻¹' u ⊆ f ⁻¹' v :=

λ x hx, h hx

-- 5ª demostración

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

example

(h : u ⊆ v)

: f ⁻¹' u ⊆ f ⁻¹' v :=

by intro x; apply h

-- 6ª demostración

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

example

(h : u ⊆ v)

: f ⁻¹' u ⊆ f ⁻¹' v :=

preimage_mono h

-- 7ª demostración

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

example

(h : u ⊆ v)

: f ⁻¹' u ⊆ f ⁻¹' v :=

by tauto

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

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

theory Monotonia_de_la_imagen_inversa
imports Main
begin

section ‹1ª demostración›

lemma
  assumes "u ⊆ v"
  shows "f -` u ⊆ f -` v"
proof (rule subsetI)
  fix x
  assume "x ∈ f -` u"
  then have "f x ∈ u"
    by (rule vimageD)
  then have "f x ∈ v"
    using ‹u ⊆ v› by (rule set_rev_mp)
  then show "x ∈ f -` v"
    by (simp only: vimage_eq)
qed

section ‹2ª demostración›

lemma
  assumes "u ⊆ v"
  shows "f -` u ⊆ f -` v"
proof
  fix x
  assume "x ∈ f -` u"
  then have "f x ∈ u"
    by simp
  then have "f x ∈ v"
    using ‹u ⊆ v› by (rule set_rev_mp)
  then show "x ∈ f -` v"
    by simp
qed

section ‹3ª demostración›

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

section ‹4ª demostración›

lemma
  assumes "u ⊆ v"
  shows "f -` u ⊆ f -` v"
  using assms
  by blast

end

theory Monotonia_de_la_imagen_inversa

imports Main

begin

section ‹1ª demostración›

lemma

assumes "u ⊆ v"

shows "f -` u ⊆ f -` v"

proof (rule subsetI)

fix x

assume "x ∈ f -` u"

then have "f x ∈ u"

by (rule vimageD)

then have "f x ∈ v"

using ‹u ⊆ v› by (rule set_rev_mp)

then show "x ∈ f -` v"

by (simp only: vimage_eq)

qed

section ‹2ª demostración›

lemma

assumes "u ⊆ v"

shows "f -` u ⊆ f -` v"

proof

fix x

assume "x ∈ f -` u"

then have "f x ∈ u"

by simp

then have "f x ∈ v"

using ‹u ⊆ v› by (rule set_rev_mp)

then show "x ∈ f -` v"

by simp

qed

section ‹3ª demostración›

lemma

assumes "u ⊆ v"

shows "f -` u ⊆ f -` v"

using assms

by (simp only: vimage_mono)

section ‹4ª demostración›

lemma

assumes "u ⊆ v"

shows "f -` u ⊆ f -` v"

using assms

by blast

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="lean"> (o <pre lang="isar">) y otra con </pre>

[/expand]

Monotonía de la imagen de conjuntos

PorJosé A. Alonso 12 junio 202112 junio 2021

Demostrar que si s ⊆ t, entonces

    f[s] ⊆ f[t]

1	f[s] ⊆ f[t]

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

import data.set.basic
import tactic

open set

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

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
sorry

import data.set.basic

import tactic

open set

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

variable f : α → β

variables s t : set α

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

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

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

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
begin
  intros y hy,
  rw mem_image at hy,
  cases hy with x hx,
  cases hx with xs fxy,
  use x,
  split,
  { exact h xs, },
  { exact fxy, },
end

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

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
begin
  intros y hy,
  rcases hy with ⟨x, xs, fxy⟩,
  use x,
  exact ⟨h xs, fxy⟩,
end

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

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
begin
  rintros y ⟨x, xs, fxy ⟩,
  use [x, h xs, fxy],
end

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

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
by finish [subset_def, mem_image_eq]

-- 5ª demostración
-- ===============

example
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
image_subset f h

import data.set.basic

import tactic

open set

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

variable f : α → β

variables s t : set α

-- 1ª demostración

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

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

begin

intros y hy,

rw mem_image at hy,

cases hy with x hx,

cases hx with xs fxy,

use x,

split,

{ exact h xs, },

{ exact fxy, },

end

-- 2ª demostración

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

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

begin

intros y hy,

rcases hy with ⟨x, xs, fxy⟩,

use x,

exact ⟨h xs, fxy⟩,

end

-- 3ª demostración

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

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

begin

rintros y ⟨x, xs, fxy ⟩,

use [x, h xs, fxy],

end

-- 4ª demostración

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

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

by finish [subset_def, mem_image_eq]

-- 5ª demostración

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

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

image_subset f h

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

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

theory Monotonia_de_la_imagen_de_conjuntos
imports Main
begin

section ‹1ª demostración›

lemma
  assumes "s ⊆ t"
  shows "f ` s ⊆ f ` t"
proof (rule subsetI)
  fix y
  assume "y ∈ f ` s"
  then show "y ∈ f ` t"
  proof (rule imageE)
    fix x
    assume "y = f x"
    assume "x ∈ s"
    then have "x ∈ t"
      using ‹s ⊆ t› by (simp only: set_rev_mp)
    then have "f x ∈ f ` t"
      by (rule imageI)
    with ‹y = f x› show "y ∈ f ` t"
      by (rule ssubst)
  qed
qed

section ‹2ª demostración›

lemma
  assumes "s ⊆ t"
  shows "f ` s ⊆ f ` t"
proof
  fix y
  assume "y ∈ f ` s"
  then show "y ∈ f ` t"
  proof
    fix x
    assume "y = f x"
    assume "x ∈ s"
    then have "x ∈ t"
      using ‹s ⊆ t› by (simp only: set_rev_mp)
    then have "f x ∈ f ` t"
      by simp
    with ‹y = f x› show "y ∈ f ` t"
      by simp
  qed
qed

section ‹3ª demostración›

lemma
  assumes "s ⊆ t"
  shows "f ` s ⊆ f ` t"
  using assms
  by blast

section ‹4ª demostración›

lemma
  assumes "s ⊆ t"
  shows "f ` s ⊆ f ` t"
  using assms
  by (simp only: image_mono)

end

theory Monotonia_de_la_imagen_de_conjuntos

imports Main

begin

section ‹1ª demostración›

lemma

assumes "s ⊆ t"

shows "f ` s ⊆ f ` t"

proof (rule subsetI)

fix y

assume "y ∈ f ` s"

then show "y ∈ f ` t"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ s"

then have "x ∈ t"

using ‹s ⊆ t› by (simp only: set_rev_mp)

then have "f x ∈ f ` t"

by (rule imageI)

with ‹y = f x› show "y ∈ f ` t"

by (rule ssubst)

qed

section ‹2ª demostración›

lemma

assumes "s ⊆ t"

shows "f ` s ⊆ f ` t"

proof

fix y

assume "y ∈ f ` s"

then show "y ∈ f ` t"

proof

fix x

assume "y = f x"

assume "x ∈ s"

then have "x ∈ t"

using ‹s ⊆ t› by (simp only: set_rev_mp)

then have "f x ∈ f ` t"

by simp

with ‹y = f x› show "y ∈ f ` t"

by simp

qed

section ‹3ª demostración›

lemma

assumes "s ⊆ t"

shows "f ` s ⊆ f ` t"

using assms

by blast

section ‹4ª demostración›

lemma

assumes "s ⊆ t"

shows "f ` s ⊆ f ` t"

using assms

by (simp only: image_mono)

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="lean"> (o <pre lang="isar">) y otra con </pre>

[/expand]

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]

Imagen de la imagen inversa

PorJosé A. Alonso 10 junio 202112 junio 2021

Demostrar que

   f[f¹[u]] ⊆ u

1	f[f¹[u]] ⊆ u

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

import data.set.basic
open set

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

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

import data.set.basic

open set

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

variable f : α → β

variable u : set β

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

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
open set

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

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

example : f '' (f⁻¹' u) ⊆ u :=
begin
  intros y h,
  cases h with x h2,
  cases h2 with hx fxy,
  rw ← fxy,
  exact hx,
end

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

example : f '' (f⁻¹' u) ⊆ u :=
begin
  intros y h,
  rcases h with ⟨x, hx, fxy⟩,
  rw ← fxy,
  exact hx,
end

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

example : f '' (f⁻¹' u) ⊆ u :=
begin
  rintros y ⟨x, hx, fxy⟩,
  rw ← fxy,
  exact hx,
end

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

example : f '' (f⁻¹' u) ⊆ u :=
begin
  rintros y ⟨x, hx, rfl⟩,
  exact hx,
end

-- 5ª demostración
-- ===============

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

-- 6ª demostración
-- ===============

example : f '' (f⁻¹' u) ⊆ u :=
by simp

import data.set.basic

open set

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

variable f : α → β

variable u : set β

-- 1ª demostración

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

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

begin

intros y h,

cases h with x h2,

cases h2 with hx fxy,

rw ← fxy,

exact hx,

end

-- 2ª demostración

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

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

begin

intros y h,

rcases h with ⟨x, hx, fxy⟩,

rw ← fxy,

exact hx,

end

-- 3ª demostración

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

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

begin

rintros y ⟨x, hx, fxy⟩,

rw ← fxy,

exact hx,

end

-- 4ª demostración

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

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

begin

rintros y ⟨x, hx, rfl⟩,

exact hx,

end

-- 5ª demostración

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

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

image_preimage_subset f u

-- 6ª demostración

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

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

by simp

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

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

theory Imagen_de_la_imagen_inversa
imports Main
begin

section ‹1ª demostración›

lemma "f ` (f -` u) ⊆ u"
proof (rule subsetI)
  fix y
  assume "y ∈ f ` (f -` u)"
  then show "y ∈ u"
  proof (rule imageE)
    fix x
    assume "y = f x"
    assume "x ∈ f -` u"
    then have "f x ∈ u"
      by (rule vimageD)
    with ‹y = f x› show "y ∈ u"
      by (rule ssubst)
  qed
qed

section ‹2ª demostración›

lemma "f ` (f -` u) ⊆ u"
proof
  fix y
  assume "y ∈ f ` (f -` u)"
  then show "y ∈ u"
  proof
    fix x
    assume "y = f x"
    assume "x ∈ f -` u"
    then have "f x ∈ u"
      by simp
    with ‹y = f x› show "y ∈ u"
      by simp
  qed
qed

section ‹3ª demostración›

lemma "f ` (f -` u) ⊆ u"
  by (simp only: image_vimage_subset)

section ‹4ª demostración›

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

end

theory Imagen_de_la_imagen_inversa

imports Main

begin

section ‹1ª demostración›

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

proof (rule subsetI)

fix y

assume "y ∈ f ` (f -` u)"

then show "y ∈ u"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ f -` u"

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 ` (f -` u) ⊆ u"

proof

fix y

assume "y ∈ f ` (f -` u)"

then show "y ∈ u"

proof

fix x

assume "y = f x"

assume "x ∈ f -` u"

then have "f x ∈ u"

by simp

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

by simp

qed

section ‹3ª demostración›

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

by (simp only: image_vimage_subset)

section ‹4ª demostración›

lemma "f ` (f -` u) ⊆ 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]